Two expressions are $\alpha$-equivalent if renaming the bound variables in one makes it exactly equal to the other. For example, $\forall x,R(x,2)$ is $\alpha$-equivalent to $\forall y,R(y,2)$, but not to $\forall y,R(y,y)$.

Perform $\alpha$-renaming on a binding, producing a new MathConcept that is $\alpha$-equivalent to the original, but with different names for the bound variables.

If you pass an argument to the binding parameter that does not pass the binds() test, the result of this function is undefined.

Construct a function whose body is an application of the form shown below. The caller provides the arity of the function as well as a list of symbols to be used in constructing the function's body, as shown below. Assume the given arity is $n$ and the list of symbols given is $F_1,\ldots,F_m$. Further assume that the symbol used to indicate an EFA (as defined here) is $A$. Then the expression function created will be $$ \lambda v_1,\ldots,v_n.((A~F_1~v_1~\cdots~v_n)~\cdots~(A~F_m~v_1~\cdots~v_n)). $$ This particular form is useful in the matching algorithm in the Problem class. The bound variables will be chosen so that none of them is equal to any of the symbols $F_1,\ldots,F_m$.

Applies ef as an expression function to a list of arguments. If ef is not an expression function (as per isAnEF()) or the list of arguments is the wrong length, an error is thrown. Otherwise, a copy of the body of ef is returned with all parameters substituted with arguments.

For example, if ef is an Expression representing $\lambda v_1,v_2.\sqrt{v_1^2+v_2^2}$ and A another representing $x-1$ and B another representing $y+1$, then applyEF(ef,A,B) would be a newly constructed Expression instance (sharing no subtrees with any of those already mentioned) representing $\sqrt{(x-1)^2+(y+1)^2}$.

No check is made regarding whether this might cause variable capture, and no effort is made to do $\alpha$-substitution to avoid variable capture. Thus this routine is of limited value; it should be used only in situations where the caller knows that no variable capture will take place. For example, if ef is $\lambda v.\sum_{i=1}^n i^v$ then applyEF(ef,i) is $\sum_{i=1}^n i^i$. No error is thrown; the capture simply happens.

Compute the arity of a given expression function. If ef is not an expression function (as judged by isAnEF()) then an error is thrown. Otherwise, a positive integer is returned representing the arity of the given function, 1 for a unary function, 2 for a binary function, etc.

If canBetaReduce() returns true, we may want to act upon that and perform the $\beta$-reduction. This function does so. It requires an argument that passes the canBetaReduce() test, and it will perform exactly one step of $\beta$-reduction. That is, it will substitute the arguments of the expression function application into (a copy of) the body of the expression function and return the result.

Note that the process of $\beta$-reduction is usually considered to be the repetition of this process in all possible ways until it termintes (if it does). That process is implemented in the function fullBetaReduce(). This function does just one step.

Get the body of a given expression function. If ef is not an expression function (as judged by isAnEF()) then an error is thrown. Otherwise, its function body returned, which is one of its descendants.

An expression can be $\beta$-reduced if it is an expression function application and the expression function in question is not a metavariable, but an actual expression function. To help distinguish these two possibilities, consider:

• If P is a metavariable and x is a Symbol, we could create an expression function application with, for example, newEFA(P,new Symbol(5)), but we could not evaluate it, because we do not know the meaning of P.
• If f is an expression function, that is, it would pass the test isAnEF(f) defined here, and x is as above, then (assuming the arity of f is 1) the expression newEFA(f,new Symbol(5)) can be evaluated, because f has a body and we can substitute 5 into its body in the appropriate places.

Thus we need a function to distinguish these two cases. Both will pass the test isAnEFA(), but only one can be applied. Such application is called $\beta$-reduction, so we have this function canBetaReduce() that can detect when we are in the second case, above, rather than the first. That is, does the expression being applied pass the isAnEF() test, or is it just a metavariable? This function returns true only in the former case, plus it also verifies that the correct number of arguments are present; if not, it returns false for that reason.

Examples:

• canBetaReduce(newEFA(metavar,arg)) returns false
• canBetaReduce(newEFA(newEF(symbol,body),arg)) returns true
• canBetaReduce(newEFA(newEF(symbol,body),too,many,args)) returns false

Create an expression function (as defined here) that is a constant function (that is, it always returns the same expression). That is, the function can be expressed as $\lambda v_1,\ldots,v_n. E$ for some expression $E$ not containing any of the $v_i$. The variables will have names chosen so that none of them appears free in $E$.

The constant used in this module as the operator when encoding Expression Functions as LogicConcepts. See the documentation at the top of this module for more information.

The constant used in this module as the operator when encoding Expression Function Applications as LogicConcepts. See the documentation at the top of this module for more information.

Make a copy of the given Expression, then find inside it all subexpressions passing the test in canBetaReduce(), and apply each such $\beta$-reduction using betaReduce(). Continue this process until there are no more opportunities for $\beta$-reduction.

This process is, in general, not guaranteed to terminate. Clients should take care to call it only in situations where it is guaranteed to terminate. For example, the following expression function application will $\beta$-reduce to itself, and thus enter an infinite loop. $$ ((\lambda v. (v~v))~(\lambda v. (v~v))) $$ In the LDE, we are unlikely to permit users to write input that requires us to apply expression functions to other expression functions, thus preventing cases like this one.

Test whether the given Expression encodes an Expression Function, as defined by the encoding documented at the top of this file, and as produced by the function newEF().

Test whether the given expression encodes an Expression Function Application, as defined by the encoding documented at the top of this file, and as produced by the function newEFA().

Creates a new expression function, encoded as a LogicConcept, as described at the top of this file. The arguments are not copied; if you do not wish them removed from their existing contexts, pass copies to this function.

For example, if x and y are Symbol instances with the names "x" and "y" and B is an Application, such as (+ x y), then newEF(x,y,B) will be the Expression ("LDE lambda" (x y) , (+ x y)).

Creates a new Expression Function Application, encoded as an Expression, as described at the top of this file. The arguments are not copied; if you do not wish them removed from their existing contexts, pass copies to this function.

For example, if F is an Expression representing an Expression Function (or a metavariable that might later be instantiated as one) and x and y are any other Expressions (let's just say the symbols "x" and "y" for this example) then newEFA(F,x,y) will be the Expression ("LDE EFA" F x y).

If the first argument is a metavariable then there must be one or more additional arguments of any type. If the first argument is an Expression Function (as per isAnEF()) then there must be a number of arguments following it that are equal to its arity. If these rules are not followed, an error is thrown.

Get the list of parameters for a given expression function. If ef is not an expression function (as judged by isAnEF()) then an error is thrown. Otherwise, an array of its parameters is returned, the exact descendants that are Symbol instances.

Create an expression function (as defined here) that returns one of its arguments. That is, the function can be expressed as $\lambda v_1,\ldots,v_n. v_i$ for some $i$ between 1 and $n$.