Abstract Syntax
trees are all you need
(1 1 (0 (1 0 1) 0))
All programming languages are syntactic sugar over abstract syntax trees. Abstract syntax lets you describe abitrary relational structure in your data regardless of its presentation. QBAR uses a minimal, Unicode-friendly s-expression language to represent all of its structured data.
Substitution
application is substitution(app (λ b) a) ≡ (subst b (id a))
Substitutions are the only interpretation-agnostic way to interact with abstract syntax. Given any expression and an atomic element in that expression, a substitution replaces all occurences of that atomic element by another expression. Function application, the most fundamental computational primitive is just substitution. QBAR supports substitution as a first class operation on all expressions.
Immutable Data
no names, no problems- bc14d39fcd29 => ((A ∨ B) ≡ (¬ ((¬ A) ∧ (¬ B))))
- 7ebd5dbac0db => (((f ∘ g) ∘ h) = (f ∘ (g ∘ h)))
- 9a4eba888924 => ((_) (_ _))
- d8c051530081 => ((rec M Z S) ↦ (rec M' Z S))
- 582eb1f484ab => (Δ ⊢ (subst T id) ≡ T type)
In QBAR, all expressions have a unique cryptographic hash associated to them which is the only allowed reference to that expression. Since we can't track changes in an expression without changing its hash, references can never be spoofed. This keeps objects and references immutable and safe.
Transformation Rules
make your inference rules stateful
Inference rules describe transformations in our knowledge of a given system. Knowledge is not just about mathematical truth, it's about state. In QBAR, rules consume a multiset of expressions and return another multiset of expressions.
Linear Compositions
rules always compose
(Γ ⊢ L type)
[weak]———————————————————
(p : (Γ L) ← Γ) (Γ ⊢ R type)
————————————————————————————————————[sub]
(Γ ⊢ L type) ((Γ L) ⊢ (subst R p) type)
———————————————————————————————————————————————[Σ-form]
(Γ ⊢ (Σ L (subst R p)) type)
dup (_ (Γ ⊢ L type))
weak (T L)
sub (δ p Δ Γ Γ (Γ L) T R)
Σ-form (X L T (subst R p))
When transformation rules take multisets to multisets, we can infer on all branches of a derivation tree at once. In this way, all rules are composable with each other: no premise-conclusion matching needed. On top of that, rule composition is associative, so reducing a composition is embarrassingly-parallel.
The Shell
data is not a programming languageQ❯ ...
Since we want to be able to model any domain problem, we can't pick the right programming language for you. Instead, QBAR comes with a proof assistant toolkit to analyze your structured data and verify your substitutions, rules, and compositions, which can be used in any programming environment.