Lurch Deductive Engine

Class

Solution

A Solution is a set of Substitutions, together with some other data that helps apply them efficiently. It can be applied to a LogicConcept, which means that it will apply all of its Substitutions simultaneously to that LogicConcept.

A Solution is so named because it can be used to store the solution for a matching Problem. Hence the Problem class provides methods for computing sets of Solutions, and the constructor for this class expects a given Problem, from which it computes and caches information that will improve its own efficiency. See the methods below for details.

Constructor

new Solution(problem, skip)

Construct an empty Solution object for the given problem. Extend it later with the add() or plus() method.

Parameters

  • problem Problem

    the problem for which the contructed object is to be the solution. The newly constructed object is not yet a solution to the given problem, but caches the problem's metavariables and Expression Function Applications, so that it is prepared to grow into a solution for it later.

  • skip boolean false

    Clients should not use this parameter; it is for internal use only, to make copying Solution objects more efficient.

See

Source

Classes

Solution

Methods

add(sub, check)

Add a new Substitution to this object. (Recall from the definition of this class that it functions as a set of Substitutions.) Or, if the Substitution fails, throw an error instead.

The function can fail if the Substitution's metavariable already appears in the given Solution, but mapped to a different Expression. This fails because a Substitution is a function, and so it cannot map the same input to more than one output. This comparison is done modulo de Bruijn attributes.

This also includes applying the given Substitution to the contents of this object before inserting the given Substitution object into this one.

Parameters

  • sub Substitution

    the substitution to add

  • check boolean true

    whether to check whether substitution can be added (the default) or not to check and just trust the caller, thus not throwing an error

Source

complete() → {boolean}

A Solution is complete if all of the metavariables appearing in the original Problem (from which the Solution was constructed) have assignments in this solution, and those assignments do not include any metavariables. If a solution is complete, it could be applied to the original problem's patterns to produce expressions containing no metavariables.

Returns

  • boolean

    whether this Solution is complete, as defined above

Source

copy()

Create a copy of this object. It is not strictly a shallow copy or a deep copy; it has the following properties.

  • It keeps the same Substitution instances internally, since these are typically immutable objects anyway, but it creates its own set of those instances, so that adding or removing entries changes only the copy.
  • It uses the same metavariable and bound metavariable sets as in the original object, because those members do not change throughout the lifetime of a Solution.

Source

domain() → {Set}

A Solution can be viewed as a partial function from metavariables to expressions. That is, it is a finite set $\{(m_1,e_1),\ldots,(m_n,e_n)\}$, where each $m_i$ is a metavariable and each $e_i$ is an expression, and the Solution maps each $m_i$ to its corresponding $e_i$. In such a case, the domain of the Solution is the set $\{m_1,\ldots,m_n\}$ of metavariables that are in the mapping.

See

Returns

  • Set

    the set of metavariables in the domain of this Solution, when it is viewed as a partial function from metavariables to expressions; the set contains the name of each metavariable as a string, not as a Symbol instance

Source

equals(other) → {boolean}

Two Solutions are equal if they have the same domain() and, for each metavariable in that domain, they map the metavariable to Substitution instances that are $\alpha$-equivalent.

Parameters

  • other Solution

    the Solution with which to compare this one

Returns

  • boolean

    whether the two Solutions are equal, as defined above

Source

get(metavariable) → {Expression|undefined}

Look up the Expression to which this Solution maps the given metavariable, and return it (or undefined if there isn't one). Recall that Solutions function as sets of Substitutions, that is, as a set of ordered pairs, and thus as a (partial) function. This method is therefore just (partial) function application.

Parameters

  • metavariable Symbol | String

    a metavariable (or just the name of a metavariable) to be looked up in this Solution

Returns

  • Expression undefined

    the Expression to which this Solution maps the given metavariable, or undefined if this solution does not map the metavariable to any Expression

Source

plus(sub, check) → {Solution}

One common workflow will be to extend a solution by first making a copy (using the copy() function) and then adding a new Substitution to it (using the add() function). This function makes that easier by making it possible to do it with just one function call. If S is a Solution, then S.plus(sub) is a copy of S, but after S.add(sub) has been called on it.

Note that if the Substitution cannot be added, this routine will throw an error, so you may wish to use try/catch.

Parameters

  • sub Substitution

    the substitution to add

  • check boolean true

    functions the same as it does in add()

Returns

  • Solution

    a copy() of this object, but with sub added, via a call to add()

Source

restrict()

Alter this object by removing any internal Substitution whose metavariable does not appear in the original Problem from which this Solution was constructed.

This is useful because some intermediate computations en route to a complete solution sometimes add new metavariables, but they should not be part of the final solution, since they were only part of the solving process, not the actual solution.

See

  • domain()
  • restricted()

Source

toString() → {string}

The string representation of a Solution is simply the comma-separated list of string representations of its Substitutions, surrounded by curly brackets to suggest a set. For example, it might be "{(A,(- x)),(B,(+ 1 t))}" or "{}".

See

Returns

  • string

    a string representation of the Solution, useful in debugging

Source