Lurch Deductive Engine

Class

Constraint

A Constraint is a pattern-expression pair often written $(p,e)$ and used to express the idea that the expression $e$ matches the pattern $p$. The $e$ will be an instance of Expression and the $p$ will be as well, but it may contain metavariables, as defined here. For more information on how Constraints fit into the work of matching in general, see the documentation for the matching module.

Note that a Constraint need not be true or satisfiable. Here are three examples using ordinary mathematical notation. For the purposes of these examples, let us assume that capital letter symbols stand for metavariables, and no other symbols are metavariables.

  • The constraint $(3-t,3-t)$ is clearly satisfiable, because its expression already exactly matches its pattern, with no metavariables even coming into play at all.
  • The constraint $(A+B,3x+y^2)$ is satisfiable, because we could instantiate the metavariables with $A\mapsto 3x,B\mapsto y^2$ to demonstrate that $e$ is of the form expressed by $p$.
  • The constraint $(3,\forall x.P(x))$ is not satisfiable, because $p\neq e$ and $p$ contains no metavariables that we might instantiate to change $p$.
  • The constraint $(A+B,\forall x.P(x))$ is not satisfiable, because no possible instantiations of the metavariables $A,B$ can make the summation in $p$ into the universal quantifier in $e$.

Typically Constraints are arranged into sets, and there are algorithms for solving sets of Constraints. See the Problem class for more details.

Constructor

new Constraint(pattern, expression)

Constructs a new Constraint with the given pattern and expression. Throws an error if expression satisfies containsAMetavariable().

Constraints are to be treated as immutable. Do not later alter the pattern or expression of this constraint. If you need a different constraint, simply construct a new one.

Parameters

  • pattern Expression

    any Expression instance, but typically one containing metavariables, to be used as the pattern for this Constraint, as documented at the top of this page

  • expression Expression

    any Expression instance that contains no instance of a metavariable, so that it can be used as the expression for this Constraint

See

Source

Classes

Constraint

Members

expression

Getter for the expression provided at construction time. This function is useful for making the expression member act as a read-only member, even though no member is really read-only in JavaScript.

Source

pattern

Getter for the pattern provided at construction time. This function is useful for making the pattern member act as a read-only member, even though no member is really read-only in JavaScript.

Source

Methods

afterSubstituting(…subs) → {Constraint}

Create a copy of this Constraint, except with the given list of Substitutions applied to it, in the order given. Because Constraint expressions cannot contain metavariables, it is necessary to apply the Substitutions only to the pattern portion of the Constraint. The same expression can be reused.

Parameters

Returns

  • Constraint

    a copy of this Constraint, but with the given Substitutions applied to its pattern

Source

children() → {Constraint}

If a Constraint has complexity() = 3, and thus complexityName() = "children", then the pattern and expression are both Applications and have the same number of children. It is therefore useful when solving this constraint to pair up the corresponding children into new Constraint instances. This function does so, returning them as an array.

For example, if we have a pattern $p=(a~b~c~d)$ and an expression $e=(w~x~y~z)$ then the Constraint $(p,e)$ has complexity 3, and we can call this function on it, yielding three new Constraints, $(a,w)$, $(b,x)$, $(c,y)$ and $(d,z)$.

See

Returns

  • Constraint

    all child constraints computed from this Constraint, as a JavaScript array, in the same order that the children appear in the pattern (and expression) of this constraint

Source

complexity() → {integer}

Compute and return the complexity of this Constraint. The return value is cached, so that future calls to this function do not recompute it. The cache is never invalidated, because Constraints are viewed as immutable. Complexities include:

  • 0, or "failure": any constraint not matching any of the categories listed below, and therefore impossible to reconcile into a solution
  • 1, or "success": any constraint $(p,e)$ for which $p=e$ (and thus $p$ contains no metavariables)
  • 2, or "instantiation": any constraint $(p,e)$ for which $p$ is a lone metavariable, so that the clear unique solution is $p\mapsto e$
  • 3, or "children": any constraint $(p,e)$ where $p$ and $e$ are both compound expressions with the same structure, so that the appropriate next step en route to a solution is to pair up their corresponding children and see if a solution exists to that Constraint set
  • 4, or "EFA": any constraint $(p,e)$ where $p$ is an Expression Function Application, as defined in the documentation for the ExpressionFunctions namespace

This value can be used to sort Constraints so that constraints with lower complexity are processed first in algorithms, for the sake of efficiency. For example, the Problem class has algorithms that make use of this function.

See

Returns

  • integer

    the complexity of this Constraint, ranked on a scale beginning with zero (trivial) and counting upwards towards more complex constraints

Source

complexityName() → {string}

This function returns a single-word description of the complexity() of this Constraint. It is mostly useful in debugging. The names listed after each integer in the documentation for the complexity() function are the names returned by this function.

See

Returns

  • string

    a description of this Constraint's complexity

Source

copy() → {Constraint}

Creates a copy of this Constraint. It is a shallow copy, in the sense that it shares the same pattern and expression instances with this Constraint, but that should be irrelevant, because Constraints are immutable. That is, they never alter their own patterns or expressions, and the client is instructed not to alter them either, as per the documentation in the constructor.

Returns

  • Constraint

    a copy of this Constraint

Source

deBruijnDecode()

Apply the de Bruijn decoding to the pattern and the expression in this Constraint, in place.

This function should be applied only to a Constraint that has been de Bruijn encoded first, because even though it is possible to call this function on any Consraint, one should think of the set of ordinary MathConcepts as distinct from the set of de Bruijn-encoded ones, and this function maps the latter set to the former, but does not map the former anywhere.

See

Source

deBruijnEncode()

Apply the de Bruijn encoding to the pattern and the expression in this Constraint, in place.

This function should be applied only once to any given Constraint, because even though it is possible to do it more than once, one should think of the set of ordinary MathConcepts as distinct from the set of de Bruijn-encoded ones, and this function maps the former set to the latter, but does not map the latter anywhere.

See

Source

equals(other) → {boolean}

Two Constraints are equal if they have the same pattern and the same expression. Comparison of patterns and expressions is done using the equals() member of the MathConcept class.

Parameters

  • other Constraint

    another instance of this class, to be compared with this one for equality

Returns

  • boolean

    whether the two instances are structurally equal

Source

isAnInstantiation() → {boolean}

If a Constraint's pattern is a single metavariable, then that Constraint can be used as a tool for substitution. For instance, the Constraint $(A,2)$ can be applied to the expression $A-\frac{A}{B}$ to yield $2-\frac{2}{B}$. A Constraint is only useful for application if its pattern is a single metavariable. This function tests whether that is the case.

See

  • applyTo()
  • appliedTo()

Returns

  • boolean

    true if and only if this Constraint can be applied like a function (that is, whether its pattern is just a single metavariable)

Source

toString() → {string}

The string representation of a Constraint $(p,e)$ is simply the string "(P,E)" where P is the putdown representation of $p$ and E is the putdown representation of $e$.

It also replaces the overly wordy JSON notation for metavariables with a double-underscore, just to increase brevity and clarity when debugging.

Returns

  • string

    a string representation of the Constraint, useful in debugging

Source