− 4x + 4, dla x ∈ N. Prosz e napisa´

Egzamin z rachunku lambda, 20 czerwca 2020

1. Niech g(x) = x

− 4x + 4, dla x ∈ N. Prosz e napisa´

c lambda-term definiuj acy funkcj

e g.

Czy ta funkcja jest definiowalna w rachunku lambda z typami prostymi za pomoc a

termu typu ω

→ ω

? Czy jest definiowalna sko´ snie (z pomoc a termu typu ω

→ ω

dla pewnego τ )? Czy jest definiowalna w polimorficznym rachunku lambda za pomoc a

termu typu ω → ω?

2. Prosz e skonstruowa´

c taki kombinator X, ˙ze

X(λxy. xx(xxxy)(λx. yx)) 

1 oraz X(λxy. xx(xyx(λx. yx))y) 

2.

3. Prosz e skonstruowa´

c taki term N , ˙ze drzewo B¨ ohma BT(N ) wygl ada tak:

λx

.x

x

OO OO OO O

oooooooo

λx

.x

x

tttttt

λx

.x

x

{{{{{

λx

.x

λx

.x

x

λx

.x

λx

.x

.. . .. . λx

.x

(Drugim argumentem zmiennej x

na lewej kraw edzi drzewa na g l

eboko´

sci k ma by´ c term T

= λx

. x

(λx

. x

(. . . (λx

. x

) . . .)) wysoko´ sci k.)

4. Czy termy

(a) λu.(λyw.w(xz)(xy))(zu);

(b) λu.(λyw.w(xz)(xy))(uz),

s a typowalne w rachunku lambda z typami prostymi? W rachunku typ´

ow iloczynowych

bez sta lej ω? W systemie F?

Rozwiazania_,

1: Funkcja g nie jest wielomianem warunkowym, wiec nie jest definiowalna w typie ω_{, p} → ω_p. Ale jest definiowalna sko´snie. Niech τ = (ω_p → ω_p → ω_p → ω_p → ω_p) → ω_p. Nasza funkcj_, e_, definiuje kombinator G = λx : ωτ. G⁰ typu ωτ → ωp. Jest ona te˙z definiowalna w systemie F, bo wystarczy G przerobi´c na polimorficzny term GF = λx : ω. Λp. G⁰[x := xτ ]. Pozostaje zdefiniowa´c G⁰ := x(λc : τ. hcπ₂⁴, cπ⁴₃, add (cπ₃⁴)(cπ⁴₄), succ(succ(cπ₄⁴))i)h4, 1, 0, 1iπ₁⁴, gdzie liczebniki sa typu ω_, p, oraz π_i⁴= λx1x2x3x4: ωp.xi.

2: Na przyk lad X = λu. uT T⁰π₂³π₁³123π³₁, gdzie T = λxyz. hx, y, zi oraz T⁰ = λxyz. hy, x, zi.

3: Zauwa˙zmy, ˙ze Tk+1 = λx1. x0(Tk[x0 := x1]), inaczej λx0. Tk+1 =β λx0x1. x0((λx0. Tk)x1). Mamy wiec T_, k =βk(λtx0x1. x0(tx1))(λx0x1. x0)x0.

Teraz zdefiniujemy N = λx0. Y(λzk. x0(z(succ k)Tk)0 u˙zywajac r´_, ownania Nk = x0Nk+1Tk.

4: Domniemane typy proste αx, αy, αz, αu zmiennych x, y, z, u wystepuj_, acych w termie 4a powinny_, spe lnia´c r´ownania: αx= αz→ β = αy → γ, αz= αu→ δ, αy= δ. Stad wynika α_, y = αz= αu→ αy, czyli αy musi by´c swoja w lasn_, a w la´_, sciwa podformu l_, a. Zatem term 4a nie jest typowalny w typach_, prostych. W systemie F ma typ p → (p → p → p) → p w otoczeniu {z : ∀p. p, x : p → p} bo powstaje przez wycieranie typ´ow z takiego termu Churcha: λu : p (λy : p λw : p→p→p. w(x(zp))(xy))(z(p→p)u).

A skoro jest silnie normalizowalny, to jest te˙z typowalny w typach iloczynowych bez pomocy omegi.

Z termem 4b sprawa jest prostsza. W otoczeniu {z : p, x : p → p} ma typ (p → p) → (p → p → p) → p, bo powstaje przez wycieranie typ´ow z termu λu : p→ p (λy : p λw : p→p→p. w(xz)(xy))(uz).