CS212
Problem Sets CS212
Problem Sets As you can see, this problem set is quite lengthy and it may take you some time to familiarize yourself with the mathematical concepts that will be use throughout the problem set. However, we want to make it clear at the beginning that you are not responsible for all the math details. So don't feel nervous if you find yourself completely lost about the math. We only expect a brief understanding so that you know what's going on.
For this assignment, you can work in pairs. If you choose to work in pairs, you must only submit one copy of your solution using the online submission system.
If you have trouble with the course software or are generally stuck, come to our office hours or consulting hours. Alternatively, post a question to the newsgroup cornell.class.cs212. As a last resort, send email to cs212@cs.cornell.edu.
Boolean logic lies at the very heart of computer science. Indeed, the CPU you are using is composed of literally millions of relatively simple logic gates. In this problem set, we will implement an interactive Scheme program that will let us write propositional calculus (the simplest form of boolean logic) formulas and manipulate them in various ways.
As an interactive program, the solver is implemented as a continuously looping program that:
This is known as a read-eval-print-loop in Scheme circles. The Swindle interpreter itself, in fact, acts in a manner that is very similar to the logic solver.
As the source code for this problem set is relatively large, we have tried to separate it into more or less independent units that can be independently understood. The naming convention that we use in this problem set was chosen to reflect that. A function will have the name object:func where object is the name of an abstract data type, and func is an operation that is supported by that data type. In addition, we define the predicate object? to be a function that returns true if its applied to a value that is an instance of object and #f otherwise.
We use a similar naming scheme for grouping sets of related functions. A function module:func is part of a group of functions that implement some functionality called module.
For example, the driver function (the function that starts the solver running) for the solver is called solver:run because it is part of the interactive solver proper.
The read function is responsible for reading user input. For example, if you say:
(define b (read))
The read function will pause and ask you to type in some input. For example if you enter 23, the variable b will be bound to the integer value 23. If you type (+ 40 2), the variable will be bound to a list of three elements. Note that in the second case, the value of b is similar to what it would be if we defined b in the following manner:
Note, especially, that the value of b is not 42.(define b '(+ 40 2))
The echon function allows us to write arbitrary things to the display, separated by spaces. The newline function moves the cursor to the beginning of the following line. The echo command is a combination of both echo and newline; it takes an arbitrary number of arguments and writes them to the display with spaces in between, and then terminates the whole thing with a newline.
The echo and echon functions are Swindle built-ins. The newline function is part of standard Scheme.
These two functions (defined in ps3.ss) are provided in order to make it easy for an interested programmer (you, the student, for example) to extend the functionality of the solver. The exclamation marks in the name of the functions call attention to the fact that these functions perform a side-effect (in particular, they modify some data that the solver depends on).
We point out these two functions at this time because they are implemented in terms of set!. Please note that you are NOT to use set! in any solutions to this problem set.
aka: Frequently Asked Questions
In doing this problem set, you are expected to respect the abstractions that we have defined. Note that in particular, this means that you should not assume anything about the implementations of the propositions, such as the incidental fact that they are lists of symbols.
It should not be necessery to use defstruct, defmethod, or any of the Swindle typing mechanisms to successfully complete this problem set.
The main solver loop (callable as solver:run) in the problem set will fail to work correctly until you complete problem two.
Boolean logic, named after George Boole (1815--1864), concerns itself with statements that are either true or false. As such, it has long been thought of as one of the precursors to modern computer science.
There are several different formalizations of boolean logic that have been developed over the years by philosophers, logicians, mathematicians and computer scientists. One particular formalization, the one that we have chosen to implement for this problem set, is the propositional calculus.
The propositional calculus deals with propositions. A proposition is simply a statement that can be either true or false. Some examples of propositions are:
In the propositional calculus, we represent propositions using propositional variables, for example p, q, r.
We can combine several propositions together using logical connectives. Thus we define a propositional formula as either:
The constant true is a formula that is always true. The constant false is a formula that is never true.
A common set of four connectives that are widely understood are:
Here are some examples of formulas:
Suppose that p stood for "It is raining", r for "John Cleese is short", s for "John Cleese has a silly walk", a for "Today is Tuesday", b for "It is Thursday", and c for "I have CS212 today". Then the preceding formulas could be informally interpreted in English as:
We would like to determine whether a given formula f is true or false. This depends only upon whether the propositional variables within the formula are true or false. That is, if we are told whether or not the propositional variables p1,...,pn are true, and we have a formula f built out of those variables, then we can determine whether or not the entire formula is true. We do so by employing the following truth table which tells us how to determine true formulas built out of connectives and sub-formulas:
X Y X & Y X | Y X=>Y ~X 1. true true true true true false 2. true false false true false false 3. false true false true true true 4. false false false false true true
Read the first line as "if X is true and y is true, then X&Y is true, X|Y is true, X=>Y is true, and ~X is false." Similarly for the other lines. So, for instance if p is true and q is false, then the formula (p & (~p | q)) => q is true because:
Sometimes, we can determine that a formula is true regardless as to whether its propositional variables are true or false. For instance, no matter what p is, p | ~p is always true. When a formula is always true independent of its variables, we say the formula is a tautology.
In this problem set, we have chosen to represent propositional formulas using an abstract data type, proposition.
In fact, we have the following type hierarchy:
We say that a variable is a kind of proposition, and that a disjunction is a kind of binary-formula, which is in turn a kind of proposition. That means that any operation that is supported by a proposition is supported by its subtypes (ie, the things that are kinds of propositions). The converse is not true. For example, all negations are kinds of propositions, but it is not necessarily true that all propositions are kinds of negations, so we can have operations on negations that are not possible with the supertype (in this particular example, we can ask a negation for the subformula its negating, but that kind of request does not make sense for a general proposition).
In order to create values that are propositions, we have several constructors.
You should only manipulate the propositional expressions using our accessor functions, and not by poking around the actual implementation of the construct.
Some sample propositions:
(variable? (variable:make 'p)) ==> #t (variable? (variable:make '(p r))) ; '(p r) == (list 'p 'r) ==> #f (variable? (variable:make 42)) ==> #f (variable? (variable:make #f)) ==> #f (variable? (variable:make 'mimsy-borogrove)) ==> #t (variable? const:TRUE) ==> #t
Note that variables are always created using the variable:make function; you should not break this abstraction.
Similarly, formulas are defined as follows. For example, the formula (((p & q) | (q & r)) => (~p | ~r)) would be represented as:
(define p (variable:make 'p))
(define q (variable:make 'q))
(define r (variable:make 'r))
(define example-formula
(implication:make (disjunction:make (conjunction:make p q)
(conjunction:make q r))
(disjunction:make (negation:make p)
(negation:make r))))
Alternatively, there is a function called proposition:translate which will translate a list containing the propositional expression into the proposition construct. Hence the above can also be represented as:
(define example-formula
(proposition:translate
'(implies (or (and p q) (and q r))
(or (not p) (not q)))))
Similarly, there is a function called proposition->list that converts a propositional construct into a list.
Please be sure to read the ps3.ss file, as it contains many other functions that will make the problem set a lot easier to implement.
In this problem set, user input is read in a Read-Eval-Print-Loop. The main structure of the routines require have already been written; you are only required to read through the code and understand how user input is parsed and executed. For this question, you will need to add a quit command to the REPL so that the user can quit from the solver. This should be quite straightforward once you understand the code.
What to turn in: For this problem, turn in your code that adds the quit function to the Read-Eval-Print-Loop.
For this problem, write a function bv:conflicts? that takes a variable, a truth value, and a variable assignment and returns #t if the given variable is in the variable assignment and the truth value is different from the assignment that is passed to bv:conflicts?. For example:
(bv:conflicts? (variable:make 'x) #t (bv:empty))
==> #f
(bv:conflicts? (variable:make 'x)
#t
(bv:extend (variable:make 'x)
#t
(bv:empty)))
==> #f
(bv:conflicts? (variable:make 'y)
#f
(bv:extend (variable:make 'y)
#t
(bv:empty)))
==> #t
(bv:conflicts? (variable:make 'z)
#f (bv:extend (variable:make 'borogrove)
#f
(bv:empty)))
==> #f
(bv:conflicts? const:FALSE #t (bv:empty))
==> #t
(bv:conflicts? const:FALSE #f (bv:empty))
==> #f
What to turn in: For this problem, turn in your definition of bv:conflicts? as well as any helper functions that you wrote that it calls.
Write the function proposition:well-formed? that takes a single parameter, and returns #t if that parameter is a well-formed formula, or #f otherwise. For the purposes of this problem, a well-formed formula is inductively defined as:
Here's some sample output:
(proposition:well-formed? (variable:make 'foobar))
==> #t
(proposition:well-formed? (disjunction:make (variable:make 'p)
(variable:make 'q)))
==> #t
(proposition:well-formed? const:TRUE)
==> #t
(proposition:well-formed? '(or p q))
==> #f ;;; '(or p q) is a 3-element list, not a proposition
(proposition:well-formed? (disjunction:make 'foo 'bar))
==> #f ;;; 'foo and 'bar are symbols, not propositions
(proposition:well-formed? (variable:make 42))
==> #f ;;; b/c (variable? (variable:make 42)) ==> #f
What to turn in: For this problem, turn in your code for the function proposition:well-formed? as well as for any additional code that you may have written in implementing proposition:well-formed?. Make your code bullet proof -- it should not generate a run-time error for any reasonable input.
Write a function proposition:find-var that takes a well-formed formula (ie, you can assume that the formula that you are passed is well-formed) and returns a list of all variables that occur in it. Each variable in the formula f should appear exactly once in the list returned by (proposition:find-var f), regardless of how many times it appears in f. The order of the variables does not matter.
(map variable:name
(proposition:find-var (proposition:translate 'x)))
==> (x)
(map variable:name
(proposition:find-var (proposition:translate
'(implies (and x (or y w))
(not z)))))
==> (w x y z)
(map variable:name
(proposition:find-var
(proposition:translate
'(and x (and x (or x (implies x x)))))))
==> (x)
(map variable:name
(proposition:find-var (proposition:translate '(or true
false))))
==> (false true)
What to turn in: For this problem, turn in your code for proposition:find-var and examples showing that it works.
At this point you have written all the functions to make the solver fully operational.
You should now start the solver by typing (solver:run). You should see the solver prompt "Solver?". You can now type commands for the solver to execute.
The solver is self-documenting, so you could now try: (help) to see a list of valid commands and a brief synopsis of each command.
Play around with the solver and get familiar with boolean logic and the interactive solver.
...and now back to our regularly scheduled problem set
Currently, we only consider unary uses of not and binary uses of and, or, and implies. not only makes sense with one argument, and one could argue about the correct meaning for n-ary implication, but the other connectives could easily take a higher number of arguments. The meaning for n-ary and (and similarly, or) is intuitive: (and e1 e2 ... en) is true iff e1 is true, e2 is true, ..., and en is true. For this problem, you have to write code to support n-ary versions of the binary connectives and and or.
To extend the binary operators to accept n-ary forms, you will have to make use of the function proposition:translator:add!. Read the ps3.ss file to see how the current binary forms are added to the translation map. (Hint: Basically you will have to convert the n-ary forms into binary forms so that you can use conjunction:make and disjunction:make to create the propositional constructs.)
Your n-ary forms should associate to the right, ie (and p q
r) should be interpreted as
Note: You should handle the cases (and x), (and), (or x), and (or) as well. Think about what these should mean, and handle them accordingly. (Hint: What does Scheme do with these cases? Why?) Again, make your code bullet proof.
Interaction with the solverSolver? (print (or p q r)) ==> (or p (or q r)) Solver? (print (and a b (or c d e f))) ==> (and a (and b (or c (or d (or e f))))) Solver? (print (implies a b c)) print: argument was not a wff
What to turn in: For this problem, turn in your code that implements the extra functionality to and and or.
Recall from the top of this web page, that in the propositional calculus we treat all variables as having either of two values: true or false.
In so-called first-order logic (note that we have now left the propositional calculus), there exists a notion of qualification. In essence you can express statements that talk about all values that a variable can take on, instead of a single particular one.
For example you can say: (forall p (implies p p)) and mean that no matter what value the variable p takes on, you assert that p implies p.
In the predicate calculus such statements are quite general because they range over all objects in your universe of discourse. In the propositional calculus, however, we only have two values: true and false. As a result, we can treat Universal (for all) and Existential (there exists) qualifications just as simple macro expansions:
(forall v F) expands to (and F[v->true] F[v->false]) (exists v F) expands to (or F[v->true] F[v->false])
That is, to translate an expression of the form (forall v F), you should translate the subformula F, and return the conjunction formed by replacing the variable v in the translation of F by true and false.
Note that this means that the variable p no longer appears in the formula.
For this problem you should implement two new translators for the translator map for the universal and existential qualifiers
In doing so, you should also implement a function (proposition:substitute v s F) that takes three arguments, the variable v to replace, a subformula s to replace it with, and a formula F on which to operate. The function should return a new formula in which all occurrences of v have been replaced by s.
Solver interaction:Solver? (print (forall p p)) ==> (and true false) Solver? (print (exists q (and q true))) ==> (or (and true true) (and false true)) Solver? (print (or (exists p (implies p q)) (not q))) ==> (or (or (implies true q) (implies false q)) (not q)) Solver? (print (or p (forall p (not p)))) ==> (or p (and (not true) (not false)))
Note that in the last example, there is a p remaining in the translated formula because it is outside the scope of the qualifier.
What to turn in: For this problem turn in your definition of proposition:substitute and all code that implements the translation of the universal and existential qualifiers.
In some situations, it is desirable to take a "high-level" formula and translate it to a "lower-level" formula that is equivalent. By equivalent we mean that, no matter what truth values you assign to the variables of the formulas, when you evaluate them, you get the same thing. For example, some CMOS hardware chips only provide the functionality of not and and. But hardware designers want to express their logic using connectives like implies and or as well as not and and. So they need a tool to translate their high-level logic descriptions down to low-level formulas that can be implemented directly by the chips. (You'll learn more about this in CS314.) Of course, we can't translate away all of the connectives, but we can sure get rid of a lot of them.
For instance, we can encode the formula (X & Y) as ~((~X) | (~Y))) thereby eliminating and in favor of not and or. Using the truth table, it is easy to see that regardless as to whether or not the formulas X and Y are true, these two formulas evaluate to the same thing:
X Y X&Y ~X ~Y (~X | ~Y) ~(~X | ~Y) -- -- --- --- --- --------- ---------- #t #t #t #f #f #f #t #t #f #f #f #t #t #f #f #t #f #t #f #t #f #f #f #f #t #t #t #f
For this problem, you will add a new command rewrite to the solver that takes a formula (checks that its well formed, etc...) and rewrites it to an equivalent formula that uses implies as the only connective. To do so, you must figure out how to replace formulae of the form ~X, X&Y, and X|Y with some combination of X, Y, true, false, and implies.
What to turn in:For this problem, turn in your code for the rewrite command.
For this problem you will add a command simplify to the solver that will take a list of variable assignments and a formula and evaluate as much of the formula as possible, given the values for the variables. Some examples will illustrate what is generally expected of you:
Interaction with the solver
Solver? (simplify () (and true (or false (implies false false)))) ==> true Solver? (simplify () (implies p false)) ==> (not p) Solver? (simplify ((p true) (q false)) (or p q)) ==> true Solver? (simplify ((p true) (q false) (p true)) p) ==> true Solver? (simplify ((p true) (p false)) q) simplify: conflicting assignment! Solver? (simplify ((p true)) q) ==> q
At least the following simplifications should be implemented:
What to turn in: For this problem set turn in all the code necessary to implement the simplify command. Note that this will likely involve writing a function list->bv (and this function should return #f if its argument cannot be successfully turned into a boolean valuation (bv)).
