syntax design

Design goal

syntax gives Luna Flow one definition of “syntax with binders” that is small enough for any symbolic AST to adopt, yet precise enough to prove the usual laws of free variables, alpha-equivalence and renaming. It serves two audiences: the lambda calculus packages, which use the concrete Term[T], and downstream ASTs, which keep their own types and reach the same algorithms through BindingSyntax.

Mathematical background

Terms

Fix the set of names $\mathcal{N}$ of the core design and a set $V$ of domain values. Terms are generated by

$$t, u \;::=\; v \;\mid\; x \;\mid\; t(u_1, \dots, u_n) \;\mid\; \beta x.\, t \qquad (v \in V,\ x \in \mathcal{N},\ n \ge 0),$$

matching the constructors Value, Variable, Apply and Bind. The binder $\beta x.\,t$ is generic: the lambda calculus reads it as $\lambda x.\,t$, a polynomial library may read it as a local scope. Values are atoms: they contain no names.

Free variables and names

$$\begin{aligned} \mathrm{FV}(v) &= \varnothing, & \mathrm{FV}(x) &= \{x\}, \\ \mathrm{FV}(t(u_1,\dots,u_n)) &= \mathrm{FV}(t) \cup \textstyle\bigcup_i \mathrm{FV}(u_i), & \mathrm{FV}(\beta x.\,t) &= \mathrm{FV}(t) \setminus \{x\}. \end{aligned}$$

$\mathrm{names}(t)$ is defined by the same equations except $\mathrm{names}(\beta x.\,t) = \mathrm{names}(t) \cup \{x\}$; it is the set all_names returns, and $\mathrm{FV}(t) \subseteq \mathrm{names}(t)$.

Alpha-equivalence

For $y \notin \mathrm{names}(t)$ write $t\{x \mapsto y\}$ for $t$ with every free occurrence of $x$ replaced by $y$. Because $y$ occurs nowhere in $t$, no occurrence can be captured. Alpha-equivalence $=_\alpha$ is the least congruence on terms such that

$$\beta x.\, t \;=_\alpha\; \beta y.\, t\{x \mapsto y\} \qquad \text{whenever } y \notin \mathrm{names}(t).$$

All the operations of this library are invariant under $=_\alpha$, and the lambda calculi are defined on alpha-equivalence classes.¹1 H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland 1984, §2.1. The library does not rely on the “variable convention” of that book; every operation renames explicitly when needed.

Design decisions

One generic term type with an opaque payload

Problem. Every symbolic package needs variables and binders, but each has its own constants: numbers, operators, typed constants.

Options. A fixed lambda calculus with an extensible constant type; a separate term type per package; one term type parameterised by the constants.

Choice. Term[T] is parameterised by its constants, and T is opaque: the algorithms never look inside a Value. This is sound only if constants contain no variables, which is the stated contract (“T is a closed atom”). An AST whose constants do contain variables must implement BindingSyntax instead (next section). Application is n-ary because most symbolic ASTs apply an operator to several arguments; the lambda calculi read it as a curried spine.

A view trait instead of a fixed AST

Problem. Downstream repositories already have ASTs. Converting them to Term[T] and back for every substitution costs time and loses structure.

Choice. BindingSyntax describes a node through a one-layer view. In categorical terms, define the signature functor

$$F(X) = 1 \;+\; \mathcal{N} \;+\; X \times X^{*} \;+\; \mathcal{N} \times X .$$

BindingView[N] is $F(N)$, project is a coalgebra $N \to F(N)$, and variable, apply, bind form an algebra on the three non-opaque summands. Every generic algorithm is a structural recursion that calls project, works on the children, and rebuilds with the constructors. The laws an implementation owes are listed in the adapter design; for Term[T] they hold by construction, since project is a bijection between non-Value terms and non-Opaque views.

Consequence. For Term[T], each generic function computes the same result as its specialised version:

$$\texttt{generic\_free\_variables}(t) = \mathrm{FV}(t), \qquad \texttt{generic\_all\_names}(t) = \mathrm{names}(t),$$

and generic_alpha_rename_bound agrees with Term::alpha_rename_bound. The proof is a direct induction: in each case the two functions have the same equation, because project returns exactly the constructor’s fields.

Deciding alpha-equivalence with binder levels

Problem. Deciding $=_\alpha$ directly from the definition requires searching for renamings.

Choice. alpha_equal walks both terms in lockstep with two binder environments $E_L, E_R$ that map each bound name to the level (binder depth, counting from the root) at which it was bound; a later binding of the same name shadows an earlier one. Writing $E(x)$ for the level of the last binding of $x$ in $E$, and $d$ for the current depth:

$$\begin{aligned} E_L, E_R \vdash_d v \sim v' &\iff v = v', \\ E_L, E_R \vdash_d x \sim y &\iff \begin{cases} E_L(x) = E_R(y) & \text{if both are bound},\\ x = y & \text{if both are free},\\ \text{false} & \text{otherwise}, \end{cases}\\ E_L, E_R \vdash_d t(\bar u) \sim t'(\bar u') &\iff |\bar u| = |\bar u'| \wedge t \sim t' \wedge \textstyle\bigwedge_i u_i \sim u'_i, \\ E_L, E_R \vdash_d \beta x.\,t \sim \beta y.\,t' &\iff E_L[x \mapsto d], E_R[y \mapsto d] \vdash_{d+1} t \sim t'. \end{aligned}$$

Theorem. alpha_equal(t, u) holds iff $t =_\alpha u$.

Proof sketch. Let $\ulcorner t \urcorner$ be the De Bruijn translation of the debruijn design, which replaces a bound occurrence at depth $d$ whose binder sits at level $\ell$ by the index $i = d - 1 - \ell$, and keeps free names. Both traversals visit the same positions at the same depth $d$, so for bound occurrences

$$\ell_L = \ell_R \iff d - 1 - \ell_L = d - 1 - \ell_R \iff i_L = i_R ,$$

and free occurrences are compared by name in both. Hence alpha_equal(t, u) iff $\ulcorner t \urcorner = \ulcorner u \urcorner$. The classical theorem that two named terms are alpha-equivalent iff their De Bruijn translations are identical²2 N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. completes the proof. $\square$

The algorithm runs in time linear in the size of the terms, plus the cost of the environment lookups (linear in the binder depth).

Capture-avoiding renaming of free variables

Problem. Applying a renaming $\rho$ under a binder can capture: renaming $x \mapsto y$ in $\beta y.\,x$ naively gives $\beta y.\,y$.

Choice. rename_free implements

$$\begin{aligned} x\rho &= \rho(x), \qquad v\rho = v, \qquad t(\bar u)\rho = (t\rho)(\overline{u\rho}),\\ (\beta x.\,t)\rho &= \begin{cases} \beta x.\; t(\rho \setminus x) & \text{if } x \notin \operatorname{tgt}(\rho \setminus x),\\ \beta x'.\; \big(t\{x \mapsto x'\}\big)(\rho \setminus x) & \text{otherwise,} \end{cases} \end{aligned}$$

with $x' = \operatorname{fresh}(x,\ \mathrm{names}(t) \cup \operatorname{supp}(\rho \setminus x) \cup \{x\})$.

Lemma (free variables of a renaming). $\mathrm{FV}(t\rho) = \rho(\mathrm{FV}(t))$.

The only interesting case is the binder without freshening. Let $\rho' = \rho \setminus x$ with $x \notin \operatorname{tgt}\rho'$. By induction $\mathrm{FV}(t\rho') = \rho'(\mathrm{FV}(t))$, so

$$\begin{aligned} \mathrm{FV}\big((\beta x.\,t)\rho\big) &= \{\rho'(n) \mid n \in \mathrm{FV}(t)\} \setminus \{x\} \\ &= \{\rho(n) \mid n \in \mathrm{FV}(t),\ n \ne x\} && \rho'(x) = x,\ \rho'(n) = \rho(n) \ne x \text{ for } n \ne x \\ &= \rho(\mathrm{FV}(\beta x.\,t)). \end{aligned}$$

The second step uses $\rho(n) \ne x$ for $n \ne x$: either $n \in \operatorname{dom}\rho'$ and $\rho(n) \in \operatorname{tgt}\rho'$, which excludes $x$, or $\rho(n) = n \ne x$. In the freshened case the same computation applies to $t\{x \mapsto x'\}$ and $x'$, since $x'$ is outside $\operatorname{supp}\rho'$ and so neither a source nor a target. The lemma says exactly that no free variable was captured.

The test $x \notin \operatorname{tgt}(\rho \setminus x)$ is conservative: it also renames the binder when the offending entry’s source does not occur in $t$. The result is still alpha-equivalent to the minimal one.

Checked bound renaming

alpha_rename_bound(t, x, y) computes $t\{x \mapsto y\}$, the body of the alpha step above, and returns None unless $y \notin \mathrm{names}(t)$ (or $x = y$). Under that side condition the alpha axiom gives directly

$$\beta x.\, t \;=_\alpha\; \beta y.\, t\{x \mapsto y\}.$$

The check is stronger than necessary (an occurrence of $y$ under an inner binder for $y$ would be harmless), but it is cheap and it is all the substitution algorithms need, because they always call it with a name chosen fresh for the body.

Correctness / invariants

• $\mathrm{FV}(t) \subseteq \mathrm{names}(t)$; map_values preserves both.
• alpha_equal is reflexive, symmetric and transitive, and coincides with $=_\alpha$ (theorem above). Reflexivity is also checked by a QuickCheck property in src/syntax/syntax_wbtest.mbt.
• rename_free satisfies $\mathrm{FV}(t\rho) = \rho(\mathrm{FV}(t))$ and is invariant under $=_\alpha$: alpha-equivalent inputs give alpha-equivalent outputs.
• alpha_rename_bound(t, x, y) = Some(t') implies $\beta x.\,t =_\alpha \beta y.\,t'$.
• On Term[T] every generic_* function equals its specialised counterpart.

Cost: free_variables and all_names are linear in the term size (in hash-set operations). rename_free and alpha_rename_bound are linear when no binder is renamed; each freshened binder adds a traversal of its body.

Alternatives rejected

• Variables inside values. Letting T contain names would require a traversal trait on T as well. Such ASTs implement BindingSyntax directly, which covers the same need with one trait.
• Multi-variable binders. A binder for several names at once is expressed as nested Bind nodes. This keeps the view small and the proofs per binder.
• Unchecked bound renaming. A version without the None case would make a capture silent. The checked form makes the precondition visible in the type.
• Alpha-equivalence by conversion. Converting both terms to De Bruijn form and comparing would allocate two new terms; the lockstep algorithm is the same comparison without the allocation.

Boundaries

• Value payloads are never inspected. A payload that contains variables is outside the contract.
• == on terms is structural, not alpha-equivalence.
• No sorts, scopes or types: every name is a term variable of the same kind.
• The package does not check that a BindingSyntax implementation obeys its laws; adapter describes how to test them.
• Substitution lives in substitution, traversal and rewriting in rewrite.

Footnotes

1. H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland 1984, §2.1. The library does not rely on the “variable convention” of that book; every operation renames explicitly when needed. ↩

2. N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. ↩