What are de Bruijn indices?

One way to express bound variables without giving them explicit names is to use de Bruijn indices, a technique that replaces symbols with numbers. The standard version of this method applies to the $\lambda$-calculus, replacing a bound variable $x$ with a natural number $n$ that is equal to the number of levels of nested $\lambda$ expressions one must walk up the syntax tree to find the one that binds $x$.

For example, $\lambda f.\lambda g.(f~(g~x))$ could be expressed as $\lambda.\lambda.(2~(1~x))$. Notice these properties of the example:

1. The inner $f$ of the original expression is replaced with a 2, because one must walk out two "$\lambda$ levels" to find the $\lambda$ that originally bound $f$.
2. The inner $g$ is now a 1 because it was bound by the first $\lambda$ above it.
3. The bound variable names are not needed, because the order of quantification is clear from the indices.

Had the example been something like $(\circ~(\lambda~x.x)~(\lambda~y.y))$, it would have become $(\circ~(\lambda.1)~(\lambda.1))$, showcasing how de Bruijn indices reduce $\alpha$-equivalence to mere expression equality.

Purpose of this module

This module provides tools to encode MathConcept instances using de Bruijn indices, but we make the following changes to extend the method from the standard version introduced above to a version that supports the full range of MathConcepts.

1. It is not only $\lambda$ expressions that are supported, but any kind of BindingExpression. For example, we can encode $\forall~x.(P~x)$ as $\forall.(P~1)$.
2. Because a BindingExpression can bind multiple variables, we must distinguish them, so our indices will be pairs, one index for the binding level (as above) and one index for which position within that binding was occupied by the symbol being encoded. For example, $\forall x,y.(>~x~y)$ can be encoded as $\forall.(>~(1,1)~(1,2))$, where I'm using the standard notation for pairs. This applies even if the binder binds only one variable, so the example from item 1., above, would actually be encoded as $\forall.(P~(1,1))$.
3. Unlike the original de Bruijn notation, we will use zero-based indexing, to be consistent with everything else in our codebase, which uses zero-based indexing. Thus the two examples from item 2., above, would actually be encoded as $\forall.(>~(0,0)~(0,1))$ and $\forall.(P~(0,0))$, respectively.

The notation used above is to illustrate the general concept of the de Bruijn conversion only. Obviously pairs like $(a,b)$ and bindings with no bound symbols like $\lambda.1$ are not valid putdown notation, so they do not represent the actual encoding. The details of that encoding appear in the next section.

Functions in this module

Given a Symbol, we can compute its encoding as a pair of de Bruijn indices with encodeSymbol(). We represent that pair as another Symbol whose name is a JSON encoding that includes the pair of indices, and that has the original symbol name stored as an attribute, so that the conversion can be inverted later (with decodeSymbol()). However, if you wish to fetch just the indices of the encoded symbol, you can do so with encodedIndices().

The encodeSymbol() function is not, however, of much use to clients, who typically want to encode entire Expressions, not just individual symbols within them. Given an Expression, we can compute its de Bruijn encoding using encodeExpression(). It yields another expression with the following properties.

• At each position where a Symbol had sat, its encoding (under encodeSymbol()) will sit instead.
• The entire resulting expression contains no BindingExpressions.
• At each position where a BindingExpression had sat as a subexpression, instead an Application now sits, of the form (A B), where A is a special symbol indicating that a BindingExpression has been encoded, and B is the encoding of the body of the original BindingExpression.
• Each such A will be decorated with an attribute that records the original names of the bound symbols, so that this encoding is invertible (using decodeExpression()).

To give one full, explicit example, consider the Expression (in putdown notation) (forall (x y) , (> x y)). Its de Bruijn encoding, according to this module, would be the following. I will use the symbol "LDE DB" as the special symbol meaning "encoded binding" and also as the attribute key for all de Bruijn attributes. Some JSON encodings have been simplified for readability, as you can see below.

(forall
  ("LDE DB" +{"LDE DB":"['x','y']"} // list of bound variable names
    (>
      "['LDE DB',0,0]" +{"LDE DB":"JSON encoding of original x symbol"}
      "['LDE DB',0,1]" +{"LDE DB":"JSON encoding of original y symbol"}
    )
  )
)

The module also provides a freeness test for de Bruijn indices, which returns true for an index $(n,m)$ iff there are at least $n+1$ encoded bindings surrounding the symbol.

Coordinating with matching

There are two exceptions to the above encoding description, each of which helps this module integrate correctly with the larger module in which it sits, the Matching module.

First, when encoding a symbol, if the symbol is a metavariable, then don't encode it at all, but leave it in its original form.

Second, one of the special symbols in the matching package, the one that marks Expression Functions Applications, is not encoded, but is left unchanged under the de Bruijn encoding. That way, Expression Function Applications retain their meanings under the de Bruijn encoding.

Finally, we do not need to apply the same protection to the Expression Function symbol, because we will not be applying the de Bruijn encoding to Expression Functions, and it would break them anyway, since it removes all bindings. But when decoding the image of a metavariable in a solution, an Expression Function may be present, so the decodeExpression() function recurs inside such structures.

Expression equality

As mentioned above, one of the benefits of de Bruijn indices is that two expressions are $\alpha$-equivalent iff their de Bruijn encodings are exactly equal. However, the implementation above mentions that our encoding function stores the original names of the bound symbols as attributes so that the encoding is invertible. Thus if we encode the identity function $\lambda x.x$ and also encode the identity function $\lambda y.y$, although the resulting expressions would seem equal, both being something like $\lambda.(0,0)$, but their attributes would distinguish them:

// Encoding of (lambda x , x):
(lambda
  ("LDE DB" +{"LDE DB":['x']}
    "['LDE DB',0,0]" +{"LDE DB":"JSON encoding of the symbol x"}
  )
)
// Encoding of (lambda y , y):
(lambda
  ("LDE DB" +{"LDE DB":['y']}
    "['LDE DB',0,0]" +{"LDE DB":"JSON encoding of the symbol y"}
  )
)

Without the attributes, we would be comparing (lambda ("LDE DB" "['LDE DB',0,0]")) to itself. With the attributes, we can still distinguish formerly-$x$ from formerly-$y$, which is undesirable.

Thus we need a way to compare two expressions for equality, but ignore these hidden attributes that are present only to enable the inversion of the de Bruijn encoding. We define the equal() function for this purpose. It simply calls the equals() function in the MathConcept class, passing an optional argument that tells it to ignore the attributes in question when doing its comparison.