Københavns Universitet

Naturvidenskabelig embedseksamen, første del Matematik & Beregninger

Skriftlig eksamen 27. oktober 2004

Sættet består af 3 opgaver, som vægtes ens. I tilfælde af fejl eller unøjagtigheder i opgaveteksten forventes det, at eksaminanderne selv præciserer besvarelsens forudsætninger. Alle sædvanlige hjælpemidler er tilladt. Opgavesættet besvares på separate ark, der udleveres af eksamenstilsynet. Besvarelsen kan formuleres på dansk eller engelsk eller en blanding heraf. Indskrivning med blyant er tilladt. Opgaveteksten kan deltagerne tage med sig.

Mathematics and Computation Exam October 27, 2004

I define [f(x, y) ≐ if(x = 0, y, f(x − 1, x : : y))] [twice ≐ λf.λx.f′(f′ x)]

Exercise 1. Prove one of the following:

[Mac lemma L04.1.1A: x ∈ N → ∀y∈N^{∗}: f(x, y) ∈ N^{∗}] [Mac antilemma L04.1.1B: x ∈ N → ∀y∈N^{∗}: f(x, y) ∈ N^{∗}]

Exercise 2. Prove one of the following:

[Mac lemma L04.1.2A: x ∈ N → ∀y∈N^{∗}: f(x, y) head ∈ N] [Mac antilemma L04.1.2B: x ∈ N → ∀y∈N^{∗}: f(x, y) head ∈ N]

Exercise 3. Prove one of the following:

[Mac lemma L04.1.3A: Y′ twice ≡ λx.⊥]

[Mac antilemma L04.1.3B: Y′ twice ≡ λx.⊥]

The following rules may be used:

[ Mac rule TypeBNotD: x ∈ B ⊢ x ∈ D ≡ F ]
[ Mac rule TypeBNotX: x ∈ B ⊢ x ∈ X ≡ F ]
[ Mac rule TypeBNotE: x ∈ B ⊢ x ∈ E ≡ F ]
[ Mac rule TypeDNotB: x ∈ D ⊢ x ∈ B ≡ F ]
[ Mac rule TypeDNotX: x ∈ D ⊢ x ∈ X ≡ F ]
[ Mac rule TypeDNotE: x ∈ D ⊢ x ∈ E ≡ F ]
[ Mac rule TypeXNotB: x ∈ X ⊢ x ∈ B ≡ F ]
[ Mac rule TypeXNotD: x ∈ X ⊢ x ∈ D ≡ F ]
[ Mac rule TypeXNotE: x ∈ X ⊢ x ∈ E ≡ F ]
[ Mac rule TypeENotB: x ∈ E ⊢ x ∈ B ≡ F ]
[ Mac rule TypeENotD: x ∈ E ⊢ x ∈ D ≡ F ]
[ Mac rule TypeENotX: x ∈ E ⊢ x ∈ X ≡ F ]

Furthermore, the following lemma may be used: [ Mac lemma L04.1.4: λx.⊥ ⪯ Y′ twice] [ Mac proof of L04.1.4:

L01 Local ⊳  A ≡ Y′ twice  ;
L02 Block ⊳  Begin  ;
L03 Algebra ⊳  Y′ twice  ;
L04 Replace ⊳ L8.18.2 ⊳  twice′ A  ;
L05 Definition ⊳  (λf.λx.f′(f′ x))′ A ;
L06 Replace ⊳ ApplyLambda ⊳  λx.A′(A′ x)  ;
L07 Block ⊳  End  ;
L08 InfoBottom ⊳  ⊥ ⪯ A′(A′ x)  ;
L09 InfoLambda ⊳ L08 ⊳  λx.⊥ ⪯ λx.A′(A′ x) ;
L10 Reverse′ ⊳ L06 ⊳ L09 ⊳  λx.⊥ ⪯ Y′ twice  ]

Mathematics and Computation Possible solutions to exam questions, October 27, 2004 A proof of Mac lemma L04.1.1A : x ∈ N → ∀y∈N^{∗}: f(x, y) ∈ N^{∗} could be as follows: Mac proof of L04.1.1A:

L01 : Definition ⊳  f(x, y) ≡ if(x = 0, y, f(x − 1, x : : y)) ;
L02 : SetN ⊳  N ∈ Set  ;
L03 : SetXListSet ⊳ L2 ⊳  N^{∗} ∈ Set  ;
L04 : Block ⊳  Begin  ;
L05 : Hypothesis ⊳  x ∈ N  ;
L06 : Hypothesis ⊳  (x = 0) ∈ T  ;
L07 : IfT ⊳ L6 ⊳  if(x = 0, y, f(x − 1, x : : y)) ≡ y  ;
L08 : Transitivity ⊳ L1 ⊳ L7 ⊳  f(x, y) ≡ y  ;
L09 : Block ⊳  Begin  ;
L10 : Hypothesis ⊳  y ∈ N^{∗}  ;
L11 : Reverse’ ⊳ L8 ⊳ L10 ⊳  f(x, y) ∈ N^{∗}  ;
L12 : Block ⊳  End  ;
L13 : Gen ⊳ L3 ⊳ L11 ⊳  ∀y∈N^{∗}: f(x, y) ∈ N^{∗}  ;
L14 : Block ⊳  End  ;
L15 : Block ⊳  Begin  ;
L16 : Hypothesis ⊳  x ∈ N  ;
L17 : Hypothesis ⊳  (x = 0) ∈ F  ;
L18 : Hypothesis ⊳  ∀y∈N^{∗}: f(x − 1, y) ∈ N^{∗}  ;
L19 : IfF ⊳ L17 ⊳  if(x = 0, y, f(x − 1, x : : y))
≡ f(x − 1, x : : y)  ;
L20 : Transitivity ⊳ L1 ⊳ L19 ⊳  f(x, y) ≡ f(x − 1, x : : y)  ;
L21 : Block ⊳  Begin  ;
L22 : Hypothesis ⊳  y ∈ N^{∗}  ;
L23 : IntroListSetPair ⊳
L2 ⊳ L16 ⊳ L22 ⊳  x : : y ∈ N^{∗}  ;
L24 : ElimAll⊳L3⊳L18⊳L23 ⊳  f(x − 1, x : : y) ∈ N^{∗}  ;
L25 : Reverse’ ⊳ L20 ⊳ L24 ⊳  f(x, y) ∈ N^{∗}  ;
L26 : Block ⊳  End  ;
L27 : Gen ⊳ L3 ⊳ L25 ⊳  ∀y∈N^{∗}: f(x, y) ∈ N^{∗}  ;
L28 : Block ⊳  End  ;
L29 : Induction ⊳ L13 ⊳ L27 ⊳ x ∈ N → ∀y∈N^{∗}: f(x, y) ∈ N^{∗}

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

Mathematics and Computation Possible solutions to exam questions, October 27, 2004 A proof of Mac antilemma L04.1.2B : x ∈ N → ∀y∈N^{∗}: f(x, y) ∈ N^{∗} could be as follows: Mac proof of L04.1.2B:

L01 : Antilemma ⊳  0 ∈ N → ∀y∈N^{∗}: f(0, y) head ∈ N ;
L02 : TypeNumeralInN ⊳  0 ∈ N  ;
L03 : L1 ⊵ L2 ⊳  ∀y∈N^{∗}: f(0, y) head ∈ N  ;
L04 : SetN ⊳  N ∈ Set  ;
L05 : IntroListSetEmpty ⊳ L4 ⊳ ⟨ ⟩ ∈ N^{∗}  ;
L06 : SetXListSet ⊳ L4 ⊳ N^{∗} ∈ Set ;
L07 : ElimAll ⊳ L6 ⊳ L3 ⊳ L5 ⊳ f(0, ⟨ ⟩) head ∈ N  ;
L08 : Computation ⊳  f(0, ⟨ ⟩) head ≡ ⟨ ⟩  ;
L09 : Replace’ ⊳ L8 ⊳ L7 ⊳  ⟨ ⟩ ∈ N  ;
L10 : SubtypeNZ ⊳ L9 ⊳  ⟨ ⟩ ∈ Z  ;
L11 : SubtypeZD ⊳ L10 ⊳  ⟨ ⟩ ∈ D  ;
L12 : TypeEmptyListInE ⊳  ⟨ ⟩ ∈ E  ;
L13 : TypeENotD ⊳ L12 ⊳  ⟨ ⟩ ∈ D ≡ F  ;
L14 : CounterTF ⊳ L11 ⊳ L13 ⊳ ⊥

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

Mathematics and Computation Possible solutions to exam questions, October 27, 2004 A proof of Mac lemma L04.1.3A : Y′ twice ≡ λx.⊥ could be as follows: Mac proof of L04.1.3A:

L1 : Block ⊳  Begin  ;
L2 : Algebra ⊳  twice′ λx.⊥  ;
L3 : Definition ⊳  (λf.λx.f′(f′ x))′ λx.⊥ ;
L4 : Replace ⊳ ApplyLambda ⊳  λx.(λx.⊥)′((λx.⊥)′ x) ;
L5 : Replace ⊳ ApplyLambda ⊳  λx.⊥  ;
L6 : Block ⊳  End  ;
L7 : MinimalY ⊳ L5 ⊳  Y′ twice ⪯ λx.⊥  ;
L8 : L04.1.4 ⊳  λx.⊥ ⪯ Y′ twice  ;
L9 : InfoAntiSymmetry ⊳ L7 ⊳ L8 ⊳ Y′ twice ≡ λx.⊥

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