TLC

Question 1

Proof by induction for ∀n ∈ N. A

Answer 1

– When x = 0 … hence A is true of 0.
– When x = k + 1, assume A holds of k
… A is true of k + 1

Question 2

Proof by induction for ∀R ∈ REGEXP. A

Answer 2

– When R = ε … hence A is true of ε
– When R = φ … hence A is true of φ
– When R = a … hence A is true of a
– When R is of shape (R1 + R2), assume A holds of R1 and R2 separately … A is true of (R1 + R2)
– When R is of shape (R1· R2), assume A holds of R1 and R2 separately … A is true of (R1 + R2)
– When R is of shape R∗1, assume A holds of R1… A is true of R∗1

Question 3

Subterm of term M

Answer 3

Includes M itself and is any substring that is itself a term except the variable between lambda and the . if it does not occur outside this position

Question 4

Parentheses:
MN
MNP
λx.MN
λxy.M
x y (pred y)

Answer 4

(MN)
((MN)P)
(λx.(MN))
(λx.(λy.M))
((x y) (pred y))

Question 5

Free variables:
FV(x)
FV(c)
FV(PQ)
FV(λx.N)

Answer 5

{x}
φ
FV(P) U FV(Q)
FV(N) \ {x}

Question 6

a-equivalence?
λx.x and λy.y
λxy.x and λyx.y
λx.xy and λx.xz

Answer 6

Yes
Yes
No

Question 7

Redex/contraction pair example

Answer 7

pred Z/Z

Question 8

Confluence

Answer 8

If M ->* P and M->* Q then there exists a term N such that P->* N and Q->* N

Question 9

Unique normal forms

Answer 9

If M->* N and M->* P with N and P normal forms, then N=P

Question 10

Fixed point and example

Answer 10

Term N is a fixed point of another term M just if MN≈N e.g. id n ≈ n

Question 11

Inversion

Answer 11

Suppose Γ⊢M:A is derivable then:
* If M is a variable x, then it must be that x:A ∈ Γ
* If M is a constant c, then it must be that c:A ∈ C
* If M is an application PQ, then there is a type B such that Γ ⊢ P : B → A and Γ ⊢ Q : B
* If M is an abstraction λx. P, then there are types B and C such that A = B → C, and Γ , x : B ⊢ P : C

Question 12

Proof involving AVB

Answer 12

Assume A is true for first case
Assume B is true for second case
Conclude with statement that holds in both cases

Question 13

Subject reduction

Answer 13

If Γ ⊢ M:A and M ->* N then Γ ⊢N:A

Question 14

Progess

Answer 14

If Γ ⊢M:A then either M is a value or there is some N such that M -> N

Question 15

Well-typed programs

Answer 15

If ⊢ M:A then M does not go wrong

Question 16

First Recursion Theorem

Answer 16

Every term has a fixed point