2 Homework 2A
Due:
Tuesday, 1/16 at 9PM
This assignment may be done with an approved PARTNER.
Note: This assignment is entirely autograded. Please check your grade after submission, and if there are mistakes, correct them and resubmit before the deadline.
What to Download:
Please start with this file, filling in where appropriate, and submit your homework to the HW2A assignment on Gradescope. This page has additional information, and allows us to format things nicely.
2.1 Problem 1
We can express propositional logic using boolean functions in LSL, a language you are most likely familiar with from Fundamentals 1 (as it’s an extension to ISL+, the language of Fundies 1). Most are built in, but some we will define. See the following table, which lists the logical operator and the corresponding LSL function (or definition, if it’s not built in).
operator in logic | operator in LSL* |
\land | and |
\lor | or |
\neg | not |
\Rightarrow | (lambda (P Q) (or (not P) Q)) |
\equiv | boolean=? |
\otimes | (lambda (P Q) (or (and P (not Q)) (and Q (not P)))) |
ite | if |
* Note that for the ones we define ourselves, these are not necessarily the only possible representations.
For example, P \land Q can be expressed as the following function:
(define (p1 P Q) (and P Q))
Translate the following expressions in logic into corresponding function definitions, named p2,p3, p4. Note that the number (and names) of arguments may be different for the different expressions, as they do not all use the same variables.
definition name | logical expression |
p2 | (P \land Q) \lor \neg (R \land S) |
p3 | P \Rightarrow \neg Q |
p4 | \neg (P \land Q) \equiv \neg P \lor \neg Q |
Template code (included in file linked at top of page):
| ;; (P /\ Q) \/ ~(R /\ S) |
| (define (p2 ...) ...) |
| ;; P -> ~Q |
| (define (p3 ...) ...) |
| ;; ~(P /\ Q) = ~ P \/ ~Q |
| (define (p4 ...) ...) |
2.2 Problem 2
Just as we can express propositional logical statements as code, we can also express proofs about propositional logic in code. These proofs are often written as truth tables, with the goal to show that a given expression is always true (or maybe is never true) regardless of the assignment of variables. You can do this by enumerating, in a table, all possible assignments of variables.
For example, if we wanted to know that P \land \neg P is false or unsatisfiable (i.e., for all possible assignments of variables, the result in false), we can define the following truth table to prove it:
P | P \land \neg P |
T | F |
F | F |
Here we see, regardless of whether we assign T or F to P, our expression ends up F.
To do this in code, we can express each row of the truth table as a unit test. We can define the above expression as:
(define (p1 P) (and P (not P)))
And then write the two lines of the truth table:
(check-expect (p1 #t) #f) (check-expect (p1 #f) #f)
This then corresponds to a proof that is verified by running those tests. If one of our cases were wrong, we would get a test failure.
For this problem, you should prove that the two following equalities (these are De Morgan’s Laws) hold for all possible assignments (i.e., are valid) by first defining them (p5 and p6) and then defining their truth tables using check-expect. Remember to include all possible combinations of inputs!
equation name | logical expression |
p5 | \neg (P \land Q) \equiv \neg P \lor \neg Q |
p6 | \neg (P \lor Q) \equiv \neg P \land \neg Q |
Template code (included in file linked at top of page):
| ;; ~(P /\ Q) = ~P \/ ~Q |
| (define (p5 ...) ...) |
| (check-expect (p5 ...) ...) |
| ; ... |
| ;; ~(P \/ Q) = ~P /\ ~Q |
| (define (p6 ...) ...) |
| (check-expect (p6 ...) ...) |
| ; ... |
2.3 Problem 3
We’ve seen that logical implication (\Rightarrow) can be defined in terms of \lor and \neg (including in the table in Problem 1).
It turns out, there are many cases when you can define one operator in terms of another.
In this exercise, for each operator, define a version of it in terms of just if. For example, \neg P, would be represented as (define (op_neg P) (if P #f #t)). You are welcome to validate your encodings using truth-table tests, but you are not required.
operator | definition name |
\land | op_and |
\lor | op_or |
\Rightarrow | op_implies |
\equiv | op_equal |
\otimes | op_xor |
Template code (included in file linked at top of page):
| ;; /\ |
| (define (op_and ...) ...) |
| ;; \/ |
| (define (op_or ...) ...) |
| ;; -> |
| (define (op_implies ...) ...) |
| ;; = |
| (define (op_equal ...) ...) |
| ;; ⊕ (exclusive or) |
| (define (op_xor ...) ...) |
2.4 Problem 4
Simplifying propositional formulas is an important topic, as simpler formulas, especially if they have fewer variables, are easier to check for validity (truth), unsatisfiability (falsehood), etc.
For example, if I have the expression P \land (Q \lor \neg Q), we can see that the subexpression Q \lor \neg Q will always be true, no matter the assignment of Q, and thus we could first simplify this to P \land T. But since P \land T is equivalent to just P, we can further simplify.
In code, what this means is that the function:
(define (p7 P Q) (and P (or Q (not Q))))
Is equivalent to the function:
(define (p7s P Q) P)
And we can check that using a truth table, which has four rows since there are two variables.
(check-expect (p7 #t #t) (p7s #t #t)) (check-expect (p7 #t #f) (p7s #t #f)) (check-expect (p7 #f #t) (p7s #f #t)) (check-expect (p7 #f #f) (p7s #f #f))
Here we left Q as an input to p7s to make it obvious that the truth table test is showing they are equivalent on all inputs. Note that it is of course equivalent to a function that does not have the extra argument, but the truth table may be harder to understand, so for this problem, we will write our simplified versions in this more verbose form, even when we can eliminate variables.
Your task, in this problem, is to perform simplifications of this form for the three problems below, and include truth tables that confirm that your simplifications were correct. We are giving you the expressions written both in logical syntax and in the LSL code that we expect you to simplify & test with.
expression | in code | your simplified version | |||||
(P \land Q) \land (R \land \neg Q) |
|
| |||||
(P \land Q \land P) \lor (Q \land R) |
|
| |||||
(P \land Q \land R) \lor (\neg Q \land S \land Q) |
|
|
Template code (included in file linked at top of page):
| ;; (P /\ Q) /\ (R /\ ~Q) |
| (define (p9 P Q R) |
| (and (and P Q) |
| (and R (not Q)))) |
| (define (p9s P Q R) |
| ...) |
| ;; (P /\ Q /\ P) \/ (Q /\ R) |
| (define (p10 P Q R) |
| (or (and P Q P) |
| (and Q R))) |
| (define (p10s P Q R) |
| ...) |
| ;; (P /\ Q /\ R) \/ (~Q /\ S /\ Q) |
| (define (p11 P Q R S) |
| (or (and P Q R) |
| (and (not Q) S Q))) |
| (define (p11s P Q R S) |
| ...) |