New Element Representation
Formula: TYPE = AlgebraClasses.Object;
Quantifier:
TYPE = {exists, forAll};
PropositionalConnective: TYPE = {and, or, xOr, difference, implies, equivalent};
FormulaData: TYPE = REF FormulaDataRec;
FormulaDataRec:
TYPE ~
RECORD [
SELECT type:*
FROM
atomic => [
rel: ASAtomicFormulaOps.Operator, -- relation
polynomial: Polynomials.Polynomial -- standard form assumed, i.e. polynomial rel 0.
],
negation => [
arg: Formula
],
compound => [
op: PropositionalConnective,
args: LIST OF Formula -- two or more, obviously; assumed to all have same free variables
],
quantified => [
quantifiers: LIST OF Quantifier, -- a sequence of m >= 1 Quantifiers
matrix: Formula -- it is assumed that matrix has at least m free variables, and that the quantifiers bind the "upper" ("rightmost") m of them.
]
ENDCASE
];
It is not assumed that Formulas are "simplified", or in "canonical form" (notions which may well be meaningless for a given FormulaStructure).
Old Element Representation
Formulas are represented as (not necessarily simplified) words that are elements of a certain Boolean Algebra.
Formula: TYPE = AC.Object;
FormulaData: TYPE = REF FormulaDataRec;
FormulaDataRec:
TYPE =
RECORD [
numFreeVars: CARDINAL,
quantifiers: QuantifierSeq ← NIL, -- Assert length(quantifiers) = numTotalVars - numFreeVars = r - k. It is assumed that the lowest k variables are free, and the highest r - k are quantified.
atomicMatrix: BOOL ← FALSE,
mainOperator: FormulaOperators.Operator, -- (and, or, or not if not atomicMatrix; otherwise a Relation)
operands: LIST OF Formula ← NIL, -- nonNIL iff not atomicMatrix; then each assumed to have r free variables, of which last (r - k) will be governed by the above quantifiers.
polynomial: POL.Polynomial ← NIL -- nonNIL iff atomicMatrix
];
QuantifierSeq: TYPE = REF QuantifierSeqRec;
QuantifierSeqRec:
TYPE =
RECORD
[SEQUENCE lengthPlus1: [1..100] OF Quantifier];
Quantifier: TYPE = {Exists, ForAll};
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;
ReadFormula:
PROC [in:
IO.
STREAM, formulaAlgebra:
AC.Object]
RETURNS [formula: Formula, termChar:
CHAR];
ReadAtomicFormula:
PROC [in:
IO.
STREAM, formulaAlgebra:
AC.Object]
RETURNS [formula: Formula, termChar:
CHAR];
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.
Simplify: AlgebraClasses.UnaryOp;
Do easy simplifications. Harder ones will be done by a cad-based method that, when available, will dynamically replace this one in the property list (that e.g. makes use of signatures that do-not occur).