Lurch core classes

source

validation/propositional-form.js


import CNFTools from './conjunctive-normal-form.js'
import { Environment } from '../environment.js'
import { LogicConcept } from '../logic-concept.js'

/**
 * Any {@link LogicConcept LogicConcept} can be interpreted as a proposition,
 * in the usual sense of propositional logic, as follows.
 * 
 *  * An {@link Expression Expression} (no matter how complex) is treated as
 *    atomic, and considered equal only to another expression with the exact
 *    same structure.
 *  * An {@link Environment Environment} containing no children is treated as
 *    the constant "true."
 *  * An {@link Environment Environment} containing exactly one child is
 *    treated the same as if it were just the child alone.
 *  * An {@link Environment Environment} containing two claim children is
 *    treated as the conjunction of those children, after viewing each as a
 *    proposition itself.
 *  * An {@link Environment Environment} containing a given $G$ followed by a
 *    claim $C$ is treated as the conditional expression "$G$ implies $C$."
 *  * An {@link Environment Environment} with more than two children, $C_1$
 *    through $C_n$, is viewed as if it contained only two children, first
 *    $C_1$ and then an environment containing $C_2$ through $C_n$.
 * 
 * For example, if we use {@link LogicConcept.fromPutdown putdown notation} to
 * express environments and expressions, then the {@link LogicConcept
 * LogicConcept} written as
 * ```
 * {
 *     :(> x 5)
 *     (> y 10)
 *     (= z 15)
 * }
 * ```
 * might correspond to the proposition $P\Rightarrow(Q\wedge R)$, if $P$, $Q$,
 * and $R$ were the propositional letters for the three expressions, in that
 * order.
 * 
 * This conversion preserves the intended meaning of the notions of
 * {@link Environment Environment} and given/claim.  Although
 * {@link LogicConcept LogicConcepts} can be more complex than that (including
 * declared variables, quantifiers, etc.), there are ways to reduce that
 * complexity to propositional form.  Once a {@link LogicConcept LogicConcept}
 * is in propositional form, it can be checked using a propositional tautology
 * checker, either intuitionistic or classical.
 * 
 * We will later add the preprocessing steps that can simplify variable and
 * constant declarations down into content amenable to propositional checking.
 * Those tools are not yet present in this version of the class.
 */
export class PropositionalForm {

    // Clients should not construct PropositionalForm instances themselves;
    // use one of the static builder functions documented below.
    constructor ( catalog ) {
        this._children = [ ]
        this._catalog = catalog || [ ]
    }

    /**
     * Construct a new instance of the PropositionalForm class, an atomic one
     * representing the logical constant "true."  Note that this is not a
     * member function, but a static method, so you would invoke it using
     * `PropositionalForm.constantTrue()`.  In fact, one does not ever
     * construct instances of the PropositionalForm class in any way other
     * than using the static methods of this class that create specific types
     * of PropositionalForms.
     * 
     * @returns {PropositionalForm} a PropositionalForm object representing
     *   the logical constant "true"
     * 
     * @see {@link PropositionalForm#isConstantTrue isConstantTrue()}
     * @see {@link PropositionalForm.atomic atomic()}
     * @see {@link PropositionalForm.conditional conditional()}
     */
    static constantTrue () {
        const result = new PropositionalForm()
        result.text = ' ' // not a possible .toPutdown() result
        return result
    }

    /**
     * Check whether this instance of the PropositionalForm class is an atomic
     * one representing the logical constant "true."  You can create such an
     * instance using the static member function
     * {@link PropositionalForm.constantTrue constantTrue()}.  Note that if
     * this function returns true, then
     * {@link PropositionalForm#isAtomic isAtomic()} will also return true.
     * 
     * @returns {boolean} whether this instance represents the constant "true"
     * 
     * @see {@link PropositionalForm.constantTrue constantTrue()}
     * @see {@link PropositionalForm#isAtomic isAtomic()}
     */
    isConstantTrue () { return this.text == ' ' }

    /**
     * Construct a new instance of the PropositionalForm class, an atomic one
     * representing the given {@link LogicConcept LogicConcept}.  Note that
     * this is not a member function, but a static method, so you would invoke
     * it using `PropositionalForm.atomic(L,c)`.  In fact, one does not ever
     * construct instances of the PropositionalForm class in any way other
     * than using the static methods of this class that create specific types
     * of PropositionalForms.
     * 
     * Note that every {@link LogicConcept LogicConcept} gets represented by a
     * different propositional letter.  The internal structure of the
     * {@link LogicConcept LogicConcept} is completely lost in this
     * conversion.  The second parameter is for internal use, to ensure that
     * the same {@link LogicConcept LogicConcept} gets converted the same way
     * each time.
     * 
     * @param {LogicConcept} LC the {@link LogicConcept LogicConcept} to
     *   represent in propositional form
     * @param {Array} [catalog] a list of the text representations of previous
     *   {@link LogicConcept LogicConcept} instances that have been converted
     *   to PropositionalForm, so that later conversions of structurally
     *   identical {@link LogicConcept LogicConcepts} get the same results;
     *   this parameter is primarily used internally, and clients may omit it
     * @returns {PropositionalForm} a PropositionalForm object representing
     *   the given {@link LogicConcept LogicConcept} `LC`
     * 
     * @see {@link PropositionalForm.constantTrue constantTrue()}
     * @see {@link PropositionalForm#isAtomic isAtomic()}
     * @see {@link PropositionalForm.conditional conditional()}
     */
    static atomic ( LC, catalog ) {
        const result = new PropositionalForm( catalog )
        result.text = LC.toPutdown().replace( /^[:]/, '' )
        result.index( result ) // add it to its own catalog
        return result
    }

    /**
     * Check whether this instance of the PropositionalForm class is an atomic
     * one.  This includes those PropositionalForm instances that represent
     * the logical constant "true," as created with the
     * {@link PropositionalForm.constantTrue constantTrue()} function, as well
     * as those created with the
     * {@link PropositionalForm.atomic atomic()} function.
     * 
     * @returns {boolean} whether this instance is atomic, in either of the
     *   two ways documented above
     * 
     * @see {@link PropositionalForm.constantTrue constantTrue()}
     * @see {@link PropositionalForm.atomic atomic()}
     * @see {@link PropositionalForm#isConditional isConditional()}
     */
    isAtomic () { return this._children.length == 0 }

    /**
     * Construct a new instance of the PropositionalForm class, a compound one
     * representing a conditional expression, that is, one of the form
     * $A\to B$, where $A$ is called the "antecedent" and $B$ the
     * "consequent."  Note that this is not a member function, but a static
     * method, so you would invoke it using `PropositionalForm.conditional(A,C,c)`.
     * In fact, one does not ever construct instances of the PropositionalForm
     * class in any way other than using the static methods of this class that
     * create specific types of PropositionalForms.
     * 
     * The third parameter is for internal use, to ensure that atomic
     * {@link LogicConcept LogicConcepts} gets represented consistently.
     * 
     * @param {LogicConcept} antecedent the {@link LogicConcept LogicConcept}
     *   to use for the left-hand side of the conditional
     * @param {LogicConcept} consequent the {@link LogicConcept LogicConcept}
     *   to use for the right-hand side of the conditional
     * @param {Array} [catalog] this parameter is passed recursively to inner
     *   construction methods, so that eventually it can be used as documented
     *   in {@link PropositionalForm.atomic atomic()}
     * @returns {PropositionalForm} a PropositionalForm object representing
     *   the conditional expression described above
     * 
     * @see {@link PropositionalForm.constantTrue constantTrue()}
     * @see {@link PropositionalForm.atomic atomic()}
     * @see {@link PropositionalForm#isConditional isConditional()}
     */
    static conditional ( antecedent, consequent, catalog ) {
        // start at the end, with an atomic conclusion
        let result = consequent instanceof PropositionalForm ?
            consequent : PropositionalForm.atomic( consequent, catalog )
        catalog = result._catalog
        // the antecedent might yield multiple propositional forms
        const premises = antecedent instanceof Environment ?
            PropositionalForm.fromConclusionsIn(
                antecedent, result._catalog ) :
            [  PropositionalForm.atomic( antecedent, result._catalog ) ]
        // so prepend them all to the conclusion one at a time, A->(B->(...))
        for ( let i = premises.length - 1 ; i >= 0 ; i-- ) {
            const next = new PropositionalForm( result._catalog )
            next._children = [ premises[i], result ]
            next.text = `[${premises[i].text},${result.text}]`
            result = next
        }
        return result
    }

    /**
     * Check whether this instance of the PropositionalForm class is a
     * conditional expression.  Note that the only non-atomic form supported
     * by this class is a conditional expression, because we need to support
     * only sequents whose conclusion is an {@link Expression Expression},
     * and (for detailed reasons not discussed here) such sequents can be
     * expressed as nested conditional PropositionalForm instances.
     * 
     * @returns {boolean} whether this instance is a conditional; note that
     *   this is true iff {@link PropositionalForm#isAtomic isAtomic()} is
     *   false
     * 
     * @see {@link PropositionalForm.conditional conditional()}
     * @see {@link PropositionalForm#isConstantTrue isConstantTrue()}
     * @see {@link PropositionalForm#isAtomic isAtomic()}
     */
    isConditional () { return this._children.length > 0 }

    /**
     * Construct a new instance of the PropositionalForm class, a compound one
     * representing a sequent, that is, one of the form
     * $P_1,\ldots,P_n\vdash C$, for some list of premises $P_i$ and
     * conclusion $C$.  This is not actually a new type of compound expression
     * different from a {@link PropositionalForm.conditional conditional()};
     * it is simply a convenience function that will build nested conditionals
     * to express the sequent in question.  If each $P_i$ were an
     * {@link Expression Expression}, the sequent is equivalent to
     * $P_1\to(P_2\to\cdots\to(P_n\to C)\cdots)$, but for more complex $P_i$,
     * some conversion/factoring takes place to represent the final result as
     * only nested conditionals.
     * 
     * @param  {...any} args a sequence of {@link LogicConcept LogicConcept}
     *   instances representing the contents $P_1,\ldots,P_n,C$ of the
     *   sequent.  Optionally, an additional last argument may be a catalog,
     *   which functions the same as it does in both
     *   {@link PropositionalForm.atomic atomic()} and
     *   {@link PropositionalForm.conditional conditional()}; clients rarely
     *   need to use it.
     * @returns {PropositionalForm} a PropositionalForm instance representing
     *   the sequent, as documented above
     */
    static sequent ( ...args ) {
        let catalog = undefined
        if ( !( args.last() instanceof LogicConcept ) ) catalog = args.pop()
        let result = PropositionalForm.atomic( args.pop(), catalog )
        for ( let i = args.length - 1 ; i >= 0 ; i-- )
            result = PropositionalForm.conditional( args[i], result )
        return result
    }

    /**
     * Build a PropositionalForm instance representing the sequent for a given
     * conclusion.  Recall that the notion of a "conclusion" within an
     * {@link Environment Environment} is
     * {@link Environment#conclusions documented here} and
     * {@link Expression#isAConclusionIn also here}.  The sequent for a
     * conclusion is a conditional $P_1\to\cdots\to P_n\to C$, whose meaning
     * is like that of the sequent $P_1,\ldots,P_n\vdash C$, where $C$ is the
     * conclusion and $P_1,\ldots,P_n$ are its accessibles.
     * 
     * @param {LogicConcept} conclusion a conclusion inside a larger
     *   {@link Environment Environment}, the sequent for which should be
     *   represented as a PropositionalForm instance
     * @param {Environment} [ancestor] the outer {@link Environment
     *   Environment} in which to do the computation (i.e., no accessibles
     *   outside this {@link Environment Environment} will be included)
     * @param {Array} [catalog] this parameter functions the same way that it
     *   does in {@link PropositionalForm.atomic atomic()} and
     *   {@link PropositionalForm.conditional conditional()}; clients rarely
     *   need to use it.
     * @returns {PropositionalForm} a PropositionalForm instance representing
     *   the sequent whose conclusion is given as the first parameter and
     *   whose premises are the accessibles to that conclusion, within the
     *   given ancestor
     */
    static fromConclusion ( conclusion, ancestor, catalog ) {
        const context = conclusion.accessibles( false, ancestor ).reverse()
        const strictContext = context.filter(
            accessible => accessible.isA( 'given' ) )
        return PropositionalForm.sequent(
            ...strictContext, conclusion, catalog )
    }

    /**
     * This function simply repeats the work of
     * {@link PropositionalForm.fromConclusion fromConclusion()} multiple
     * times, once for each conclusion appearing in the given
     * {@link Environment Environment}, using that environment for the context
     * in each case.  The result is thus an array of the results one would get
     * by running the loop.
     * 
     * One can view the conjunction of these PropositionalForm results as the
     * meaning of the given {@link Environment Environment}.
     * 
     * @param {Environment} environment the {@link Environment Environment}
     *   whose conclusions should be used
     * @param {Array} [catalog] this parameter functions the same way that it
     *   does in {@link PropositionalForm.atomic atomic()} and
     *   {@link PropositionalForm.conditional conditional()}; clients rarely
     *   need to use it.
     * @returns {PropositionalForm[]} an array of PropositionalForm instances,
     *   one for each conclusion in the given {@link Environment Environment},
     *   each one representing the sequent for that conclusion in that
     *   {@link Environment Environment}
     */
    static fromConclusionsIn ( environment, catalog ) {
        return environment.conclusions().map( conclusion =>
            PropositionalForm.fromConclusion(
                conclusion, environment, catalog ) )
    }

    /**
     * The representation of this PropositionalForm object in conjunctive
     * normal form, and thus ready for use in satisfiability checking.  This
     * function can be called by clients, but it is more likely to be called
     * by them only indirectly, when they call
     * {@link PropositionalForm#isAClassicalTautology isAClassicalTautology()}
     * or {@link PropositionalForm#isAnIntuitionisticTautology
     * isAnIntuitionisticTautology()}.
     * 
     * @returns {Array[]} a representation of this PropositionalForm object
     *   in conjunctive normal form, as documented in
     *   {@link CNF the CNF namespace}
     * 
     * @see {@link PropositionalForm#isAClassicalTautology
     *   isAClassicalTautology()}
     * @see {@link PropositionalForm#isAnIntuitionisticTautology
     *   isAnIntuitionisticTautology()}
     * @see {@link PropositionalForm#negatedCNF negatedCNF()}
     */
    CNF () {
        if ( this.isConstantTrue() ) return CNFTools.constantTrue()
        if ( this.isAtomic() ) return CNFTools.proposition( this.index() )
        // (A -> B) <=> (-A v B)
        return CNFTools.or( this.LHS().negatedCNF(), this.RHS().CNF(),
                            () => this.unused() )
    }

    /**
     * The representation of *the negation of* this PropositionalForm object
     * in conjunctive normal form, and thus ready for use in satisfiability
     * checking.  This function can be called by clients, but it is more
     * likely to be called by them only indirectly, when they call
     * {@link PropositionalForm#isAClassicalTautology isAClassicalTautology()}
     * or {@link PropositionalForm#isAnIntuitionisticTautology
     * isAnIntuitionisticTautology()}.
     * 
     * Note: Negating a CNF once created is a bothersome process, so it is
     * much easier at the outset to have a routine that simply creates a CNF
     * of the negation of the expression desired.  That is the motivation for
     * the creation of this method.
     * 
     * @returns {Array[]} a representation of *the negation of* this
     *   PropositionalForm object in conjunctive normal form, as documented in
     *   {@link CNF the CNF namespace}
     * 
     * @see {@link PropositionalForm#isAClassicalTautology
     *   isAClassicalTautology()}
     * @see {@link PropositionalForm#isAnIntuitionisticTautology
     *   isAnIntuitionisticTautology()}
     * @see {@link PropositionalForm#CNF CNF()}
     */
    negatedCNF () {
        if ( this.isConstantTrue() ) return CNFTools.constantFalse()
        if ( this.isAtomic() ) return CNFTools.proposition( -this.index() )
        // -(A -> B) <=> (A ^ -B)
        return CNFTools.and( this.LHS().CNF(), this.RHS().negatedCNF() )
    }

    /**
     * Whether a propositional logic expression is a classical tautology can
     * be checked by the laborious but straightforward method of truth tables.
     * Such a method, however, is exponential in running time.  So instead, we
     * ask whether the negation of the expression is satisfiable, an
     * equivalent question, but one that is amenable to the efficiencies in
     * the satisfiability checker {@link CNF.isSatisfiable documented here}.
     * 
     * @returns {boolean} whether this PropositionalForm object is (when
     *   interpreted as a propositional logic expression) a tautology, using
     *   the rules of classical propositional logic
     * 
     * @see {@link PropositionalForm#CNF CNF()}
     * @see {@link PropositionalForm#negatedCNF negatedCNF()}
     * @see {@link PropositionalForm#isAnIntuitionisticTautology
     *   isAnIntuitionisticTautology()}
     */
    isAClassicalTautology () {
        // classical tautology <=> negation is not satisfiable
        return !CNFTools.isSatisfiable( this.negatedCNF(),
                                        this._catalog.length )
    }

    /**
     * Whether a propositional logic expression is an intuitionistic tautology
     * can be checked by attempting to construct a proof.  Because we are
     * limiting ourselves to expressions that contain only the conditional
     * operator, there are only three possible logical rules in play, making
     * the proof search a straightforward one.  In the worst case scenario,
     * the search still takes exponential time, but we incorporate a number of
     * efficienceies into the search process to minimize that problem.
     * 
     * @returns {boolean} whether this PropositionalForm object is (when
     *   interpreted as a propositional logic expression) a tautology, using
     *   the rules of intuitionistic propositional logic
     * 
     * @see {@link PropositionalForm#CNF CNF()}
     * @see {@link PropositionalForm#negatedCNF negatedCNF()}
     * @see {@link PropositionalForm#isAnIntuitionisticTautology
     *   isAnIntuitionisticTautology()}
     */
    isAnIntuitionisticTautology () {
        return canProveInIPL( [ ], [ ], this, true, new Set() )
    }

    ////////////////
    //
    //  The remaining functions are primarily used internally by this class,
    //  and thus we do not document them for clients to call (that is, there
    //  are no JSDoc comments below).  We provide, instead, brief JavaScript
    //  comments for reference by the developers of this class.
    //
    /////////////////

    // Convenience functions for getting the arguments of a conditional
    LHS () { return this._children[0] }
    RHS () { return this._children[1] }

    // For an atomic, what is my index in my own catalog?
    // This has the side effect of adding it to the catalog if it's not
    // already there.  Thus it is reasonable to call this function and just
    // discard the value, if your goal is just to add something to the catalog.
    index () {
        const text = this.text
        const index = this._catalog.indexOf( text )
        if ( index > -1 ) return index + 1
        this._catalog.push( text )
        return this._catalog.length
    }

    // A new symbol generator for the catalog stored in this object.
    // Each time it is called it will produce a new integer (which is how we
    // represent symbols, because we will be using them in CNFs) that has not
    // been used for any atomic before, and is now reserved so that it will
    // not be used by any atomic in the future.
    unused () {
        this._catalog.push( null )   // does not matter what we push, because:
        return this._catalog.length  // this will be its 1-based index
    }

    // Does a PropositionalForm object with the same the text representation
    // as this one appear in the given array?
    isIn ( array ) { return array.some( entry => entry.text == this.text ) }

    // Yields the given array with this object added.
    // More specifically:  Given an array of PropositionalForm objects, if one
    // with this object's text representation is already in the array, then
    // return the array unchanged.  Otherwise return a new array equal to the
    // old, plus this object appended to the end.
    addedTo ( array ) {
        return this.isIn( array ) ? array : array.concat( [ this ] )
    }

    // Does this PropositionalForm follow classically from the list of other
    // PropositionalForm objects P_1,...,P_n given as arguments?
    // (They must all have the same catalog for this to be checkable.)
    followsClassicallyFrom ( ...premises ) {
        if ( premises.some( premise => premise._catalog != this._catalog ) )
            throw new Error(
                'All premises must share a catalog with the conclusion' )
        let asAConditional = this
        premises.forEach( premise => {
            const next = new PropositionalForm( asAConditional._catalog )
            next._children = [ premise, asAConditional ]
            asAConditional = next
        } )
        return asAConditional.isAClassicalTautology()
    }

}

// Helper function, not public.  Checks if a sequent is valid in
// intuitionistic propositional logic (IPL).
// The sequent has a list of PropositionalForms (PFs) on the left and one PF
// on the right.  More specifically, the parameters are:
//   atomics = an array of all premises satisfying .isAtomic()
//   conditionals = an array of all premises satisfying .isConditional()
//   conclusion = the conclusion of the sequent to be checked; may or may not
//     be atomic
//   checkCPLFirst = boolean, true iff we should check CPL first.  Reason:
//     If a sequent is not CPL valid then it is not IPL valid.  Since we have
//     a fast algorithm for checking CPL validity, we run that first, and if
//     it says false, we say false.  However, there may be times when the
//     caller already knows that the sequent is CPL valid, and in that case
//     the caller may set this to false, to not waste time re-verifying that.
//   proven = JavaScript Set of texts of PFs that we already know follow from
//     the LHS of the sequent.  This set is not just atomics.  It grows as we
//     try recursive subproofs that don't end up succeeding, but that do prove
//     some new PFs before they fail, and we don't want to forget them.
const canProveInIPL = (
    atomics, conditionals, conclusion, checkCPLFirst, proven
) => {

    // console.log( 'IPL: '
    //            + atomics.map( x=>x.text ).join( ',' ) + '; '
    //            + conditionals.map( x=>x.text ).join( ',' ) + '; '
    //            + [...proven].join( ',' ) + ' |- '
    //            + conclusion.text + ' (' + checkCPLFirst + ')' )

    // If the conclusion is literally the constant true, we're done.
    if ( conclusion.isConstantTrue() ) {
        return true
    }

    // don't bother with FIC if SAT says no...unless the caller told us not to
    // do this check.  (Recursive calls that already know the check will pass
    // may tell us to skip it to save time.)
    if ( checkCPLFirst
      && !conclusion.followsClassicallyFrom( ...atomics, ...conditionals ) )
        return false

    // If the conclusion is already known, just stop now.
    if ( proven.has( conclusion.text ) ) return true

    // apply the GR rule as many times as needed to achieve an atomic RHS
    while ( conclusion.isConditional() ) {
        const A = conclusion.LHS()
        if ( A.isAtomic() ) {
            atomics = A.addedTo( atomics )
        } else {
            conditionals = A.addedTo( conditionals )
        }
        conclusion = conclusion._children[1]
    }

    // console.log( ' ... '
    //            + atomics.map( x=>x.text ).join( ',' ) + '; '
    //            + conditionals.map( x=>x.text ).join( ',' ) + '; '
    //            + [...proven].join( ',' ) + ' |- '
    //            + conclusion.text + ' (' + checkCPLFirst + ')' )

    // conclusion is now atomic.  if the S rule applies, done
    if ( conclusion.isIn( atomics ) ) return true

    // recursive applications of GL rule
    for ( let i = 0 ; i < conditionals.length ; i++ ) {
        // Try the left subproof, and record anything you prove while you work
        // on it, so that even if it fails, we increase our knowledge.  If
        // that left subproof fails, move on to the next conditional.
        const LHS = conditionals[i].LHS()
        if ( canProveInIPL(
                atomics, conditionals.without( i ), LHS, true, proven ) )
            proven.add( LHS.text )
        else
            continue
        // The left subproof succeeds, so the whole question is now equivalent
        // to whether the right subproof succeeds.
        // Note: No need to call SAT in either of the following recursions,
        // because in both cases, the sequent we're deferring to in recursion
        // is provable (in both IPL and CPL) iff the current sequent is.
        // Since we already know that the current one is CPL-provable, we know
        // the one in the recursion is, so there's no need to waste time
        // verifying that fact.
        const RHS = conditionals[i].RHS()
        return RHS.isAtomic() ?
            canProveInIPL( RHS.addedTo( atomics ), conditionals.without( i ),
                conclusion, false, proven ) :
            canProveInIPL( atomics, RHS.addedTo( conditionals.without( i ) ),
                conclusion, false, proven )
    }

    // failed to prove it in any of the legal ways, so it is not
    // intuitionistically true
    return false

}