Structure Constructor
MakeFormulaAlgebra:
PROC [polynomialRing: AlgebraClasses.Object]
RETURNS [formulaAlgebra: AlgebraClasses.Object];
The baseCoeffRing of polynomialRing may be either ordered or unordered; if unordered, it is the user's responsibility not to create atomic formulas with relations like "less". However, AllVarEval will catch an attempt to eval such a bogus atomic formula.
Record that the resulting Structure is a BooleanAlgebra.
Structure Operations
PrintName: AlgebraClasses.ToRopeOp;
ShortPrintName: AlgebraClasses.ToRopeOp;
IsFormulaAlgebra: AlgebraClasses.UnaryPredicate;
PolynomialRing: AlgebraClasses.UnaryOp;
selector: polynomialRing of a Formula Structure
Element Constructors
Quantify:
PROC [quantifiers:
LIST
OF Quantifier, in: Formula]
RETURNS [out: Formula];
No check that the quantifiers actually correspond to the rightmost free variables of the representation of the input Formula in the way that the caller intended.
QuantifyChecked:
PROC [quantifiers:
LIST
OF Quantifier, variables:
LIST
OF Variables.Variable, in: Formula]
RETURNS [out: Formula];
Gets the free variables V of the input formula, and checks that the supplied list of m variables is exactly the rightmost m variables of V.
Element Conversion and I/O
Recast: AlgebraClasses.BinaryOp;
CanRecast: AlgebraClasses.BinaryPredicate;
ToExpr: AlgebraClasses.ToExprOp;
LegalFirstChar: AlgebraClasses.LegalFirstCharOp;
Read: AlgebraClasses.ReadOp;
FromRope: AlgebraClasses.FromRopeOp;
ToRope: AlgebraClasses.ToRopeOp;
Write: AlgebraClasses.WriteOp;
Element Operations
FreeVariables: AlgebraClasses.UnaryToListOp;
Returns an (ordered) list of the free variables of a Formula
Negate: AlgebraClasses.UnaryOp;
And: AlgebraClasses.NaryOp;
Checks that args have same free variables, as do all binary or more ops.
Or: AlgebraClasses.NaryOp;
XOr: AlgebraClasses.BinaryOp;
Difference: AlgebraClasses.BinaryOp;
Implies: AlgebraClasses.BinaryOp;
Equiv: AlgebraClasses.BinaryOp;
AllVarEval: AlgebraClasses.BinaryOp;
First arg is a Formula, secondArg a point (Vector).
Checks that length(point) = num free vars of Formula.
Returns an element of the Structure Bools. Or should be BinaryPredicate?
Lazy evaluation:
For a conjunction, stops and returns false as soon as one false conjunct found.
For a disjunction, stops and returns true as soon as one true disjunct found.
For a difference, returns AllVarEv[A AND (NOT B)].
For an implication, returns AllVarEv[(NOT A) OR B].
For an equivalence, returns AllVarEv[A=>B AND B=>A].
Should complain if baseCoeffRing of polynomialRing of the formulaAlgebra is unordered, and input formula is an atomic formula with an order relation (e.g. "less").
Eval: AlgebraClasses.BinaryOp;
First arg is a Formula, secondArg a point (Vector).
Checks that n = length(point) <= m = num free vars of Formula. Assumes that rightmost free vars are to be evaluated
If n < m, then returns a Formula with m-n free variables; if n = m, returns AllVarEval[firstArg, secondArg];
If n < m, basically just walks the formula and evaluates the polynomials in the atomic formulas.