Logic in Cecil

For this part of the homework, to gain practice programming in Cecil and using Vortex, you will develop an implementation of propositional logic formulae (i.e., boolean expressions) in Cecil.  Your implementation should exploit a number of Cecil language features, as well as including some interesting algorithms and representation choices.

The logic.cecil file is a starter file defining the interface to Formula objects; you should flesh it out with a real implementation.  The logic-tests.cecil file contains an initial set of tests for your implementation; sample output of running logic-tests.cecil on my sample solution is here. You should also add your own tests to logic-tests.cecil.

API

There are several different kinds of logic formulae that can be constructed:

• true and false literals (named True and False)
• boolean variables (created by invoking Variable(name), where name is the name of the variable)
• negations (created by invoking Not(f), where f is some formula)
• conjunctions (created by invoking And(f1, f2), where f1 and f2 are some formulae)
• disjunctions (created by invoking Or(f1, f2), where f1 and f2 are some formulae)
• implications (created by invoking Implies(f1, f2), where f1 and f2 are some formulae, meaning that f1 implies f2)

All of these expressions yield an object of type Formula (or some subtype of Formula).

The following operations are defined on Formula objects (in addition to the formula "constructors" above):

• =(Formula, Formula):bool
  returns whether two formulae are structurally equal
• print_string(Formula):string
  returns a printable string representation of the formula
• evaluate(Formula, bindings:table[string,bool]):bool
  returns whether the formula evaluates to true or false, where bindings specifies the boolean values of (at least) the variables in the formula (evaluate is allowed to fail if any variables mentioned in the formula are not given values in bindings)
• varsDo(Formula, &(string):void):void
  invoke the argument closure on the name of each variable occurring in the formula; if a variable appears in the formula more than once, the closure will be invoked with that variable's name more than once.

Optionally, there is an additional operation available for formulae:

• isTautology(Formula):bool
  return whether the formula is always true, no matter what bindings are given to the variables in it; for example, And(Variable("a"),Not(Variable("a"))) is a classic tautology, the "law of the excluded middle."

Canonical Representation

Formulae must be represented internally in canonical form.

• Implications must be represented using negations and disjunctions (there is no direct representation of an implication):
  • Implies(A, B) should be represented as Or(Not(A), B).
• Disjunctions cannot have disjunctions as their second argument; this forces disjunctions to be written in left-associative form:
  • Or(A, Or(B,C)) should be represented as Or(Or(A,B), C).
• Conjunctions cannot have disjunctions as either argument, and cannot have conjunctions as their second argument:
  • And(Or(A,B), C) should be represented as Or(And(A,C), And(B,C));
  • And(A, Or(B,C)), if A is not a disjunction, should be represented as Or(And(A,B), And(A,C));
  • And(A, And(B,C)) should be represented as And(And(A,B), C).
• Negations can have neither disjunctions nor conjunctions as arguments:
  • Not(And(A,B)) should be represented as Or(Not(A), Not(B));
  • Not(Or(A,B)) should be represented as And(Not(A), Not(B)).
  (Note how the Ands and Ors swap roles when negations are pushed inside them.)

Implementation Notes

You should use good Cecil style in your implementation.  You should use type declarations for method and field arguments and results, and you should be able to successfully typecheck your implementation.  Several features of Cecil will be helpful, including multimethods and easy support for one-of-a-kind objects.  Explicit tests like if should be used rarely, if at all; method dispatching should take care of any "type tests".  Here are some suggestions:

• You should probably have concrete objects to represent True and False, and template objects for VariableFormula, NegationFormula, ConjunctionFormula, and DisjunctionFormula.  These can be organized into a suitable inheritance hierarchy below abstract object Formula.
• The canonical form rules suggest introducing abstract objects like NegationOrSimplerFormula and ConjunctionOrSimplerFormula, where true, false, and variables are "simpler" than negations, which are simpler than conjunctions, which are simpler than disjunctions. LiteralFormula (for True and False) and AtomicFormula (for literals and variables) might also be useful notions to help in organizing the hierarchy.
• The = operation can have a default implementation for a pair of Formulae that returns false, which is overridden by a multimethod for each Formula descendant that might return true.  E.g., in my sample solution, I have the following multimethod:

  method =(f1@:ConjunctionFormula, f2@:ConjunctionFormula):bool { 
      f1.arg1 = f2.arg1 & { f1.arg2 = f2.arg2 } }

• The "constructor" operations like Not, And, and Or need to identify whether their arguments are in the required form, and if not, what to do about it. The best way to do this is to define several (multi)methods that dispatch differently, and handle the various cases.  E.g., in my sample solution, I have the following Or methods:

  method Or(f1@:Formula, f2@:ConjunctionOrSimplerFormula):Formula {
      concrete object isa DisjunctionFormula { arg1 := f1, arg2 := f2 } }
  method Or(f1@:Formula, f2@:DisjunctionFormula):Formula {
      Or(Or(f1, f2.arg1), f2.arg2) }

  The former method handles the case where the arguments are already in the required form, while the latter method handles the rule that Or(A, Or(B,C)) should be represented as Or(Or(A,B), C).
• To test whether a formula is a tautology, one can first compute the set of unique names used in the formula, then construct all possible combinations of true and false for that many variables, and for each combination construct an assignment table mapping each unique variable name to some boolean value, and evaluate the formula under that assignment.  If all assignments lead to the formula being true, then it's a tautology.