Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://lurchmath.github.io/second-order-matching/docs/OpenMathAPI.html below:

JSDoc: Namespace: OpenMathAPI

This namespace creates an API by which this package can use a simple JavaScript implementation of OpenMath to store and manipulate mathematical expressions.

As documented on the main page, it is not necessary for you to use OpenMath. If you have your own class, you can create an object that wraps your expression class in an API spoken by this module, so that you need not convert your custom expression types to/from OpenMath.

To do so, create a single object that maps names of functions in this module's API to their implementations using your custom expression class. To see how to get started, and how to connect the resulting object to this module, see the second code example on the main page of this documentation.

Every function documented below is explained in two ways: First, the general requirement of that element of the API is described without reference to OpenMath specifically, so that those who are reading this for the purposes of writing their own expression API have that information in general terms. Secondly, the specifics of the OpenMath implementation in this file is described.

To enable you to write an API like the one below, your custom expression class must have the following features.

• It must be a hierarchical structure (as in filterSubexpressions) of objects that can be variables (or at least identifiers more broadly), function applications, bindings (that is, the application of quantifiers or quantifier-like symbols), and optionally other atomic expressions as well.
• It must be possible to tell when an instance is each of these things, so that you can write the essential functions isVariable, isApplication, and isBinding.
• It must be possible to construct instances of each type, so that you can write the essential functions variable, application, and binding.
• It must be possible to mark a variable with the "is a metavariable" boolean flag. If your expression class does not support attributes on expressions, you can do this using, for example, a prefix used only internally, as in the previous point. See the documentation for setMetavariable for more specifics on this idea. This enables you to write isMetavariable, setMetavariable, and clearMetavariable.
• It must be possible to query the essential details of each type of expression:
  • For a variable, you must be able to write getVariableName.
  • For an application, you must be able to write getChildren. This treates the function application like a LISP S-expression. For example, 3+5 would be seen as (+ 3 5) and should therefore return three children.
  • For a binding, you must be able to write bindingHead (the quantifier or other head symbol), bindingVariables (the array of bound variables), bindingBody (the body inside the expression). For example, in the expression "for all x and y, x+y=y+x," the head is the universal quantifier (the "for all" symbol), the bound variables are x and y, and the body is the expression x+y=y+x.
• You must be able to write a function that checks whether a given instance of a given variable appears free in an ancestor expression. This should be do-able if your expression class can do all of the above things. See the documentation for variableIsFree for details.
• You must provide an expression (typically an atomic, like a symbol or variable) that will be used as the operator for metalinguistic expressions. (Such expressions arise when we write things like P(x) not as an expression in the language itself, but to mean the computation of an expression in the language by substituting x into a function P that generates expressions.) You can use any expression that will not be appearing naturally in any matching problem you provide to this package, so that there will be no confusion or ambiguity. An unusual symbol is sufficient, such as one named "_expression_function" or something equally unlikely to occur elsewhere.

Source:

• openmath-api.js, line 11

The application function should construct a function application expression whose children are in the array passed as the one parameter to this function. The first child is the operator and the rest are its operands, as in an a LISP S-expression, such as (* 3 5) for "3 times 5." The exact objects in the list given should be used; this function should not make copies.

The OpenMath implementation uses a constructor with a similar purpose that is built into the OpenMath module.

Source:

• openmath-api.js, line 284

The binding function should construct a binding expression whose head is the given symbol (typically the quantifier if that's what type of expression it is), whose bound variables are in the array given as the second parameter, and whose body is the third expression given. For example, to construct the expression "for all x, P" (for any expression P), pass three arguments: The "for all" symbol, the JavaScript array containing just the variable expression x, and finally the expression P. The exact objects in the arguments should be used; this function should not make copies.

The OpenMath implementation uses a constructor with a similar purpose that is built into the OpenMath module.

Source:

• openmath-api.js, line 344

The bindingBody function is typically called with a binding expression, as one might construct using the binding function. This function should return its body, that is, the last argument given to the binding constructor, which is typically the main expression in the binding. The original body expression must be returned, not a copy. If the given expression does not pass the isBinding check, this function should return null.

The OpenMath implementation stores the body internally, so we can simply return that here.

Source:

• openmath-api.js, line 405

The bindingHead function will typically be called with a binding expression, as one might construct using the binding function. This function should return its head symbol, that is, the first argument given to the binding constructor, which is typically the quantifier (if the expression is a quantification). The original symbol must be returned, not a copy. If the given expression does not pass the isBinding check, this function should return null.

The OpenMath implementation stores the symbol internally, so we can simply return that here.

Source:

• openmath-api.js, line 364

The bindingVariables function is typically called with a binding expression, as one might construct using the binding function. This function should return all of its bound variables, that is, the array passed as second parameter to the binding constructor. The exact objects must be returned, not copies, and they should be in a JavaScript array. If the given expression does not pass the isBinding check, this function should return null.

The OpenMath implementation stores the bound variables in an array internally, so we can simply return that array here. Although we could slice it to ensure it will not get corrupted, the other code in this module does not alter bound variable arrays that it has queried from expressions, so this implementation is safe for our purposes.

Source:

• openmath-api.js, line 383

The clearMetavariable function removes the attribute or mark set in setMetavariable, if indeed such an attribute exists on the given expression. This should restore the variable to its original condition.

The OpenMath implementation removes any attribute with the same key used in setMetavariable.

Source:

• openmath-api.js, line 506

The copy function must create a deep copy of an expression and return the new copy.

The OpenMath library provides a copy function that we use here.

Source:

• openmath-api.js, line 144

The equal function computes deep structural equality, which can be true even if the two objects are not the same in memory. Any two expressions that have the same hierarchical structure should be considered equal.

The OpenMath library provides a structural equality function, and we defer to that.

Source:

• openmath-api.js, line 155

The getChildren function can expect that the input object is a function application expression, as one might construct using the application function. This function should return all of its children, that is, the array passed to the application constructor, in the same order (operator first, operands in order thereafter). The exact children must be returned, not copies, and they should be in a JavaScript array. If the given expression does not pass the isApplication check, this function should return an empty array.

The OpenMath implementation stores the children in an array internally, so we can simply return that array here. Although we could slice it to ensure it will not get corrupted, the other code in this module does not alter child arrays that it has queried from expressions, so this implementation is safe for our purposes.

Source:

• openmath-api.js, line 300

The getVariableName function must return, as a string, the name of the variable stored in the given expression. If the given expression does not pass the isVariable check, this function should return null.

The OpenMath implementation uses the built-in .name attribute of OpenMath variable instances.

Source:

• openmath-api.js, line 207

Helper function used when adding pairs to a constraint list. Returns the list of variables that appear in a given expression.

Source:

• language.js, line 170

a list containing any variables in the given expression

The isApplication function should return true if and only if the given expression is a function application. This excludes other compound expression types, particularly binding expressions (that is, applications of quantifiers).

The OpenMath implementation relies on the fact that "application" is a built-in OpenMath type.

Source:

• openmath-api.js, line 271

The isBinding function should return true if and only if the given expression is a binding expression, that is, the application of a quantifier, such as "there exists x such that x-1=0". This excludes other compound expression types, particularly function application (that is, where no dummy variables are used/bound, like the x in the example just given).

The OpenMath implementation relies on the fact that "binding" is a built-in OpenMath type.

Source:

• openmath-api.js, line 329

The isExpression function must return true if and only if the one input is an instance of the class of expressions.

In the OpenMath case, we provide a function that returns true if and only if the given object is an OpenMath expression.

Source:

• openmath-api.js, line 99

The isMetavariable function returns true if and only if the given argument is a variable or symbol and the attribute or mark described in setMetavariable is present on it.

The OpenMath implementation checks whether there is an attribute with the same key-value pair used in setMetavariable.

Source:

• openmath-api.js, line 489

The isVariable function must return true if and only if the given expression is a variable. That is, the expression class for which we are defining an API must have a notion of variable (or at least "identifier") and this function must return true if and only if the given expression is that kind.

The OpenMath implementation here looks up the OpenMath type and checks to see if it is the "variable" type defined in the OpenMath standard.

Source:

• openmath-api.js, line 192

The replace function should find where its first argument sits inside any parent structure, remove it from that location, and then place the second parameter in that place instead. No specific return value is required. If the first parameter does not have a parent, this function is permitted to do nothing.

The OpenMath library has a function that does this. While it also updates the internal references of the parameters, this extra behavior does not harm the results of this function.

Source:

• openmath-api.js, line 169

The sameType function must return true if and only if two expressions have the same type. This does not require an expression class to have an extensive type system, but it must at least distinguish three broad types of expressions: atomic expressions must be different from function applications, which are both different from bindings (that is, the application of a quantifier or other binding symbol, such as a summation or integral). Any type system that is at least as granular as this basic minimum is sufficient.

Here we simply look up the OpenMath type of each object and compare them, because OpenMath has types for application, binding, and several different types of atomic expressions (among other things).

Source:

• openmath-api.js, line 125

The setMetavariable function takes an expression as input. If it is not a variable or symbol, this function does nothing. But if it is, then this function adds to it an attribute (or any kind of mark) that will distinguish the variable as a metavariable. Note these important attributes of this mark:

1. It affects only this instance of the variable. Other variables with the same name are not marked.
2. It affects copies made later of this instance. That is, copying this instance should copy the mark as well.
3. A test of equality between two variables of the same name, but one being a metavariable and the other not, should yield a false result (not equal). But two non-metavariables with the same name are equal, as are two metavariables with the same name.

The purpose of metavariables need not be documented here, but briefly, they are used when pattern matching, to distinguish a variable that can match against any expression from a variable that can match only other instances of itself.

If your expression class doesn't support adding attributes to expressions, you could use prefixes or suffixes to distinguish metavariables from non-metavariables.

The OpenMath implementation uses the fact that OpenMath expressions can be decorated with an arbitrary number of attributes. We use one whose key is a special symbol defined earlier and whose value is the constant "true."

Source:

• openmath-api.js, line 452

The variable function constructs an instance of your expression class that is a variable with the given name.

The OpenMath implementation uses a constructor with a similar purpose that is built into the OpenMath module.

Source:

• openmath-api.js, line 221

The variableIsFree function will be called with a variable expression as the first argument and some other expression as its second argument. (If the second argument is null or omitted, the topmost ancestor should be treated as the default value.) It should return true if and only if the variable (not a copy of the variable, but the given instance) appears in the given expression, not within the scope of a binding expression that binds the variable (that is, whose list of bound variables includes a variable of the same name).

The OpenMath implementation has a more general isFree function that works for variables or larger expressions, and we can simply defer to that.

Source:

• openmath-api.js, line 425

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4