Lurch Deductive Engine

source

matching/solution.js


import { Symbol as LurchSymbol } from "../symbol.js"
import { metavariable, metavariableNamesIn } from "./metavariables.js"
import { Substitution } from "./substitution.js"
import { Problem } from "./problem.js"
import {
    fullBetaReduce, alphaEquivalent, isAnEFA
} from './expression-functions.js'
import { equal as deBruijnEquals } from './de-bruijn.js'

/**
 * A Solution is a set of {@link Substitution Substitutions}, together with
 * some other data that helps apply them efficiently.  It can be applied to a
 * {@link LogicConcept LogicConcept}, which means that it will apply all of
 * its {@link Substitution Substitutions} simultaneously to that
 * {@link LogicConcept LogicConcept}.
 * 
 * A Solution is so named because it can be used to store the solution for a
 * matching {@link Problem Problem}.  Hence the {@link Problem Problem} class
 * provides methods for computing sets of Solutions, and the constructor for
 * this class expects a given {@link Problem Problem}, from which it computes
 * and caches information that will improve its own efficiency.  See the
 * methods below for details.
 */
export class Solution {

    /**
     * Construct an empty Solution object for the given `problem`.  Extend it
     * later with the {@link Solution#add add()} or
     * {@link Solution#plus plus()} method.
     * 
     * @param {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
     *   {@link module:Metavariables.metavariable metavariables} and Expression
     *   Function Applications, so that it is prepared to grow into a solution
     *   for it later.
     * @param {boolean} skip Clients should not use this parameter; it is for
     *   internal use only, to make copying Solution objects more efficient.
     * 
     * @see {@link Solution#add add()}
     * @see {@link Solution#plus plus()}
     */
    constructor ( problem, skip = false ) {
        // Ensure this object is created from a real Problem instance:
        if ( !( problem instanceof Problem ) )
            throw new Error(
                'Solution constructor requires a Problem instance' )
        this._problem = problem

        // Compute data from the problem only if requested to do so:
        if ( !skip ) {
            const pats = problem.constraints.map(
                constraint => constraint.pattern )
            this._metavariables = pats.map( metavariableNamesIn )
                .reduce( ( A, B ) => new Set( [ ...A, ...B ] ), new Set() )
            this._EFAs = pats.map( pattern =>
                pattern.descendantsSatisfying( isAnEFA ) ).flat( 1 )
        }

        // We initialize an empty member here, but it is an important one, so
        // we document its format.  The _substitutions object maps metavariable
        // names to Substitution instances that replace that metavariable.
        // This isn't redundant; it makes for fast lookup.
        this._substitutions = { }
    }

    /**
     * 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 {@link Substitution 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.
     */
    copy () {
        // Pass skip=true to avoid computing data we're about to provide:
        const result = new Solution( this._problem, true )
        // Now provide that data:
        for ( let metavariable in this._substitutions )
            if ( this._substitutions.hasOwnProperty( metavariable ) )
                result._substitutions[metavariable] =
                    this._substitutions[metavariable]
        result._metavariables = this._metavariables
        result._EFAs = this._EFAs
        // Done, return the copy:
        return result
    }

    /**
     * Two Solutions are equal if they have the same
     * {@link Solution#domain domain()} and, for each metavariable in that
     * domain, they map the metavariable to
     * {@link Substitution Substitution} instances that are
     * {@link module:ExpressionFunctions.alphaEquivalent $\alpha$-equivalent}.
     * 
     * @param {Solution} other the Solution with which to compare this one
     * @returns {boolean} whether the two Solutions are equal, as defined above
     */
    equals ( other ) {
        const d1 = Array.from( this.domain() )
        const d2 = other.domain()
        return d1.length == d2.size
            && d1.every( mv => d2.has( mv ) )
            && d1.every( mv =>
                alphaEquivalent( this.get( mv ), other.get( mv ) ) )
    }

    /**
     * Look up the {@link Expression 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
     * {@link Substitution Substitutions}, that is, as a set of ordered pairs,
     * and thus as a (partial) function.  This method is therefore just
     * (partial) function application.
     * 
     * @param {Symbol|String} metavariable a metavariable (or just the name of
     *   a metavariable) to be looked up in this Solution
     * @returns {Expression|undefined} the {@link Expression Expression} to
     *   which this Solution maps the given metavariable, or undefined if this
     *   solution does not map the metavariable to any
     *   {@link Expression Expression}
     */
    get ( metavariable ) {
        if ( metavariable instanceof LurchSymbol )
            metavariable = metavariable.text()
        return this._substitutions.hasOwnProperty( metavariable ) ?
            this._substitutions[metavariable].expression : undefined
    }

    /**
     * This method is designed to support the
     * {@link Substitution#applyTo applyTo()} method in the
     * {@link Substitution Substitution} class.  See the documentation there
     * for details.
     * 
     * @param  {...Substitution} subs a list of substitutions to apply
     * 
     * @see {@link Substitution#applyTo applyTo() in the Substitution class}
     */
    substitute ( ...subs ) {
        subs.forEach( sub => {
            for ( let metavariable in this._substitutions )
                if ( this._substitutions.hasOwnProperty( metavariable ) )
                    this._substitutions[metavariable] =
                        this._substitutions[metavariable].afterSubstituting(
                            sub )
        } )
    }

    /**
     * This method is designed to support the
     * {@link Substitution#appliedTo appliedTo()} method in the
     * {@link Substitution Substitution} class.  See the documentation there
     * for details.
     * 
     * @param  {...Substitution} subs a list of substitutions to apply
     * 
     * @see {@link Substitution#appliedTo appiedTo() in the Substitution class}
     */
    afterSubstituting ( ...subs ) {
        const result = this.copy()
        result.substitute( ...subs )
        return result
    }

    // For internal use.  Applies beta reduction to all the patterns in all the
    // solution's substitutions.
    betaReduce () {
        this.domain().forEach( mv => {
            const sub = this._substitutions[mv]
            const reduced = fullBetaReduce( sub.expression )
            if ( !reduced.equals( sub.expression ) )
                this._substitutions[mv] = new Substitution(
                    new LurchSymbol( mv ).asA( metavariable ), reduced )
        } )
    }

    /**
     * Add a new {@link Substitution Substitution} to this object.  (Recall
     * from the definition of this class that it functions as a set of
     * {@link Substitution Substitutions}.)  Or, if the
     * {@link Substitution Substitution} fails, throw an error instead.
     * 
     * The function can fail if the {@link Substitution}'s metavariable already
     * appears in the given Solution, but mapped to a different
     * {@link Expression}.  This fails because a {@link Substitution} is a
     * function, and so it cannot map the same input to more than one output.
     * This comparison is done {@link module:deBruijn.equal modulo de Bruijn
     * attributes}.
     * 
     * This also includes applying the given {@link Substitution Substitution}
     * to the contents of this object before inserting the given
     * {@link Substitution Substitution} object into this one.
     * 
     * @param {Substitution} sub the substitution to add
     * @param {boolean} check whether to check whether `substitution` can
     *   be added (the default) or not to check and just trust the caller,
     *   thus not throwing an error
     */
    add ( sub, check = true ) {
        // if we're checking to prevent errors, do so now:
        if ( check ) {
            const mvName = sub.metavariable.text()
            const oldValue = this.get( mvName )
            if ( oldValue && !deBruijnEquals( oldValue, sub.expression ) )
                throw new Error(
                    `Function condition failed for metavariable ${mvName}` )
        }
        // modify inner substitutions
        this.substitute( sub )
        this.betaReduce()
        // add the sub to our list
        this._substitutions[sub.metavariable.text()] = sub
    }

    /**
     * One common workflow will be to extend a solution by first making a copy
     * (using the {@link Solution#copy copy()} function) and then adding a new
     * {@link Substitution Substitution} to it (using the
     * {@link Solution#add 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 {@link Substitution Substitution} cannot be added, this
     * routine will throw an error, so you may wish to use `try`/`catch`.
     * 
     * @param {Substitution} sub the substitution to add
     * @param {boolean} check functions the same as it does in
     *   {@link Solution#add add()}
     * @returns {Solution} a {@link Solution#copy copy()} of this object, but
     *   with `sub` added, via a call to {@link Solution#add add()}
     */
    plus ( sub, check = true ) {
        const result = this.copy()
        result.add( sub, check )
        return result
    }

    /**
     * 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.
     * 
     * @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 {@link Symbol Symbol} instance
     *
     * @see {@link Solution#restrict restrict()}
     * @see {@link Solution#restricted restricted()}
     */
    domain () {
        const result = new Set()
        for ( let metavariable in this._substitutions )
            if ( this._substitutions.hasOwnProperty( metavariable ) )
                result.add( metavariable )
        return result
    }

    /**
     * Alter this object by removing any internal
     * {@link Substitution Substitution} whose metavariable does not appear in
     * the original {@link Problem 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 {@link Substitution#domain domain()}
     * @see {@link Substitution#restricted restricted()}
     */
    restrict () {
        for ( let metavariable in this._substitutions )
            if ( this._substitutions.hasOwnProperty( metavariable )
              && !this._metavariables.has( metavariable ) )
                delete this._substitutions[metavariable]
    }

    /**
     * Return a copy of this Solution, but with
     * {@link Substitution#restrict restrict()} having been applied to the
     * copy.
     * 
     * @see {@link Substitution#domain domain()}
     * @see {@link Substitution#restrict restrict()}
     * @see {@link Substitution#copy copy()}
     */
    restricted () {
        const result = this.copy()
        result.restrict()
        return result
    }

    /**
     * A Solution is complete if all of the metavariables appearing in the
     * original {@link Problem 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.
     * 
     * @return {boolean} whether this Solution is complete, as defined above
     */
    complete () {
        const d = this.domain()
        return Array.from( this._metavariables ).every( mv => d.has( mv ) )
            && Array.from( d ).every( mv =>
                this._substitutions[mv].metavariableNames().size == 0 )
    }

    /**
     * The string representation of a Solution is simply the comma-separated
     * list of string representations of its
     * {@link Substitution Substitutions},
     * surrounded by curly brackets to suggest a set.  For example, it might be
     * "{(A,(- x)),(B,(+ 1 t))}" or "{}".
     * 
     * @returns {string} a string representation of the Solution, useful in
     *   debugging
     * 
     * @see {@link Substitution#toString toString() for individual Substitutions}
     */
    toString () {
        const d = Array.from( this.domain() )
        d.sort()
        return `{${d.map(x=>this._substitutions[x].toString()).join(',')}}`
    }

    // for internal use only, by *solutions() member of "friend" class Problem
    deBruijnDecode () {
        for ( let metavariable in this._substitutions )
            if ( this._substitutions.hasOwnProperty( metavariable ) )
                this._substitutions[metavariable].deBruijnDecode()
    }

}