Homework #3

1.1, 2.1, 3.1, and 4.1 due Friday, Feb 2 in class. The rest is due Tuesday, Feb 6 in class.

This is a paper and pencil assignment. Pencil. Not pen. Please write legibly!

1. Prove the following theorems:

   1. P₀, P₁, ..., P_k |= Q   iff   P₀ ⋀ P₁ ⋀ ... ⋀ P_k |= Q

   2. P₀, P₁, ..., P_k |= Q   iff   |= (P₀ ⋀ P₁ ⋀ ... ⋀ P_k) → Q

2. Recall your sum-list function from HW #1 Problem 4.

   1. Formulate a structural induction principle for List[Number].

   2. Prove that, for every pair of List[Number] xs and ys,

      (sum-list (append xs ys)) = (+ (sum-list xs) (sum-list ys))

3. Recall your data definition of a binary tree of numbers (BTN) from HW #1 Problem 4.

   1. Formulate a structural induction principle for BTN.

   2. On the same problem, you were asked to formulate test cases that demonstrate that the sum of a BTN is the same as the sum of the list of numbers obtained by flattening the tree. Prove that this test works for every BTN.

      Hint: The result in exercise 2.2 will help.

4. Recall the data definition for propositions given in HW #2.

   1. Write down a structural induction principle for propositions.

   2. We defined the truth value of a proposition given an interpretation as follows:

      ;; Interpretation = (A -> {⊤, ⊥})
      
      ;; M : Proposition Interpretation -> {⊤, ⊥}
      ;; determine truth of a proposition under a particular interpretation
      M[P -> Q, a] = if M[P, a] then M[Q, a] else ⊤
M[P /\ Q, a] = min( M[P, a] , M[Q, a] )
M[P \/ Q, a] = max( M[P, a] , M[Q, a] )
M[~P, a] = flip( M[P, a] )
M[true, a] = ⊤
M[false, a] = ⊥
M[A, a] = a[A]

      where
      
      ;; flip : {⊤, ⊥} -> {⊤, ⊥}
      flip(⊤) = ⊥
flip(⊥) = ⊤

      ;; min : {⊤, ⊥} {⊤, ⊥} -> {⊤, ⊥}
      min(⊤, ⊤) = ⊤
min(X, Y) = ⊥, when X and Y are not both ⊤.
      
      ;; max : {⊤, ⊥} {⊤, ⊥} -> {⊤, ⊥}
      max(⊥, ⊥) = ⊥
max(X, Y) = ⊤, when X and Y are not both ⊥.

      Prove that M holds up its end of the contract. That is, prove:

      For all propositions P and interpretations a, either M[P, a] = ⊤ or M[P, a] = ⊥.