Many mathematical expressions include "dummy variables," also called "bound variables." For example, $\sum_{i=1}^n a_i$ uses $i$ as a "dummy" or "bound" variable. Similarly, $\int x^2;dx$ has $x$ as a bound varibale. There are many other examples, including (but not limited to) the following.

• indexed sums, products, unions, and intersections throughout mathematics
• set-builder notation, e.g., $\left\{ x+y \mid 0 < x < y \right\}$
• existentially and universally quantified expressions, such as $\forall x > 0, ~|x|=x$.
• $\lambda$ expressions from computer science, as in $\lambda x.x$

We say that such expressions "bind" the dummy/bound variable, and we have two types of them in Lurch: BindingExpressions and BindingEnvironments. In order to factor the common attributes out of those two classes, we implement the notion of binding as what some languages call an "interface," here. We place it in the BindingInterface namespace, and it can be added to any class by calling the addTo() function.

Each of the example types of expressions given above include not only a body in which a variable is bound, but also an operator applied to that body. For example, in $\bigcup_i A_i$, we not only have the body $A_i$ in which $i$ is bound, but we are also applying the union operator to that body. However, we do not include the operator in the binding itself, because not all cases use an operator; in particular, BindingEnvironments do not have an operator.

Consequently, when encoding something like $\bigcup_i A_i$, we would encode the $A_i$ as the body of a BindingExpression with a bound variable list of length 1, containing just $i$, and then wrap that BindingExpression in an Application of the $\cup$ Symbol. One might construct it with code like the following example (though this is not the only possible way to encode such an idea).

new Application(
    new LurchSymbol( '⋃' ),
    new BindingExpression(
        new LurchSymbol( 'i' ),
        new Application(
            new LurchSymbol( 'subscript' ),
            new LurchSymbol( 'A' ),
            new LurchSymbol( 'i' )
        )
    )
)

Bindings were inspired by a structure of the same name defined in the OpenMath Standard, but the reader is not expected to read that standard; we define in this documentation our version of what a binding is, both for Expressions and Environments.

A binding is defined by a sequence of $n$ children satisfying the following requirements. Most functions in this interface depend upon these requirements being satisfied in order for the functions to work correctly. Constructors for classes implementing this interface should check to ensure that these requirements are satisfied at construction time, and provide documentation stating that clients should not violate these requirements with tree manipulation later.

• The first $n-1$ children will be the sequence of bound variables. There must be at least one bound variable, so we have that $n>1$. Each bound variable must be a Symbol. You can use allAreSymbols() to help verify the requirement.
• The last child is called the body(). This is what "sits inside" the binding, such as the integrand in an integral, the summand in a summation, the inner statement in a quantification, etc. Although it is most commonly an Expression, it does not have to be; a binding with an Expression body is a BindingExpression and a binding with an Environment body is a BindingEnvironment. Binding environments are typically subproofs that begin with the declaration of one or more arbitrary variables, which act as bound within that subproof.

The API provided in this namespace can be added to any class by calling the addTo() function on the class's prototype. Then all the functions documented below will be available in members of that class.