Global

Members

(constant) CASES

Source:

(constant) getAPI

Get the API stored in the global variable in this module, as set by setAPI().
Source:

(constant) setAPI

Provide an API by which this module can deal with expressions. More needs to be documented about this; the only existing API is the OpenMath API. See openmath-api.js for details.
Source:

Methods

alphaConvert(binding, which_var, replace_var)

Takes a binding, a bound variable in that binding, and a replacement variable. Returns the result of replacing (without capture) all instances of the bound variable with the replacement variable.
Parameters:
Name Type Description
binding OM an OM binding
which_var OM the bound variable to replace
replace_var OM the replacement variable
Source:
Returns:
a copy of the alpha converted binding

alphaEquivalent(expr1, expr2)

Checks if two expressions are alpha equivalent. Two expressions are alpha equivalent if one can be transformed into the other by the renaming of bound variables. If called when neither expr1 nor expr2 are applications or bindings, this function returns false because alpha equivalence is not defined for free variables or constants.
Parameters:
Name Type Description
expr1 OM an OM expression (must be application or binding on first call)
expr2 OM an OM expression (must be application or binding on first call)gef
Source:
Returns:
true if the two expressions are alpha equivalent, false otherwise

applyExpressionFunctionApplication(EFA)

If canApplyExpressionFunctionApplication is true, returns the beta reduction of the EF and the arguments it is applied to.
Parameters:
Name Type Description
EFA OM an expression function application
Source:

betaReduce(EF, expr_list)

Takes an expression function representing λv_1,...,v_k.B and a list of expressions e_1,...,e_k and returns the beta reduction of ((λv_1,...,v_k.B)(e_1,...,e_k)) which is the expression B with all v_i replaced by the corresponding e_i. This beta reduction is capture avoiding. See replaceWithoutCapture for details.
Parameters:
Name Type Description
EF OM an expression function with n variables
expr_list Array.<OM> a list of expressions of length n
Source:
Returns:
an expression manipulated as described above

canApplyExpressionFunctionApplication(EFA)

Tests whether an EFA is of the form EF(args). If the EFA is of this form, applyExpressionFunctionApplication can be called with this EFA as an argument.
Parameters:
Name Type Description
EFA OM an expression function application
Source:

checkVariable(variable, nextNewVariableIndex)

Helper function used when adding pairs to a constraint list. Takes a variable and checks if it of the form, vX where X is some number. If it is of this form, it returns X + 1 if it is greater than the given index.
Parameters:
Name Type Description
variable OM the variable to be checked
nextNewVariableIndex Number the number to check against
Source:

getExpressionArgumentsFromApplication(EFA)

If this is an EFA, extract and return the array of arguments to which the function is to be applied. Otherwise return null.
Parameters:
Name Type Description
EFA OM an expression function application
Source:

getExpressionFunctionFromApplication(EFA)

If this is an EFA, extract and return the expression function application that is to be applied. Otherwise return null.
Parameters:
Name Type Description
EFA OM an expression function application
Source:

getNewVariableRelativeTo(expr)

Helper function for other expression manipulation functions.
Parameters:
Name Type Description
expr OM an OM expression, more expr arguments are accepted.
Source:
Returns:
the first variable of the form xN which appears nowhere in the supplied expression(s).

isExpressionFunction(expression)

Tests whether an expression is an expression function.
Parameters:
Name Type Description
expression OM the expression to be checked
Source:

isExpressionFunctionApplication()

Source:
Returns:
true if the supplied expression is an EFA

isFree(expr)

Is the given expression free in its topmost ancestor? That is, are all variables free within this expression still free within that topmost ancestor?
Parameters:
Name Type Description
expr OM the expression to test
Source:

makeConstantExpression(new_variable, expression)

Takes a new variable (relative to some constraint list) and an expression and returns an EF which has the meaning λv_n.expr where v_n is the new variable and expr is the expression. I.e. creates a constant expression function.
Parameters:
Name Type Description
new_variable OM an OM variable
expression OM an OM expression
Source:

makeExpressionFunction(variables, body)

Makes a new expression function with the meaning λv1,...,vk.B where v1,...,vk are the variables and B is any OM expression.
Parameters:
Name Type Description
variables Array.<OM> a list of OM variables
body OM any OM expression
Source:

makeExpressionFunctionApplication(func, arguments)

Makes a new expression function application with the meaning F(arg) where F is either an expression function (EF), or a metavariable which is expected to be replaced by an EF. In the case that F is an EF, the expression function can be applied to the argument see applyExpressionFunctionApplication.
Parameters:
Name Type Description
func OM either an EF or something which can be instantiated as an EF.
arguments Array.<OM> a list of OM expressions
Source:

makeImitationExpression(variables, expr)

Takes a list of variables, denoted v1,...,vk, an expression which is denoted g(e1,...,em), and a list of temporary metavariables. For an application, returns an EF with the meaning λv_1,...,v_k.g(H_1(v_1,...,v_k),...,H_m(v_1,...,v_k)) where each H_i denotes a temporary EFA as well as a list of the newly created temporary metavariables [H_1,...,H_m]. I.e. it returns an 'imitation' expression function where the body is the original expression with each argument replaced by a temporary EFA.
Parameters:
Name Type Description
variables OM a list of OM variables
expr OM an OM application
Source:
Returns:
an EF which is the imitation expression described above

makeProjectionExpression(variables, point)

Takes a list of variables v_1,...,v_k and a single variable (a point) v_i and returns an EF with the meaning λv_1,...,v_k.v_i. I.e. returns a projection expression function for v_i with k arguments.
Parameters:
Name Type Description
variables Array.<OM> a list of OM variables
point OM a single OM variable
Source:

occursFree(inner, outer)

Return true iff an instance (i.e., copy) of the inner expression occurs in the outer expression and that occurrence is free (not just in outer, but absolutely)
Parameters:
Name Type Description
inner OM the expression to seek a free occurrence of
outer OM the expression in which to search
Source:

replace(toReplace, withThis)

The API provides a function for replacing an expression, wherever it sits in its parent tree, with another expression. But the behavior can vary from one API implementation to another: Does the function return the replaced expression, the replacement, or neither? Does the variable that referred to the replaced expression now refer to the replacement, or not? We standardize that here by creating this wrapper, which always returns the replacement, and can thus be used to update variables if needed.
Parameters:
Name Type Description
toReplace OM The expression to be replaced
withThis OM The expression with which to replace it
Source:

replaceWithoutCapture(expr, variable, replacement)

Takes an expression, a variable, and a replacement expression. Manipulates the expression in place in order to replace all occurences of the variable with the expression in such a way that variable capture will not occur. Because this function will be called whenever a metavariable's instantiation is discovered by the solve() routine in MatchingChallenge, it must guarantee that NO occurrences of the variable remain after the function is complete. Note that this function addresses only variable capture that would occur from a binding expression inside expr; it does not address any binders that may sit in a parent above expr.
Parameters:
Name Type Description
expr OM an OM expression
variable OM an OM variable
replacement OM an OM expression
Source: