Mathematics and Computation Exam like questions, October 24, 2004

Exams consist of three questions, but here you have four exam like questions. I define

H(x) ≐ x < 0\{ \begin{matrix}0 \\ 1 \end{matrix}

Exercise 1. (Too small for an exam question) Prove one of the following: [Mac lemma L04.0.4A: x ∈ B → if(x, u, if(x, v, w)) ≡ if(x, u, w)] [Mac antilemma L04.0.4B: x ∈ B → if(x, u, if(x, v, w)) ≡ if(x, u, w)]

Exercise 2. Prove one of the following:

[Mac lemma L04.0.5A: x ∈ D → H(x) ∈ N]

[Mac antilemma L04.0.5B: x ∈ D → H(x) ∈ N]

Exercise 3. Prove one of the following:

[Mac lemma L04.0.6A: x ∈ B → x ∧ x ≡ x]

[Mac antilemma L04.0.6B: x ∈ B → x ∧ x ≡ x]

Exercise 4. (Too large for an exam question) Prove one of the following: [Mac lemma L04.0.7A: Y′ λf.λx.case(x, T, f′ x) ≡ λx.case(x, T, ⊥)] [Mac antilemma L04.0.7B: Y′ λf.λx.case(x, T, f′ x) ≡ λx.case(x, T, ⊥)]

The following rules may be used:

[ Mac rule Case1: case(x, case(x, u, v), w) ≡ case(x, u, w) ]
[ Mac rule Case2: case(x, u, case(x, v, w)) ≡ case(x, u, w) ]

Mathematics and Computation Possible solutions to exam like questions, October 24, 2004 A proof of Mac lemma L04.0.4A : x ∈ B → if(x, u, if(x, v, w) ≡ if(x, u, w)) could be as follows: Mac proof of L04.0.4A:

L01 : Block ⊳  Begin  ;
L02 : Hypothesis ⊳  x ∈ T  ;
L03 : IfT ⊳ L2 ⊳  if(x, u, if(x, v, w)) ≡ u  ;
L04 : IfT ⊳ L2 ⊳  if(x, u, w) ≡ u  ;
L05 : Commutativity ⊳ L4 ⊳  u ≡ if(x, u, w)  ;
L06 : Transitivity ⊳ L3 ⊳ L5 ⊳  if(x, u, if(x, v, w)) ≡ if(x, u, w)  ;
L07 : Block ⊳  End  ;
L08 : Block ⊳  Begin  ;
L09 : Hypothesis ⊳  x ∈ F  ;
L10 : IfF ⊳ L9 ⊳  if(x, v, w) ≡ w  ;
L11 : Replace ⊳ L10 ⊳  if(x, u, if(x, v, w)) ≡ if(x, u, w)  ;
L12 : Block ⊳  End  ;
L13 : Cases ⊳ L6 ⊳ L11 ⊳  x∈B → if(x, u, if(x, v, w)) ≡ if(x, u, w)

Line 6 could also have argumentation Reverse’ ⊳ L4 ⊳ L3 ^{·} in which case Line 5 can be omitted.

L04.0.4A ^{·} rule L04.0.4A

Mathematics and Computation Possible solutions to exam like questions, October 24, 2004 A proof of Mac lemma L04.0.5A : x ∈ D → H(x) ∈ N could be as follows: Mac proof of L04.0.5A:

L01 : Block ⊳  Begin  ;
L02 : Hypothesis ⊳  (x < 0) ∈ T  ;
L03 : IfT ⊳ L2 ⊳  if(x < 0, 0, 1) ≡ 0  ;
L04 : TypeNumeralInN ⊳  0 ∈ N  ;
L05 : Reverse’ ⊳ L3 ⊳ L4 ⊳  if(x < 0, 0, 1) ∈ N  ;
L06 : Block ⊳  End  ;
L07 : Block ⊳  Begin  ;
L08 : Hypothesis ⊳  (x < 0) ∈ F  ;
L09 : IfF ⊳ L8 ⊳  if(x < 0, 0, 1) ≡ 1  ;
L10 : TypeNumeralInN ⊳  1 ∈ N  ;
L11 : Reverse’ ⊳ L9 ⊳ L10 ⊳  if(x < 0, 0, 1) ∈ N  ;
L12 : Block ⊳  End  ;
L13 : Cases ⊳ L5 ⊳ L11 ⊳  (x < 0) ∈ B → if(x < 0, 0, 1) ∈ N ;
L14 : Hypothesis ⊳  x ∈ D  ;
L15 : TypeNumeralInD ⊳  0 ∈ D  ;
L16 : TypeD<D ⊳ L14 ⊳ L15 ⊳ (x < 0) ∈ B  ;
L17 : L13 ⊵ L16 ⊳  if(x < 0, 0, 1) ∈ N  ;
L18 : Definition ⊳  H(x) ≡ if(x < 0, 0, 1)  ;
L19 : Reverse’ ⊳ L18 ⊳ L17 ⊳  H(x) ∈ N

H(x) ^{·} was used by Oliver Heaviside for investigations of electronic circuits.

L04.0.5A ^{·} rule L04.0.5A

Mathematics and Computation Possible solutions to exam like questions, October 24, 2004

A proof of

Mac antilemma L04.0.6B : x ∈ B → x ∧ x ≡ x

could use a non-standard representation F ≡ N ˙. . (N ˙. . N) ^{·} of falsehood. One may prove F ∈ B ^{·} using the type function \overline{B} ^{·} from page 336 in the text book and one may then combine F ∈ B ^{·} with the antilemma to get F ∧ F ≡ F ^{·}. On the other hand, we have F ∧F ≡ F ^{·} (by Computation) so we get F ≡ F ^{·}. Hence, by the definitions of F ^{·} and F ^{·} we get N ˙. . N ≡ N ˙. . (N ˙. . N) ^{·}. Taking the Tail of both sides gives N ≡ N ˙. . N ^{·} which, by the definitions of T ^{·} and F ^{·} is the same as T ≡ F ^{·}. CounterTF then yields the contradiction. The proof may look thus:

Mac proof of L04.0.6B:

L01 : Local ⊳  F ≡ N ˙. . (N : : N)  ;
L02 : Computation ⊳  \overline{B}′ F  ;
L03 : Block ⊳  Begin  ;
L04 : Algebra ⊳  ℓ′ F  ;
L05 : Replace ⊳ ClassicalPair ⊳  ℓ′ N ∧ ℓ′(N ˙. . N)  ;
L06 : Replace ⊳ ClassicalPair ⊳  ℓ′ N ∧ (ℓ′ N ∧ ℓ′ N) ;
L07 : Replace ⊳ ClassicalNil ⊳  T ∧ (T ∧ T)  ;
L08 : Computation ⊳  T  ;
L09 : Block ⊳  End  ;
L10 : IntroB ⊳ L8 ⊳ L2 ⊳  F ∈ B  ;
L11 : Antilemma ⊳  F ∈ B → F ∧ F ≡ F ;
L12 : L11 ⊵ L10 ⊳  F ∧ F ≡ F  ;
L13 : Block ⊳  Begin  ;
L14 : Algebra ⊳  T  ;
L15 : Computation ⊳  (F ∧ F) Tail  ;
L16 : Replace ⊳ L12 ⊳  F Tail  ;
L17 : Computation ⊳  F  ;
L18 : Block ⊳  End  ;
L19 : CounterTF ⊳ L17 ⊳  ⊥

L04.0.6B ^{·} rule L04.0.6B

A proof of

Mac lemma L04.0.7A : Y′ λf.λx.case(x, T, f′ x) ≡ λx.case(x, T, ⊥)

could be constructed as follows: First, define A ^{·} to be shorthand for Y′ λf.λx.case(x, T, f′ x) ^{·} (Line 1 below). Then compute A ^{·} using Lemma L8.18.2 (Line 2–6 below). After Line 6 we know that A ≡ λx.case(x, T, A′ x) ^{·} which makes it easy to prove λx.case(x, T, ⊥) ⪯ A ^{·} (Line 7–10 below).

This proves half of the Lemma L04.0.7A: InfoAntiSymmetry says that if λx.case(x, T, ⊥) ⪯ A ^{·} and A ⪯ λx.case(x, T, ⊥) ^{·} then the lemma holds (Line 18 below).

Hence, to prove the lemma, we have to prove A ⪯ λx.case(x, T, ⊥) ^{·} (Line 17 below). In other words, we have to prove that A ^{·} is less that a term that contains ⊥ ^{·}. One of the very few rules that allows that is MinimalY on page 427 in the text book. That rule looks promissing since A ^{·} contains the fixed point operator Y ^{·}.

Applying MinimalY backwards to Line 17 gives

λf.λx.case(x, T, f′x)′ λx.case(x, T, ⊥) ≡ λx.case(x, T, ⊥) ^{·}

which turns out to be easy to prove (Line 11–16 below). Line 15 uses Case2 which was provided together with the exercise.

Mac proof of L04.0.7A:

L01 : Local ⊳  A ≡ Y′ λf.λx.case(x, T, f′ x)  ;
L02 : Block ⊳  Begin  ;
L03 : Algebra ⊳  A  ;
L04 : Replace ⊳ L8.18.2 ⊳  (λf.λx.case(x, T, f′ x))′ A  ;
L05 : Replace⊳ApplyLambda ⊳  λx.case(x, T, A′ x)  ;
L06 : Block ⊳  End  ;
L07 : InfoBottom ⊳  ⊥ ⪯ A′ x  ;
L08 : Monotonicity’ ⊳ L7 ⊳  case(x, T, ⊥) ⪯ case(x, T, A′ x)  ;
L09 : InfoLambda ⊳ L8 ⊳  λx.case(x, T, ⊥) ⪯ λx.case(x, T, A′ x) ;
L10 : Reverse’ ⊳ L5 ⊳ L9 ⊳  λx.case(x, T, ⊥) ⪯ A  ;
L11 : Block ⊳  Begin  ;
L12 : Algebra ⊳  λf.λx.case(x,T,f′x)′λx.case(x,T,⊥) ;
L13 : Replace⊳ApplyLambda ⊳  λx.case(x, T, (λx.case(x, T, ⊥))′ x) ;
L14 : Replace⊳ApplyLambda ⊳  λx.case(x, T, case(x, T, ⊥))  ;
L15 : Replace ⊳ Case2 ⊳  λx.case(x, T, ⊥)  ;
L16 : Block ⊳  End  ;
L17 : MinimalY ⊳ L15 ⊳  A ⪯ λx.case(x, T, ⊥)  ;
L18 : InfoAntiSymmetry ⊳
L17 ⊳ L10 ⊳  A ≡ λx.case(x, T, ⊥)

L04.0.7A ^{·} rule L04.0.7A