Lurch Deductive Engine

Class

Substitution

A substitution is a metavariable-expression pair $(m,e)$ that can be used for substitution in other expressions. (See also the definitions of metavariable and Expression.)

For example, if $x$ is a metavariable and $(x,2k-1)$ is a substitution, then if we consider the expression $x^2+px$, applying the substitution would yield the expression $(2k-1)^2+p(2k-1)$.

Constructor

new Substitution()

Constructs a new Substitution instance from a variety of types of inputs. See the documentation at the top of this class for the explanation of how a Substitution instance is a metavariable-expression pair $(m,e)$.

  • If two inputs are given, a metavariable $m$ and an expression $e$, construct a Substitution from the pair $(m,e)$.
  • If one input is given, a Constraint, and that constraint passes the isAnInstantiation() test, then it can be interpreted as a Substitution. The constraint $(p,e)$ is such that $p$ is a metavariable, and thus if we let $m=p$, we have a substitution $(m,e)$.
  • In all other cases, throw an error, because the cases above are the only supported cases.

See

Source

Classes

Substitution

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

metavariable

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

Source

Methods

afterSubstituting(…subs) → {Substitution}

This function operates just as substitute() does, but rather than altering this object in place, it makes a copy, alters the copy, and returns that copy.

Parameters

  • subs Substitution <repeatable>

    the list of Substitutions to apply to this Substitution's expression, in the order given

See

  • substitute()

Returns

  • Substitution

    a copy of this Substitution, but with the replacements made

Source

appliedTo(target) → {any}

Apply this Substitution to the given target, returning the result as a new instance (not altering the original).

If the target is a LogicConcept, this is identical to making a copy of target and then calling applyTo() on it, except for one case: If the target is equal to the metavariable of this Substitution, and has no parent, then applyTo() will have no effect, but this routine will return a copy of the Substitution's expression, as expected.

If the target is not a LogicConcept, but it implements the afterSubstituting() method, then that method is called with this Substitution as argument, and its result returned. In particular, this class itself implements an afterSubstituting() method, so one can apply Substitutions to other Substitutions.

No other options are supported, and will return an error.

Parameters

  • target

    the object to which we should apply this Substitution, resulting in a copy

See

Returns

  • any

    a new copy of the target with the application of this Substitution having been done

Source

applyTo(target)

Apply this Substitution to the given target, in place.

  • If the target is a LogicConcept, find all subexpressions of it that are structurally equal to the metavariable of this Substitution, and replace all of them simultaneously with the expression of this Substitution. (All the documentation after this bulleted list is for this case.)
  • If the target is any other type of object that has a substitute method, call that method, passing this Substitution object as an argument, and let the target handle the details. In particular, this class itself implements a substitute() method, so Substitutions can be applied to one another.
  • No other cases are supported, and will throw errors.

The word "simultaneously" is important because if the expression that is inserted as part of the replacement contains any metavariables, they will not be considered for substitution.

Note that there is one case in which this may fail to produce the desired results: If the target is itself a copy of this Substitution's metavariable, and has no parent, then it cannot be replaced in-place, due to the nature of the MathConcept replacement API. If such a case may occur, you may prefer to use the appliedTo() function instead.

Parameters

  • target

    the target to which we should apply this Substitution, in place

See

Source

copy() → {Substitution}

Creates a deep copy of this Substitution, that is, its metavariable and expression are copies of the ones in this object.

Returns

  • Substitution

    a deep copy of this Substitution

Source

equals(other) → {boolean}

Two Substitutions are equal if they have the same metavariable and the same expression. Comparison of metavariables and expressions is done using the equals() member of the MathConcept class.

Parameters

  • other Substitution

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

Returns

  • boolean

    whether the two instances are structurally equal

Source

metavariableNames() → {Set}

Get the set of names of metavariables that appear anywhere in the expression of this substitution. Caches the result so that once it is computed, this is fast to compute again.

Returns

  • Set

    a Set of strings, equal to the names of all metavariables appearing in the expression of this substitution

Source

substitute(…subs)

Apply a sequence of Substitution instances, in the order given, to the expression of this Substitution instance, in place.

For example, if S1 is a Substitution mapping the metavariable $M$ to the expression $f(x,Y)$, where $Y$ was another metavariable, and S2 is the substitution mapping $Y$ to $5$, then S1.substitute(S2) would alter S1 in place so that it mapped $M$ to $f(x,5)$.

S.substitute(X1,...,Xn) is equivalent to S.substitute(X1) and then S.substitute(X2) and so forth, in that order. It is also equivalent to X1.applyTo(S) and then X2.applyTo(S) and so forth, in that order.

Parameters

  • subs Substitution <repeatable>

    the list of Substitutions to apply to this Substitution's expression, in the order given

See

  • applyTo()
  • afterSubstituting()

Source

toString() → {string}

The string representation of a Substitution $(m,e)$ is simply the string "(M,E)" where M is the putdown representation of $m$ and E is the putdown representation of $e$.

This function also improves brevity and clarity when debugging by making a few text replacements, as follows:

  • The JSON notation for the metavariable attribute is replaced with a double underscore, so rather than seeing 'P +{"_type_LDE MV":true}', you will see simply P__.
  • The binder for expression functions, "LDE lambda", is replaced with the more compact and intuitive 𝝺.
  • The symbol for expression function application, "LDE EFA", is replaced with the more compact @, which can be read as shorthand for "apply."

Returns

  • string

    a string representation of the Substitution, useful in debugging

Source