2.1. Named Syntax🔗

We now return to the notation used at the beginning of the chapter. De Bruijn indices are convenient for the implementation, but a term such as λ λ 1 0 is unnecessarily difficult to read. Named terms record the syntax written on paper: variables have names, and lambdas say which name they bind.

e ::= x \mid \lambda x.\ e \mid e\ e

This datatype is raw syntax: it remembers the literal choice of binder name. Consequently λx. x and λy. y are different values of Term, even though they describe the same function. We will recover the usual notion of equality up to binder renaming through compilation.

2.2. Compilation to De Bruijn Terms🔗

Compilation translates readable named syntax into the de Bruijn representation that already carries the semantics. While traversing a term, the list ctx records the binders currently in scope. The nearest binder is at the head.

When the compiler encounters a variable x, it searches this list. If the first occurrence of x is at position n, the variable becomes bound index n. If x is absent, it remains a named free variable.

\begin{array}{rcl} \llbracket x \rrbracket_\rho &=& \begin{cases} n & \rho(n) = x\\ x & x \notin \rho \end{cases}\\ \llbracket \lambda x.\ e \rrbracket_\rho &=& \lambda.\ \llbracket e \rrbracket_{x,\rho}\\ \llbracket e_1\ e_2 \rrbracket_\rho &=& \llbracket e_1 \rrbracket_\rho\ \llbracket e_2 \rrbracket_\rho \end{array}

For example, compiling λx. λy. x proceeds with the binder lists [], then [x], then [y,x]. The occurrence of x is found at position one, producing λ λ 1.

Adding new binders at the head also handles shadowing. In λx. λx. x, the occurrence is found at position zero and therefore refers to the inner lambda.

The compiler cannot create a dangling index: every index comes from an actual name in the binder list. The first theorem states the precise invariant. If the list contains d binders, the compiled term is scoped at depth d. Starting with the empty list therefore produces a locally closed term.

To recover an actual named common reduct later, we also need to print a scoped de Bruijn term with names. Binder names are chosen fresh from the names already in use; their particular spelling has no mathematical significance.

2.3. Free Variables of Named Terms🔗

Free variables are easy to read directly from named syntax, so here we use the standard recursive definition rather than hiding it behind compilation. A variable contributes its name, application takes the union, and a lambda removes the name it binds.

\begin{array}{rcl} FV(x) &=& \{x\}\\ FV(\lambda x.\ e) &=& FV(e) \setminus \{x\}\\ FV(e_1\ e_2) &=& FV(e_1) \cup FV(e_2) \end{array}

This does not introduce a competing meaning of “free variable.” The theorem fv_toDBWith proves that the direct definition agrees with the de Bruijn one after compilation. Its extra condition z ∉ ρ says that a name already supplied by the binder list is no longer free. With an empty binder list this condition disappears, giving fv_toDB.

A named term is closed when this set is empty. Abstraction shape is another simple syntactic observation, so IsAbstraction is also defined directly on Term. The bridge theorems below show that closedness and abstraction shape agree with compilation.

2.4. Semantics of Named Terms🔗

2.5. Programming with Untyped Terms🔗

The calculus contains no primitive data. Nevertheless, functions can encode familiar computations. From this point onward we use named terms for examples and rely on compilation for their meaning.

The identity function returns its argument. Church booleans encode true and false by their choice between two arguments: true selects the first, while false selects the second. A conditional can therefore apply its boolean to the two branches. Negation asks the boolean to choose false before true, reversing its result.