import { LogicConcept } from '../logic-concept.js'
import { Application } from '../application.js'
import { BindingExpression } from '../binding-expression.js'
import { Symbol as LurchSymbol } from '../symbol.js'
import {
expressionFunctionApplication, isAnEF, newEF, parametersOfEF, bodyOfEF
} from './expression-functions.js'
import { metavariable } from './metavariables.js'
/**
* ## 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$.
* 1. The inner $g$ is now a 1 because it was bound by the first $\lambda$
* above it.
* 1. 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 {@link 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 {@link MathConcept MathConcepts}.
*
* 1. It is not only $\lambda$ expressions that are supported, but any kind of
* {@link BindingExpression}. For example, we can encode $\forall~x.(P~x)$
* as $\forall.(P~1)$.
* 2. Because a {@link 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 {@link LogicConcept#fromPutdown
* 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 {@link Symbol}, we can compute its encoding as a pair of de Bruijn
* indices with {@link module:deBruijn.encodeSymbol encodeSymbol()}. We
* represent that pair as another {@link 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 {@link module:deBruijn.decodeSymbol decodeSymbol()}).
* However, if you wish to fetch just the indices of the encoded symbol, you can
* do so with {@link module:deBruijn.encodedIndices encodedIndices()}.
*
* The {@link module:deBruijn.encodeSymbol encodeSymbol()} function is not,
* however, of much use to clients, who typically want to encode entire
* {@link Expression Expressions}, not just individual symbols within them.
* Given an {@link Expression}, we can compute its de Bruijn encoding using
* {@link module:deBruijn.encodeExpression encodeExpression()}. It yields
* another expression with the following properties.
*
* * At each position where a {@link Symbol} had sat, its encoding (under
* {@link module:deBruijn.encodeSymbol encodeSymbol()}) will sit instead.
* * The entire resulting expression contains no
* {@link BindingExpression BindingExpressions}.
* * At each position where a {@link BindingExpression} had sat as a
* subexpression, instead an {@link Application} now sits, of the form
* `(A B)`, where `A` is a special symbol indicating that a
* {@link BindingExpression} has been encoded, and `B` is the encoding of the
* body of the original {@link 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 {@link module:deBruijn.decodeExpression decodeExpression()}).
*
* To give one full, explicit example, consider the {@link Expression} (in
* {@link LogicConcept#fromPutdown 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 {@link module:deBruijn.free 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, {@link module:Matching 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
* {@link module:deBruijn.decodeExpression 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 {@link module:deBruijn.equal equal()}
* function for this purpose. It simply calls the {@link MathConcept#equals
* equals()} function in the {@link MathConcept} class, passing an optional
* argument that tells it to ignore the attributes in question when doing its
* comparison.
*
* @module deBruijn
*/
/**
* This string is used for several purposes in this module.
*
* * Encoded {@link Symbol Symbols} use this string as the key for the
* attribute that stores their original text.
* * Encoded {@link BindingExpression BindingExpressions} use this string as
* the key for the attribute that stores their original list of bound symbol
* names.
* * Encoded {@link BindingExpression BindingExpressions} are
* {@link Application Applications} whose operator is a symbol with this
* string as its text.
*/
export const deBruijn = 'LDE DB'
// A symbol whose value is the above constant
const deBruijnSymbol = new LurchSymbol( deBruijn )
// Given any symbol, compute the i and j that form its index pair (i,j),
// defined in the documentation at the top of this module.
// Or, if the symbol is free where it sits, return undefined.
const symbolToIndices = symbol => {
const binders = symbol.ancestorsSatisfying(
a => a instanceof BindingExpression )
for ( let i = 0 ; i < binders.length ; i++ ) {
const boundSymbols = binders[i].boundSymbols()
for ( let j = 0 ; j < boundSymbols.length ; j++ )
if ( boundSymbols[j].text() == symbol.text() )
return [ i, j ]
}
}
/**
* This function takes an input {@link Symbol} and returns an output
* {@link Symbol} whose name encodes the de Bruijn index of the first symbol.
* Recall from the definition at the top of this module that, in this module, a
* de Bruijn index is a pair of natural numbers. Note that the context of the
* input {@link Symbol} (its ancestor chain, and whether it is bound by any of
* those ancestors) is what determines the result of this function.
*
* The encoded symbol returned by this function has an attribute that stores the
* original name of this symbol, so that this encoding can be reversed by
* {@link module:deBruijn.decodeSymbol decodeSymbol()}. For two important
* details about how symbol encoding coordinates with the Matching module, see
* the documentation at the top of this module.
*
* @function
* @param {Symbol} symbol the symbol to be encoded
* @returns {Symbol} a new symbol whose name encodes the de Bruijn indices of
* the input
* @see {@link module:deBruijn.encodedIndices encodedIndices()}
* @see {@link module:deBruijn.decodeSymbol decodeSymbol()}
* @see {@link module:deBruijn.encodeExpression encodeExpression()}
*/
export const encodeSymbol = symbol => {
// Exceptions: Don't modify special symbol used for EFAs, nor metavariables:
if ( symbol.equals( expressionFunctionApplication )
|| symbol.isA( metavariable ) )
return symbol.copy()
// Okay, now do the normal de Bruijn encoding:
const indices = symbolToIndices( symbol )
return new LurchSymbol( JSON.stringify(
indices ? [ deBruijn, ...indices ] : [ deBruijn, symbol.text() ]
) ).attr( [ [ deBruijn, symbol.toJSON() ] ] )
}
/**
* This function takes a {@link Symbol} encoded by the
* {@link module:deBruijn.encodeSymbol encodeSymbol()} function and returns the
* de Bruijn indices stored within its name.
*
* @function
* @param {Symbol} symbol a symbol that was de Bruijn-encoded
* @returns {number[]} a pair of natural numbers, the de Bruijn indices of the
* input
* @see {@link module:deBruijn.encodeSymbol encodeSymbol()}
* @see {@link module:deBruijn.decodeSymbol decodeSymbol()}
*/
export const encodedIndices = symbol => {
if ( !( symbol instanceof LurchSymbol ) ) return
try {
const parts = JSON.parse( symbol.text() )
return parts.length == 3 && parts[0] == deBruijn ?
parts.slice( 1 ) : undefined
} catch {
return undefined
}
}
/**
* Alter the name of a de Bruijn index (an encoded {@link Symbol}) so that it
* still encodes a de Bruijn index, but the two components have been adjusted
* (up or down) by the differences given in the latter two arguments. That is,
* a de Bruijn index $(i,j)$ can be adjusted with $(\Delta_i,\Delta_j)$ to
* become $(i+\Delta_i,j+\Delta_j)$.
*
* If the first argument is an {@link Application}, this function distributes
* itself across the {@link Application}'s children. If it is neither a
* {@link Symbol} nor an {@link Application}, this function does nothing.
*
* @function
* @param {Symbol} target an encoded de Bruijn index
* @param {integer} deltaI the amount by which to adjust the first component of
* the index
* @param {integer} deltaJ the amount by which to adjust teh second component of
* the index
*/
export const adjustIndices = ( target, deltaI, deltaJ ) => {
if ( target instanceof Application )
return target.children().forEach( child =>
adjustIndices( child, deltaI, deltaJ ) )
const original = encodedIndices( target )
if ( !original ) return
target.setAttribute( 'symbol text', JSON.stringify(
[ deBruijn, original[0] + deltaI, original[1] + deltaJ ] ) )
}
/**
* This function takes a {@link Symbol} encoded by the
* {@link module:deBruijn.encodeSymbol encodeSymbol()} function and returns (a
* copy of) the original symbol that was passed to the encoding function. The
* de Bruijn indices encoded in the input are discarded, and its original name
* (stored in an attribute) is restored.
*
* If it receives a symbol that has no de Bruijn encoding information stored in
* an attribute, it returns the symbol untouched.
*
* @function
* @param {Symbol} symbol a symbol that was de Bruijn-encoded
* @returns {Symbol} a copy of the original {@link Symbol} that was encoded to
* produce the input `symbol`
* @see {@link module:deBruijn.encodeSymbol encodeSymbol()}
* @see {@link module:deBruijn.encodedIndices encodedIndices()}
* @see {@link module:deBruijn.decodeExpression decodeExpression()}
*/
export const decodeSymbol = symbol => {
const serialized = symbol.getAttribute( deBruijn )
return serialized ? LogicConcept.fromJSON( serialized ) : symbol.copy()
}
/**
* This function takes an input {@link Expression} and returns an output
* {@link Expression} that is the de Bruijn-encoded form of the input. The full
* list of guarantees this function provides, and the properties its output will
* have, is given in the documentation at the top of this module.
*
* In summary, all of its {@link BindingExpression BindingExpressions} have been
* replaced with {@link Application Applications} with no bound symbols, and all
* formerly-bound symbols have been replaced with their encoded versions as de
* Bruijn indices, as computed by the
* {@link module:deBruijn.encodeSymbol encodeSymbol()}) function.
*
* This operation can be reversed by applying the
* {@link module:deBruijn.decodeExpression decodeExpression()} function.
*
* @function
* @param {Expression} expression the expression to be encoded
* @returns {Expression} the encoded version, with the properties described
* above
* @see {@link module:deBruijn.encodeSymbol encodeSymbol()}
* @see {@link module:deBruijn.decodeExpression decodeExpression()}
*/
export const encodeExpression = expression =>
expression instanceof LurchSymbol ? encodeSymbol( expression ) :
expression instanceof Application ? new Application(
...expression.children().map( encodeExpression ) ) :
// therefore expression instanceof BindingExpression:
new Application(
deBruijnSymbol.copy().attr( [ [
deBruijn, expression.boundSymbols().map( symbol => symbol.toJSON() )
] ] ),
encodeExpression( expression.body() ) )
export const isEncodedBinding = expression =>
( expression instanceof Application )
&& equal( expression.child( 0 ), deBruijnSymbol )
/**
* This function takes an {@link Expression} encoded by the
* {@link module:deBruijn.encodeExpression encodeExpression()} function
* and returns (a copy of) the original expression that was passed to the
* encoding function.
*
* @function
* @param {Symbol} symbol an expression that was de Bruijn-encoded
* @returns {Symbol} a copy of the original {@link Expression} that was encoded
* to produce the input `expression`
* @see {@link module:deBruijn.encodeExpression encodeExpression()}
* @see {@link module:deBruijn.decodeSymbol decodeSymbol()}
*/
export const decodeExpression = expression => {
// Case 1: Symbols have their own decoding routine
if ( expression instanceof LurchSymbol )
return decodeSymbol( expression )
// Case 2: Expression Functions
if ( isAnEF( expression ) )
return newEF(
...parametersOfEF( expression ).map( v => v.copy() ),
decodeExpression( bodyOfEF( expression ) )
)
// Case 3: (Other) Applications
if ( expression instanceof Application ) {
if ( equal( expression.child( 0 ), deBruijnSymbol ) ) {
// subcase 1: application that encodes what used to be a binding
const symbolNames = expression.child( 0 ).getAttribute( deBruijn )
if ( !symbolNames )
throw new Error( 'Missing de Bruijn attribute on Application' )
return new BindingExpression(
...symbolNames.map( json => LogicConcept.fromJSON( json ) ),
decodeExpression( expression.child( 1 ) ) )
} else {
// subcase 2: application that is just an application
return new Application(
...expression.children().map( decodeExpression ) )
}
}
// therefore expression instanceof BindingExpression, which means this is
// not a correctly-encoded de Bruijn expression
throw new Error( 'No bindings permitted in de Bruijn encodings' )
}
/**
* See the documentation at the top of this module for why it is important to be
* able to test two expressions for equivalence, ignoring the attributes that
* may have been added during the de Bruijn encoding process that produced those
* two expressions. This function does exactly that, using the
* `attributesToIgnore` feature of the {@link MathConcept#equals equals()}
* function in the {@link MathConcept} class.
*
* @function
* @param {Expression} expression1 the left-hand side of the equality test; this
* function asks if this is equal to `expression2`
* @param {Expression} expression2 the right-hand side of the equality test;
* this function asks if this is equal to `expression1`
* @returns {boolean} whether the two {@link Expression Expressions} are equal
* except for any attributes that were added as part of the de Bruijn encoding
* process
*/
export const equal = ( expression1, expression2 ) =>
expression1.equals( expression2, [ deBruijn ] )
/**
* A de Bruijn index, as defined at the top of this module, is a symbol encoding
* a pair of natural numbers, the first of which says how many bindings one must
* pass as one walks up the ancestor chain of this symbol before we encounter
* the binding that binds this symbol. Thus a de Bruijn index is free if the
* number of bindings in its ancestor chain is greater than or equal to that
* first index.
*
* This function tests that and returns true if that freeness condition is met,
* false if the first component of the de Bruijn index is smaller than the
* number of bindings above the symbol, and undefined if the argument given is
* not a de Bruijn index. Note that, because we are working with
* {@link Expressions} that have been encoded with
* {@link module:deBruijn.encodeExpression encodeExpression()}, a binding is not
* a {@link BindingExpression}, but an encoded version thereof.
*
* @param {Symbol} symbol the symbol to test for freeness
* @returns {boolean} whether the symbol is a free de Bruijn index
*/
export const free = symbol => {
const indices = encodedIndices( symbol )
if ( !indices ) return undefined
const encodedBindings = symbol.ancestorsSatisfying( isEncodedBinding )
return indices[0] >= encodedBindings.length
}
source