• Nie Znaleziono Wyników

1. Nie korzystaj ac ze znanych definicji dodawania, mno˙zenia, poprzednika, itp., napisa´

N/A
N/A
Protected

Academic year: 2021

Share "1. Nie korzystaj ac ze znanych definicji dodawania, mno˙zenia, poprzednika, itp., napisa´"

Copied!
15
0
0

Pełen tekst

(1)

1. Nie korzystaj ac ze znanych definicji dodawania, mno˙zenia, poprzednika, itp., napisa´

,

c lambda-termy definiuj ace funkcje f, g : N → N, gdzie

,

(a) f (n) = n

2

+ n + 1;

(b) g(n) = n

2

− n + 1.

Czy te funkcje s a definiowalne w rachunku lambda z typami prostymi? Czy s

,

a definio-

,

walne w polimorficznym rachunku lambda?

2. (a) Napisa´ c term Id typu ω

p→p

→ ω

p

definiuj acy na liczebnikach Churcha funkcj

,

e

,

identyczno´ sciow a (tj. taki, ˙ze Id n  n, dla dowolnego n.)

,

(b) Czy w rachunku lambda z typami prostymi istnieje kombinator J , kt´ ory definiuje funkcj e identyczno´

,

sciow a w N i ma typ ω

, p

→ ω

p→p

, gdzie p jest zmienn a typow

,

a?

,

(c) Czy istnieje taki kombinator typu ω

p

→ ω

q

, gdzie q jest zmienn a r´

,

o˙zn a od p?

,

3. Napisa´ c term H definiuj acy funkcj

,

e h(n) = n

, 2

− 2n + 5 w rachunku lambda bez typ´ ow,

nie wykorzystuj ac dodawania, mno˙zenia, poprzednika, itp.

,

4. Liczebniki Parigota, to kombinatory postaci P

n

= λxf. f P

n−1

(f P

n−2

(. . . (f P

0

x) . . .)), gdzie P

0

= K. Na przyk lad P

2

= λxf.f [λx

0

f

0

.f

0

Kx

0

](f Kx).

(a) Zdefiniowa´ c operacje nast epnika i poprzednika dla liczebnik´

,

ow Parigota.

(b) Nie u˙zywaj ac operator´

,

ow punktu sta lego zdefiniowa´ c rekursor , tj. taki term R, ˙ze:

RP

0

BF =

β

B oraz RP

n+1

BF =

β

F P

n

(RP

n

BF ) dla dowolnych term´ ow B, F i dowolnego n ∈ N.

(c) Zdefiniowa´ c operacj e dodawania dla liczebnik´

,

ow Parigota.

(d) Czy term P

2

jest typowalny w rachunku lambda z typami prostymi?

5. Skonstruowa´ c taki kombinator X, ˙ze

X(λyz.y(yz(yy))z) 

βη

K; oraz X(λyz.y(yz(yz))z) 

βη

S.

6. Skonstruowa´ c taki kombinator X, ˙ze

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

β

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

β

2.

7. Skonstruowa´ c taki term M , ˙ze M L =

β

true oraz M R =

β

false, gdzie

• L = λxy. x(λz. zx(λu. xxu))y;

• R = λx. x(λz. z(λy. xy)(λu. x(xz)u)).

8. Skonstruowa´ c taki kombinator X, ˙ze

X(λxz. x(λu.zu)(λyz. y(xyy)z)) 

β

true oraz X(λxz. xz(λy. y(xxy))) 

β

false.

9. Skonstruowa´ c taki kombinator X, ˙ze

X(λxy. x(λz.xz(xz))y) 

β

K oraz X(λx. x(λz.xz(xx))) 

β

S .

1Zadania pochodza g l´, ownie z egzamin´ow pisemnych i ´cwicze´n pandemicznych.

(2)

10. Skonstruowa´ c taki term M , ˙ze M L =

β

true oraz M R =

β

false, gdzie L = λx. x(λy. xx(yy(λz. zxy)))x;

R = λx. x(λy. xx(yy(λz. zyx)))x

11. Zdefiniowa´ c yakie kombinatory X

1

, X

2

, X

3

, ˙ze:

X

1

(λxy. x(xIx)(y(λy. xy)y)) =

β

I oraz X

1

(λxy. x(xIx)(y(λy. xx)y)) =

β

S;

X

2

(λxy. x(λz. zx)(λz. x(yyz)z)) =

β

true oraz X

2

(λxy. x(λy. yx)(λz. x(yyx)z)) =

β

false;

X

3

(λxyz. xz(yx(yxx)y)z) =

β

0 oraz X

3

(λxyz. xz(yx(yxy)y)z) =

β

1.

12. Niech Φ = λtxy. x(ty). Drzewo B¨ ohma termu YΦ ma tak a w lasno´

,

s´ c: prawie wszystkie zmienne wyst epuj

,

ace w wierzcho lkach drzewa s

,

a zwi

,

azane lambda-abstrakcjami znaj-

,

duj acymi si

,

e o 1 poziom wy˙zej (

,

” w odleg lo´ sci 1”). Poda´ c przyk lad termu, w kt´ orym

” odleg lo´ s´ c” mi edzy lambd

,

a i zwi

,

azan

,

a przez ni

,

a zmienn

,

a jest prawie zawsze r´

,

owna 2.

13. Skonstruowa´ c term M o takiej w lasno´ sci: drzewo B¨ ohma BT(M ) jest niesko´ nczone i ka˙zdy jego wierzcho lek ma wi ecej syn´

,

ow ni˙z mia l jego ojciec.

14. Skonstruowa´ c taki term M , ˙ze (patrz rysunek):

– drzewo B¨ ohma BT(M ) jest pe lnym drzewem binarnym;

– w korzeniu tego drzewa jest etykieta λx

0

x

1

. x

0

;

– w ka˙zdym wierzcho lku dowolnego poziomu k > 0 jest etykieta λx

k+1

. x

k

.

λx

0

x

1

. x

0

''

ww

λx

2

. x

1



λx

2

. x

1



λx

3

. x

2





λx

3

. x

2





λx

3

. x

2





λx

3

. x

2





λx

4

. x

3

λx

4

. x

3

λx

4

. x

3

λx

4

. x

3

λx

4

. x

3

λx

4

. x

3

λx

4

. x

3

λx

4

. x

3

. . . . . . . . . . . . . . . . . . . . . . . .

15. Niech M b edzie jak w zadaniu 14 i niech N = λx

, 0

x

1

. x

0

(λx

2

. x

1

(λx

3

. x

2

)). Czy istnieje taki kombinator T , ˙ze T N =

β

K, ale T M =

β

S? Je´ sli tak, to jaki?

16. Przy oznaczeniach z zadania 4 skonstruowa´ c taki kombinator M , ˙ze drzewo B¨ ohma

(3)

BT(M ) ma kszta lt jak na rysunku:

λx. x

zz $$

P

0

x

{{ !!

P

1

x

}} 

P

2

x

 

P

3

. . .

17. Napisa´ c taki term M , kt´ orego drzewo B¨ ohma ma na ka˙zdym poziomie n dok ladnie n li´ sci o etykiecie x

n

i jeden wierzcho lek o etykiecie λx

n+1

. x

n+1

, na przyk lad:

λx

1

. x

1

""

x

1

λx

2

. x

2

""

|| 

x

2

x

2

λx

3

. x

3

""

||vv 

x

3

x

3

x

3

λx

4

. x

4

.. .

18. Skonstruowa´ c taki term N , ˙ze drzewo B¨ ohma BT(N ) ma tylko jedn a ga l

,

,

z, oraz:

– je´ sli n = k

2

, to na poziomie n jest etykieta λx

k+1

. x

k

; – je´ sli k

2

< n < (k + 1)

2

, to na poziomie n jest etykieta x

k

.

Dla oszcz edno´

,

sci miejsca drzewo BT(N ) jest na rysunku przewr´ ocone na bok:

λx

1

. x

0

λx

2

. x

1

x

1

x

1

λx

3

. x

2

x

2

x

2

x

2

x

2

λx

4

. x

3

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

,

λx

0

.x

0

x

0

λx

1

.x

0

x

0

λx

1

.x

0

x

0

λx

1

.x

0

λx

2

.x

1

x

0

λx

1

.x

0

λx

2

.x

1

.. . .. . λx

3

.x

2

(4)

(Drugim argumentem zmiennej x

0

na lewej kraw edzi drzewa na g l

,

eboko´

,

sci k ma by´ c term T

k

= λx

1

. x

0

(λx

2

. x

1

(. . . (λx

k+1

. x

k

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

20. Skonstruowa´ c taki term M , ˙ze (patrz rysunek):

– drzewo B¨ ohma BT(M ) jest pe lnym drzewem binarnym;

– w korzeniu tego drzewa jest etykieta λx

0

. x

0

;

– w ka˙zdym wierzcho lku dowolnego poziomu k > 0 jest etykieta:

– λx

k

. x

k−1

, gdy k jest nieparzyste, – λx

k

. x

k−2

, gdy k jest parzyste.

λx

0

. x

0

))

uu

λx

1

. x

0

##

||

λx

1

. x

0

##

||

λx

2

. x

0





λx

2

. x

0





λx

2

. x

0





λx

2

. x

0





λx

3

. x

2

λx

3

. x

2

λx

3

. x

2

λx

3

. x

2

λx

3

. x

2

λx

3

. x

2

λx

3

. x

2

λx

3

. x

2

. . . . . . . . . . . . . . . . . . . . . . . . 21. Zbada´ c, czy Y =

β

Θ, gdzie:

Y = λf. (λx. f (xx))(λx. f (xx));

Θ = (λxf. f (xxf ))(λxf. f (xxf )).

22. Pokaza´ c, ˙ze istnieje niesko´ nczenie wiele kombinator´ ow punktu sta lego, i ˙ze ˙zaden z nich nie ma postaci normalnej.

23. Jaka ni´ c jest interpretacj a termu I w modelu D

,

? 24. Jaka ni´ c jest interpretacj a termu K w modelu D

,

?

25. Niech omega = [[λx. xx]] w modelu D

. Pokaza´ c, ˙ze omega

0

= ⊥ i omega

1

= id, oraz ˙ze omega

n+1

(d) = ϕ

n−1

(d(ψ

n−1

(d)))), dla d ∈ D

n

. Wywnioskowa´ c st ad, ˙ze [[Ω]] = ⊥.

,

26. Jakie zbiory s a interpretacjami term´

,

ow K, ω i Ω w modelu P

ω

?

27. Pokaza´ c, ˙ze P

ω

6|= 1 = I i wywnioskowa´ c, ˙ze model P

ω

nie jest ekstensjonalny.

28. Pokaza´ c, ˙ze kazdy term w postaci normalnej jest typowalny w systemie BCD bez u˙zycia sta lej ω.

29. Kt´ ore z nast epuj

,

acych term´

,

ow s a typowalne w rachunku lambda z typami prostymi?

,

W jaki spos´ ob? A kt´ ore w innych systemach z typami?

(a) λxyz. z(xy)(yx)?

(b) λxyz. x(xy)(xy)?

(c) λxyz. x(xy)(zy)?

30. Kt´ ore z nast epuj

,

acych term´

,

ow

(5)

(a) λxy. xy(yx);

(b) λxy. xy(xy);

(c) λxy. xy(xyy);

(d) λxy.(λz. zz)(xy);

s a typowalne w rachunku lambda z typami

,

(a) prostymi?

(b) iloczynowymi?

(c) pozytywnymi rekurencyjnymi?

(d) polimorficznymi?

31. 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?

32. Czy termy λxyzu. x(xu)(zu)(yz) i λxyzu. x(yz)(zu)(xu) s a typowalne w rachunku typ´

,

ow prostych? A w typach iloczynowych bez omegi?

33. Ile term´ ow zamkni etych w postaci normalnej ma typ (p → q → r) → (p → q) → p → r ?

,

34. Czy istnieje kombinator (term zamkni ety) typu:

,

(a) ((((q → p) → q) → q) → p) → p?

(b) ((((p → q) → q) → q) → p) → p?

35. Czy istnieje term zamkni ety typu:

,

(a) ((p → q) → p) → p;

(b) ((((p → q) → p) → p) → q) → q?

36. W typie prostym τ wyst epuje tylko jeden typ atomowy p. Udowodni´

,

c, ze term zamkni ety

,

typu τ istnieje wtedy i tylko wtedy, gdy τ jest klasyczn a tautologi

,

a.

,2

37. Pokaza´ c, ˙ze dowolny typ prosty τ mo˙zna efektywnie (w czasie wielomianowym) prze- kszta lci´ c w typ prosty σ

τ

spe lniaj acy warunek:

,

Typ τ nie ma inhabitanta wtedy i tylko wtedy, gdy σ

τ

ma, z dok ladno´ sci a do βη-

,

konwersji, dok ladnie jednego inhabitanta

38. Poda´ c przyk lad λI-termu zamkni etego M , typowalnego w typach prostych, oraz takiego

,

typu τ , ˙ze 0 M : τ , ale istnieje tanie N , ˙ze M →

β

N i ` N : τ .

2Wskaz´owka: zauwa˙zy´c, ˙ze formu la postaci τ1→ · · · → τn→ p z jedna zmienn, a zdaniow, a p jest klasyczn, a, tautologia wtedy i tylko wtedy, gdy co najmniej jedna z formu l τ, inie jest klasyczna tautologi, a.,

(6)

39. Prosz e poda´

,

c przyk lad ci agu term´

,

ow M

0

β

M

1

β

· · · →

β

M

n

, o tej w lasno´ sci,

˙ze w systemie typ´ ow prostych zachodzi ` M

i

: τ

i

dla pewnych typ´ ow τ

i

, ale je´ sli j > i, to 0 M

i

: τ

j

. (Ka˙zdy krok beta-redukcji dodaje jaki´ s nowy typ.)

Czy termy M

i

maj a t

,

e sam

,

a w lasno´

,

s´ c w systemie BCD typ´ ow iloczynowych?

40. Skonstruowa´ c taki term M , kt´ oremu w otoczeniu x : p, y : q mo˙zna przypisa´ c (w systemie typ´ ow prostych) wy l acznie typ ((p → q) → p) → p.

,

41. Niech Γ = {a : p, b : q}. Skonstruowa´ c taki term M , ˙ze Γ ` M : τ wtedy i tylko wtedy, gdy τ = ((p → q) → p) → q → p.

42. Poda´ c przyk lad takiego ci agu typ´

,

ow prostych τ

n

d lugo´ sci O(n), ˙ze ka˙zdy zamkni ety

,

term M w postaci normalnej,

3

kt´ ory jest typu τ

n

, ma d lugo´ s´ c co najmniej O(2

n

).

43. Niech F = λnf xa

1

a

2

. n(λyz

1

z

2

. yz

2

z

1

)(λz

1

z

2

. z

1

)(xa

1

a

2

)(f xa

1

a

2

).

(a) Czy term F 5 ma posta´ c β-normaln a? A posta´

,

c βη-normaln a? Je´

,

sli tak, to jak a?

,

(b) Czy term F jest typowalny w rachunku lambda z typami prostymi?

44. Niech f (n) = if (n = 1) then 3 else 2. Czy funkcja f jest:

(a) definiowalna w beztypowym rachunku lambda?

(b) β-definiowalna w rachunku z typami prostymi?

(c) sko´ snie β-definiowalna w rachunku z typami prostymi?

(d) βη-definiowalna w rachunku z typami prostymi?

Czy dla funkcji g(n) = if (n = 0) then 3 else 2 odpowiedzi s a takie same?

,

45. Niech g(x) = x

2

− 4x + 4, dla x ∈ N. 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 ω

p

→ ω

p

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

, τ

→ ω

p

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

,

termu typu ω → ω?

46. Term F jest •-testem parzysto´ sci (symbol • zast epuje β lub βη), gdy dla dowolnego n

,

zachodzi F n =

0, gdy n jest parzyste i F n =

1, gdy n jest nieparzyste.

(a) Skonstruowa´ c term F , kt´ ory jest β-testem parzysto´ sci.

(b) Czy istnieje β-test parzysto´ sci, kt´ ory jest typu ω

p

→ ω

p

?

(c) Skonstruowa´ c βη-test parzysto´ sci

4

typu ω

τ

→ ω

τ

, gdzie τ = p → p → p.

47. Dla n ∈ N, niech g(n) = if n parzyste then n else n + 1. Napisa´c lambda-term, kt´ory definiuje funkcj e g (ze wzgl

,

edu na β-konwersj

,

e) i ma typ ω → ω w polimorficznym ra-

,

chunku lambda. Czy ta funkcja jest definiowalna w rachunku lambda z typami prostymi za pomoc a termu typu ω

, p

→ ω

p

? Czy mo˙zna j a zdefiniowa´

,

c sko´ snie (z pomoc a termu

,

typu ω

τ

→ ω

p

dla pewnego τ ) je´ sli dopu´ scimy βη-konwersj e?

,

3Wersja z du˙za gwiazdk, a: nale˙zy opu´, sci´c s lowa

”w postaci normalnej”.

4Wskaz´owka: co to jest n(λf xy. f yx)K?

(7)

48. Pokaza´ c, ˙ze funkcja λλn. 3n

2

−7n+4 jest definiowalna sko´snie (tj. termem typu ω

τ

→ ω

p

, dla jakiego´ s τ ).

49. Pokaza´ c, ˙ze funkcja λλn. if n ≤ 2 then n else n + 2 jest definiowalna ze wzgl edu na

,

βη-konwersj e termem typu ω

, τ

→ ω

τ

, dla jakiego´ s τ .

50. Niech C = (λF xy. xF (λz. 1)(yF (λz. 0)))(λf g.gf ). Jak a funkcj

,

e z N

, 2

do N definiu- je ten term? Ile krok´ ow redukcji (z dok ladno´ sci a do sta lego czynnika) potrzeba do

,

obliczenia warto´ sci tej funkcji dla danych argument´ ow? Czy term C jest typowalny w rachunku typ´ ow prostych? Czy dla jakiego´ s τ ma typ ω

τ

→ ω

τ

→ ω

τ

, gdzie ω

τ

= (τ → τ ) → τ → τ ? Je´ sli nie, to czy istnieje term typu ω → ω → ω, definiuj acy t

,

e

,

sam a funkcj

,

e? A term typu ω

, τ

→ ω

τ

→ ω

ρ

, dla r´ o˙znych τ, ρ?

51. Czy nast epuj

,

ace formu ly s

,

a twierdzeniami logiki intuicjonistycznej?

,

(a) ((p → q) → r) → (p → r) → r?

(b) ((((p → q) → r) → (p → r) → r) → q) → q?

52. Czy nast epuj

,

ace formu ly s

,

a twierdzeniami logiki intuicjonistycznej:

,

(a) ((((q → p) → q) → q) → p) → p?

(b) ((((p → q) → q) → q) → p) → p?

53. Czy nast epuj

,

ace formu ly s

,

a twierdzeniami logiki intuicjonistycznej:

,

(a) ((P → Q) → P ) → ((Q → P ) → P ) → P ;

(b) ((P → Q) → Q) → P → Q;

(c) (S → Q → R) → ((S → R) → P ) → ((Q → R) → P ) → P .

54. Niech ∼α oznacza implikacj e α → •, gdzie • jest ustalon

,

a zmienn

,

a zdaniow

,

a r´

,

o˙zn a od

,

zmiennych p, q, r, s. Kt´ ora z nast epuj

,

acych formu l jest twierdzeniem intuicjonistycznym?

,

(a) ((p → q) → r) → ((q → s) → r) → r.

(b) ((∼p → ∼q) → ∼r) → ((∼q → ∼s) → ∼r) → ∼r.

55. Pokaza´ c, ˙ze term λx. xx ma niesko´ nczenie wiele r´ o˙znych typ´ ow w systemie BCD. (Nie liczymy instancji tego samego schematu, jak np. typy p ∩ (p → q) → q i r ∩ (r → (r → s)) → r → s.)

56. Czy istnieje taki kombinator punktu sta lego, kt´ oremu mo˙zna przypisa´ c typ w systemie typ´ ow iloczynowych λ

∩≤

(bez omegi)? A w systemie BCD (czyli w systemie λ

∩≤ω

)?

57. Czy kombinatorowi Y = λf. (λx. f (xx))(λx. f (xx)) mo˙zna w systemie BCD przypisa´ c jaki´ s typ r´ o˙zny od ω? Czy Y ma w tym systemie typ (p → p) → p ?

58. Dlaczego w systemie BCD przyjmuje si e aksjomat ω ≤ ω → ω? A dlaczego nie przyjmuje

,

si e aksjomatu σ → τ ∩ ρ ≤ (σ → τ ) ∩ (σ → ρ)?

,

59. Udowodni´ c, ˙ze je´ sli F

1

i F

2

s a filtrami w algebrze T typ´

,

ow iloczynowych, to filtrem jest

te˙z zbi´ or F

1

· F

2

= {τ | σ → τ ∈ F

1

dla pewnego σ ∈ F

2

}.

(8)

60. Niech τ = ∀r(∀q(q → r) → r) i niech σ = ∀p((τ → p) → p). Napisa´ c takie termy there : τ → σ i back : σ → τ , ˙ze w systemie F zachodzi r´ owno´ s´ c I =

β

λx

τ

back (there x).

Czy ka˙zdy term zamkni ety typu σ jest beta-r´

,

owny wyra˙zeniu postaci there(N )?

61. W systemie F definiujemy produkt τ × % jako τ × % = ∀p((τ → % → p) → p).

Para uporz adkowana hM

, τ

, N

%

i to term Λpλx

τ →%→p

. xM N . Poda´ c przyk lad takich typ´ ow τ i %, ˙ze typ τ × % ma

” za du˙zo element´ ow” tj. istnieje term zamkni ety tego

,

typu w postaci normalnej, kt´ ory nie jest par a uporz

,

adkowan

,

a.

,

62. Udowodni´ c, ˙ze system G¨ odla T mo˙zna interpretowa´ c w systemie Girarda F. Jak wiadomo, w systemie F, (czyli w polimorficznym rachunku lambda) mo˙zna reprezentowa´ c liczby naturalne jako termy zamkni ete typu ω = ∀p((p → p) → (p → p)). Nale˙zy zdefiniowa´

,

c polimorficzny rekursor, tj. term zamkni ety

,

R : ∀p [(ω → p → p) → (ω → p → p)], kt´ ory dla dowolnego typu σ spe lnia warunki

RσM (succ n)N =

β

M n(RσM nN ) oraz RσM 0N =

β

N ,

gdzie n jest dowolnym liczebnikiem, a symbol succ oznacza term reprezentuj acy operacj

,

e

,

nastepnika. Inaczej m´ owi ac, term Rσ ma si

,

e zachowywa´

,

c jak rekursor R

σ

w systemie T.

63. Napisa´ c term typu ω → ω, kt´ ory definiuje w systemie F w stylu Churcha dzielenie ca lkowite przez trzy.

64. Czy ka˙zda funkcja obliczalna jest definiowalna w systemie F?

Rozwi azania

,

1: Definicje funkcji f stanowi term λnλf λx. f (n(nf )(nf x)). Funkcja f jest wielomianem, wi, ec jest, definiowalna w typach prostych.

Definicja funkcji g jest trudniejsza. Przypomnijmy najpierw, ˙ze pare hM, N i mo˙zna reprezentowa´, c przez λz. zM N , a rzutowania definiowa´c jako Π1(M ) = M (λuv. u), Π2(M ) = M (λuv. v). Niech F = λp. hλf x. (f (nf x), λf x. mf (nf (nf x))i. Term F ma w lasno´s´c F hn, mi =βhn + 1, m + 2 · ni dla dowolnych liczebnik´ow Churcha n i m. Poniewa˙z g(n + 1) − g(n) = 2n, dla n ∈ N, wiec funkcja g jest, definiowana termem λn. Π2(nF h0, 1i).

Funkcja g nie jest wielomianem warunkowym, bo nie istnieje taki wielomian h o wsp´o lczynnikach naturalnych, ˙ze g(n) = h(n) dla wszystkich n > 0. (Dwa r´o˙zne wielomiany stopnia co najwy˙zej k nie moga si, e zgadza´, c w wiecej ni˙z k punktach.) Zatem nie jest definiowalna w typach prostych. Ale, jest definiowalna sko´snie, bo para liczebnik´ow typu ωp ma typ τ = (ωp → ωp → ωp) → ωp. Wtedy operacja G ma typ τ → τ , a term M ma typ ωτ → ωp.

Funkcja g jest definiowalna w systemie F, gdzie para liczebnik´ow typu ω ma typ ω ∧ ω, czyli typ

∀p. (ω → ω → p) → p. Je´sli n ma polimorficzny typ ω, to wyra˙zenie nGh0, 1iπ2 te˙z ma typ ω.

2a: Jedna z mo˙zliwo´sci: Id = λnωp→pfp→pxp. n(λgp→pzp. f (gz))Ip→px.

2b: Nie istnieje. Poniewa˙z ωp→p = ωp → ωp, wiec term J ma typ ω, p → ωp → ωp, czyli powinien w zwyk lym sensie definiowa´c wielomian warunkowy dw´och zmiennych. Jednak ˙zadamy aby J m =, β m, skad J mnf x =, βmnf x =βnm(f )x. Zatem J musia lby definiowa´c funkcje wyk ladnicz, a, kt´, ora nie jest wielomianem warunkowym.

2c: Te˙z nie istnieje. Bez straty og´olno´sci mo˙zna za lo˙zy´c, ˙ze J : ωp → ωq jest w postaci normalnej, czyli J = λnωpλfq→qλxq. M , gdzie term M jest typu q. Wtedy albo M = x albo M = f M0, gdzie M0 te˙z ma typ q. I tak dalej, wiec J = λn, ωpλfq→qλxq. f (f (. . . (f x) . . . )) definiuje funkcje sta l, a.,

(9)

3: Zacznijmy od operacji G = λp. hλf x. f (f (p true f x), λf x. p true f (p false f x)i. Dla p = hm, ni mamy Gp  hm + 2, m + ni. Dlatego k-krotna iteracja G, zaczynajaca si, e od pary h1, 4i daje, w wyniku h1 + 2k, h(k+1)i. Trzeba jeszcze dobrze zacza´,c i zdekodowa´c wynik, na przyk lad w ten spos´ob: H = λn. n(λp. p true (λz. Gp) h1, 4i) h0, 5ifalse. Sens: zaczynajac od p := h0, 5i wykonujemy, petl, e for i = 1 to n do if p true = 0 then h1, 4i else Gp, a wynik rzutujemy na 1. wsp´, o lrzedn, a., 4: Poprzednik to pred = λp. pKK, nastepnik to succ = λpxf. f p(pxf ). Rekursor to po prostu I,, dodawanie to add = λpq. pq(λxy. succ y). Niech ν0= t → s → t, oraz νn+1= t → [νn→ t → t] → t.

Typem termu P2jest ν2.

5: Nale˙zy zastosowa´c technike B¨, ohm-out . Otrzymamy wtedy np.

X = λx.x(λuv.hu, vi)(λuvw.S)π1π21KIπ1. Sprawdzamy poprawno´s´c rozwiazania. Przyjmijmy nast, epuj, ace oznaczenia:,

M = (λyz.y(yz(yy))z), N = (λyz.y(yz(yz))z), Q = λuvw.S, P = λuv.hu, vi.

Aplikacja M P Q redukuje sie do hhQ, λw.hP, wii, Qi. Po zaaplikowaniu tego termu do argument´, ow π1, π2, I, π1 dostajemy kolejno hQ, λw.hP, wii, λw.hP, wi, hP, Ii i wreszcie P . Tymczasem aplikacja M (λuv.hu, vi)Qπ1π21podobnie redukuje sie do Q. Pozostaje sprawdzi´, c, ˙ze P KIπ1 hK, Iiπ1 K.

6: Na przyk lad X = λu. uT T0π23π13123π31, gdzie T = λxyz. hx, y, zi oraz T0 = λxyz. hy, x, zi.

7: Szukanym termem jest na przyk lad M = λx. x true I false I (λx. true) I false.

8: Na przyk lad X = λv. v(λxy. hx, yi) I π2I π1(λxy. true) false π2, gdzie hx, yi, π1 i π2 oznaczaja, odpowiednio termy λz. zxy, λxy. x i λxy. y.

9: Na przyk lad X = λv. v(λxy. hx, yi)Iπ1(λxyz. K)π21II(λxy. S).

10: Na przyk lad λX. XPKK0K0K true(λz. false)K, gdzie P = λxyz. zxy, K0 = λxy. y.

12: Drzewo B¨ohma termu YΦ ma tylko jedna ga l,,z: λx0x1. x0(λx1. x0(λx2. x1. . . Zwiazek mi, edzy, poddrzewem T (xn) zaczynajacym si, e od λx, n+1 i poddrzewem T (xn+1) zaczynajacym si, e od λx, n+2, mo˙zemy zapisa´c tak: T (xn) = λxn+1. xn(T (xn+1)). To prowadzi do r´ownania sta lopunktowego postaci T = λxy. x(T y), czyli T = Φ T , kt´orego rozwiazaniem jest T = YΦ.,

Aby skonstruowa´c takie M , ˙ze BT(M ) = λx0x1x2.x0(λx3. x1(λx4. x2. . . , postepujemy podobnie,, otrzymujac r´, ownanie T = λxyz. x(T yz). Szukanym termem jest M = Y(λtxyz. x(tyz)).

13: Zacznijmy od tego, ˙ze operacja λn.n(λy.yz)x, zaaplikowana do liczebnika n, daje w wyniku n-krotna aplikacj, e xz . . . z. Je´, sli wiec M, n+1 ma drzewo, w kt´orym korze´n ma n + 1 syn´ow, to ko- rze´n drzewa BT(λx.n(λy.yMn+1)x) ma n syn´ow, ka˙zdy postaci BT(Mn+1). Pozostaje te konstrukcj, e, ujednostajni´c. Przyjmijmy F = λV λnλx.n(λy.y(V (succ n))x i niech M = YF 1. Latwo widzie´c, ˙ze:

M =βF (YF )1 =βλx.1(λy.y(YF 2)x =β λx.x(YF 2)

=βλx.x(λx0.2(λy.y(YF 3)x0)) =βλx.x(λx0.x0(YF 3)(YF 3)) =β· · ·

14: Poddrzewa B(xk) zaczepione w wewnetrznych wierzcho lkach tego drzewa s, a w istocie takie same,, r´o˙znia si, e tylko zmienn, a woln, a. Szukamy wi, ec takiego termu Q, ˙ze BT(Qx) = B(x). Term Q powinien, spe lnia´c r´owno´s´c Qx = λy. x(Qy)(Qy), zatem mo˙zemy przyja´,c Q = Y(λqxy. x(qy)(qy)). Poszukiwane rozwiazanie to M = λx, 0. Qx0.

15: Tak, na przyk lad T = λX. Xπ2(λxy. S)K.

16: Nasz term ma sie rozwija´, c tak: λx. xP0(xP1(. . . , wiec rozwi, a˙zemy r´, ownanie N px = xp(N (succ p)x).

Niech wiec N = Y(λnpx. xp(n(succ p)x)) i mo˙zemy zdefiniowa´, c M jako N P0.

17: Wez ly wewn, etrzne drzewa na g l, eboko´, sci n sa korzeniami drzew BT(M, n) pozostajacych ze sob, a, w zwiazku M, n = λx. xx . . . xMn+1, gdzie zmienna x wystepuje n + 1 razy. Prowadzi to do r´, ownania M = λnx. n(λy. yx)x(M (succ n)). Poszukiwany term, to M0= Y(λmnx. n(λy. yx)x(M (succ n)))0.

18: Wierzcho lki drzewa na g leboko´, sci k2 odpowiadaja termom Q, k z jedna zmienn, a woln, a x, k. Mamy taka zale˙zno´, s´c Qk =β λxk+1. x2k+1k (Qk+1). Przedstawiajac Q, k w postaci aplikacji Qkxk otrzymamy r´ownanie Qkxk =β λxk+1. xk(kxk(kxk(Q(succ k)xk+1))). Z pomoca kombinatora punktu sta lego,

(10)

znajdziemy rozwiazanie Q = Y(λqkxy. x(kx(kx(Q(succ k)y))). Poszukiwany term to N = λx, 1. Q0x0. 19: 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.

20: M = λx0. x0(N x0)(N x0), gdzie N = Y(λnxy. x(λz.x(nz)(nz))(λz.x(nz)(nz)).

21: Te dwa termy nie sa β-r´, owne. Gdyby tak by lo, to z twierdzenia Churcha-Rossera musia lby istnie´c taki term M , ˙ze Y β M i Θ β M . Term Θ redukuje sie w jednym kroku tylko do, λf. f (Θf ), gdzie T = λxf. f (xxf ), mamy wiec M = λf. f P , gdzie Θf , β P . Przez indukcje mo˙zna, pokaza´c, ˙ze wtedy P ma zawsze podterm Θ. Ale term M , jako redukt termu Y, musi by´c postaci λf. fk((λx. f (xx))(λx. f (xx))), co latwo wynika przez indukcje. ˙, Zaden taki term nie ma podtermu postaci Θ.

22: Niech δn = λx1x2· · · xn. f (x1x1· · · x1), gdzie x1 powtarza sie n + 1 razy., Wtedy taki term Yn = λf.δnδn· · · δn, gdzie δn powtarza sie n + 1 razy, jest kombinatorem punktu sta lego. Istotnie,, Yn(F ) =β DnDn· · · Dn, gdzie Dn= λx1x2· · · xn.F (x1x1· · · x1). A zatem Yn(F ) =β F (DnDn· · · Dn).

Przypu´s´cmy, ˙ze kombinator punktu sta lego L ma posta´c normalna. Oczywi´, scie musi to by´c abstrakcja λy. . . . , bo L jest kombinatorem. Dla dowolnej zmiennej x mamy x( Lx) = Lx. Oznacza to, ˙ze po normalizacji term Lx zaczyna sie od x, a wi, ec posta´, c normalna L musi by´c taka: λy.yL. Ale wstawiajac to do r´, owno´sci x( Lx) = Lx otrzymujemy x(xL0) = xL0 gdzie L0 = L[y := x]. To jest niemo˙zliwe bo mamy tu dwie r´o˙zne postaci normalne.

23: Jest to ni´c a = (an)n∈N, gdzie a0 = ⊥ ∈ D0 oraz ka˙zda z funkcji an : Dn−1 → Dn−1, dla n > 0 jest identyczno´sciowa. Jest to faktycznie ni´c, bo ψ0(a1) = ⊥ = a0, oraz ψn+1(an+2) = ψn◦ an+2◦ ϕn = ψn◦ idDn+1 ◦ ϕn = ψn◦ ϕn = idDn= an+1. Ponadto [[λx x]] · y = [[x]][x7→y]= y oraz a · y = sup{an+1(yn) | n ∈ N} = sup{yn | n ∈ N} = y, wiec teza wynika z ekstensjonalno´, sci modelu.

24: W modelu Delement k = [[K]] ma w lasno´s´c k · d · e = d, w szczeg´olno´sci je´sli d ∈ Dn+1, e ∈ Dn, to kn+2(d)(e) = (k · d)n+1(e) = (k · d · e)n= dn = ψn(d). W szczeg´olno´sci dla d ∈ D1 mamy k2(d) = λλa.ψ0(d) = λλa.d(⊥). Czyli k2 to funkcja numer 2 na naszym rysunku. Zatem k1= ψ1(k2) = idD0

i k0= ψ0(k1) = id(⊥) = ⊥, wiec k = (⊥, id, ,λλda.ψ0(d), λλda.ψ1(d), . . . ).

25: Skoro omega = [[λx. xx]], to omega · d = d · d, dla d ∈ D, w szczeg´olno´sci je´sli d ∈ Dn, to omegan+1(d) = (omega · d)n = (d · d)n = dn+1(·d) = ϕn(d)(d). Dla n = 0 wynika stad, ˙ze, omega1(d) = ϕ0(d)(d) = (λλa. d)(d) = d, czyli omega1 = id. Stad od razu omega, 0 = ψ0(id) = ⊥.

Dla n > 0 mamy omegan+1(d) = ϕn(d)(d) = ϕn−1(d(ψn−1(d)). Z powy˙zszego latwo dostajemy omegan+1(omegan) = ϕn−1(omegan(omegan−1)). Dalej poniewa˙z omega1(omega0) = id(⊥) = ⊥, wiec, [[Ω]] = sup{omegan+1(omegan) | n ∈ N} = ⊥.

26: W modelu Pω:

• [[K]] = graph(λλa.

”N× a”) = {(m, n) | n ∈

”N× en”} = {(m, (k, l)) | l ∈ em}.

• [[xx]]x7→a= fun(a)(a) = {m | ∃n(en⊆ a ∧ (n, m) ∈ a)}.

• [[ω]] = graph(λλa. fun(a)(a)) = {(x, m) | m ∈ fun(ex)(ex)}

= {(x, m) | ∃n(en ⊆ ex∧ (n, m) ∈ ex)}.

• [[Ω]] = [[xx]]x7→[[ω]]= {m | ∃n(en⊆ [[ω]] ∧ (n, m) ∈ [[ω]])}.

Przypu´s´cmy, ˙ze m ∈ [[Ω]] i niech n = min{n | en ⊆ [[ω]] ∧ (n, m) ∈ [[ω]]}. Ale skoro (n, m) ∈ [[ω]], to istnieje takie n0, ˙ze en0 ⊆ en ⊆ [[ω]] oraz (n0, m) ∈ en ⊆ [[ω]]. Sprzeczno´s´c, bo wtedy n0 < n. Zatem [[Ω]] = ∅ = ⊥.

27: Poniewa˙z Ix =β x oraz 1x =β λy.xy, wiec wystarczy je´, sli udowodnimy, ˙ze Pω 6|= x = λy.xy.

Niech v(x) = a. Wtedy [[x]]v = a. Natomiast [[λy.xy]]v = graph(g), gdzie g(b) = [[xy]]v[y7→b]= a · b = fun(a)(b) = {m | ∃k ∈ N(ek ⊆ b ∧ (k, m) ∈ a)}. A wiec [[λy.xy]], [x7→a] = {(n, m) | m ∈ g(en)} = {(n, m) | ∃k ∈ N(ek⊆ en∧ (k, m) ∈ a}.

(11)

Je´sli a jest niepustym zbiorem sko´nczonym, to [[λy.xy]]v, jest zbiorem niesko´nczonym, w szczeg´olno´sci [[λy.xy]]v 6= a. Istotnie, niech (k, m) ∈ a. Wtedy ka˙zda para (n, m) gdzie ek⊆ en nale˙zy do [[λy.xy]]v. Poniewa˙z Pω jest lambda-modelem, wiec spe lnia w szczeg´, olno´sci warunek [[λx.M ]]v· a = [[M ]]v[x7→a], dla dowolnych a i M . Stad dla dowolnych a, b ∈ P, ω mamy ([[1]] · a) · b = a · b = ([[I]] · a) · b. Gdyby model by l ekstensjonalny to mieliby´smy [[1]] · a = [[I]] · a, dla dowolnego a, i wreszcie [[1]] = [[I]].

28: Dow´od przez indukcje ze wzgl, edu na budow, e termu normalnego. Termy normalne s, a postaci, xN1. . . Nk lub λx. M . W pierwszym przypadku, z za lo˙zenia indukcyjnego mamy Γi ` Ni : τi dla ka˙zdego i. Wtedy Γ1& . . . &Γk, x : τ1 → . . . → τk → q ` xN1. . . Nk : q. W drugim przypadku, z za lo˙zenia indukcyjnego Γ ` M : σ. Je´sli x : τ ∈ Γ dla pewnego τ to Γ ` λx. M : τ → σ. Je´sli x nie wystepuje w Γ to z os labiania Γ, x : q ` M : σ i Γ ` λx. M : q → σ.,

29: Je´sli przez αx, αy, αz oznaczymy poszukiwane typy zmiennych x, y, z, to term (a) prowadzi do uk ladu r´owna´n αx = αy → β, αy = αx → γ, skad dostajemy r´, ownanie αx = (αx → γ) → β, kt´ore nie ma rozwiazania. Term (a) nie ma wi, ec typu prostego. Ale w rachunku z pozytywnymi typami, rekurencyjnymi ten term ma typ α → (α → r) → (q → r → s) → s, gdzie α = µp. (p → r) → q.

Dla termu (b) dostajemy r´ownania αx= αy → β = β → β → γ, skad wynika, ˙ze β = β → γ i znowu, nie ma rozwiazania. Tym razem jednak typowanie rekurencyjne nie jest pozytywne (typ β wyst, epuje, na negatywnej pozycji w β → γ).

Term (c) jest typowalny w typach prostych. Mamy tu r´ownania αx = αy → β, αx = β → δ → γ, αz = αy → δ, kt´ore mo˙zna rozwiaza´, c, przyjmujac α, y = β = δ → γ, αx = (δ → γ) → δ → γ, αz= (δ → γ) → δ. Term (c) ma wszystkie typy ((δ → γ) → δ → γ) → (δ → γ) → ((δ → γ) → δ) → δ.

Termy (a)–(c) sa postaciami normalnymi, s, a wi, ec typowalne w systemie z typami iloczynowymi, (zadanie 28). W polimorficznym rachunku lambda ka˙zdemu z nich mo˙zna przypisa´c typ ∀p p →

∀p p → ∀p p → q.

30: Pr´oba typowania termu (30a) prowadzi do uk ladu r´owna´n:

αx= αy→ β → γ, αy= αx→ β, (1)

kt´ory implikuje αx = (αx → β) → β → γ, a wiec nie ma rozwi, azania w typach prostych. Dla, termu (30b) mamy uk lad r´owna´n:

αx= αy→ β → γ = αy→ β, (2)

kt´ory te˙z nie ma rozwiazania, bo implikuje β = β → γ. Natomiast w przypadku termu (30c) dostajemy, unifikacje α, x= αy → β → γ = αy → αy → δ, kt´ora rozwi, azujemy przyjmuj, ac δ = β = α, y = p oraz αx= p → p → p. Oznacza to, ˙ze nasz term ma typ (p → p → p) → p → p.

R´o˙znica pomiedzy r´, ownaniami (1) i (2) polega na tym, ˙ze w przypadku (2) otrzymujemy r´ownanie β = β → γ, w kt´orym petla od β do β jest negatywna. A wi, ec term (30b) nie jest typowalny, w systemie pozytywnych typ´ow rekurencyjnych. Inaczej jest dla r´owna´n (1), gdzie mo˙zemy przyja´,c β = q, γ = r, αx= µp. (p → q) → q → r, αy = (µp. (p → q) → q → r) → q. Term (30a) ma wiec typ, (µp. (p → q) → q → r) → ((µp. (p → q) → q → r) → q) → r.

Term (30d) nie jest typowalny w systemie typ´ow prostych, ani pozytywnych typ´ow rekurencyjnych, bo zmienna z jest aplikowana sama do siebie. Jej domniemany typ αz musia lby wiec spe lnia´, c r´ownanie αz= αz→ β, kt´ore nie ma rozwiazania, i gdzie p, etla od α, zdo αz jest negatywna.

W polimorficznym rachunku lambda mo˙zna mu przypisa´c typ, bo ten term jest wytarciem termu Churcha λxq→∀p (p→p)λyq(λz∀p (p→p). z(r → r)zr)(xy), kt´ory ma typ (q → ∀p (p → p)) → q → r → r.

Wszystkie termy maja w lasno´, s´c silnej normalizacji, wiec s, a typowalne w systemie typ´, ow iloczyno- wych. Wszystkie opr´ocz (30d) sa nawet postaciami normalnymi, wi, ec s, a te˙z typowalne w systemie F., Na przyk lad, term (30a) ma miedzy innymi typ iloczynowy p ∧ (p → p → p) → p ∧ (p → p) → p,, a term (30b) ma typ (p → p → p) ∧ (p → p) → p → p. Oba termy maja za´, s typ polimorficzny (∀p p) → (∀p p) → p.

31: Domniemane typy proste αx, αy, αz, αuzmiennych x, y, z, u wystepuj, acych w termie 31a 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 31a nie jest typowalny w typach,

(12)

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 31b 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).

33: Jedynym takim termem jest S. Je´sli term M w postaci normalnej ma w pustym otoczeniu typ (p → q → r) → (p → q) → p → r to musi by´c abstrakcja M = λx. N (nie mo˙ze si, e zaczyna´, c od zmiennej wolnej, bo takich nie ma). Wtedy x : p → q → r ` N : (p → q) → p → r. Term N nie mo˙ze by´c aplikacja zmiennej x do jakich´, s argument´ow, bo musia lby mie´c wtedy typ q → r albo r. Zatem N = λy. P , gdzie x : p → q → r, y : p → q ` P : p → r. Term P te˙z nie mo˙ze by´c aplikacja (dlaczego?), wiec P = λz. Q, gdzie Q ma typ r w otoczeniu Γ = {x : p → q → r, y : p → q, z : p}. Jedyna, mo˙zliwo´s´c, to Q = xRT , gdzie R i T maja w Γ odpowiednio typy p i q. Jedyne takie termy to R = z, i T = yz.

34: Term λx(((q→p)→q)→q)→p. x(λy(q→p)→q. y(λzq. x(λy(q→p)→q1 z))) jest typu (52a).

Ale nie istnieje term zamkniety typu (52b). Gdyby taki term istnia l, to mia lby posta´, c normalna, wi, ec, wystarczy pokaza´c, ˙ze nie istnieje szukany term w postaci normalnej. Niech M bedzie najkr´, otszym takim termem. Musi on by´c abstrakcja postaci M = λx, (((p→q)→q)→q)→pN , gdzie N jest typu p, a wiec, N = xP dla pewnego P typu ((p → q) → q) → q. Term P musi by´c abstrakcja P = λy, (p→q)→qQ, gdzie Q jest typu q i musi by´c Q = yR dla pewnego R : p → q. Zatem R = λzp.T , gdzie T : q, ´sci´slej:

x : (((p → q) → q) → q) → p, y : (p → q) → q, z : p ` T : q,

i na dodatek T jest najkr´otszy mo˙zliwy (bo taki ma by´c term M ). Rozumujac podobnie jak wy˙zej,, otrzymamy, ˙ze T = y(λz1p.T1), gdzie T1: q. Niech teraz T2= T1[z1:= z]. Wtedy:

x : (((p → q) → q) → q) → p, y : (p → q) → q, z : p ` T2: q, a term T2 jest kr´otszy ni˙z T , sprzeczno´s´c.

35: Term zamkniety typu ((p → q) → p) → p nie istnieje. Gdyby taki term istnia l, to mia lby posta´, c normalna tego samego typu. Ta posta´, c normalna musia laby by´c taka: λx N , gdzie N spe lnia warunek x : (p → q) → p ` N : p. Jedyna mo˙zliwo´s´c to N = xM , gdzie x : (p → q) → p ` M : p → q.

Term M jest te˙z normalny, wiec jest albo aplikacj, a zmiennej do jakich´, s argument´ow albo abstrakcja., Oczywi´scie pierwsza mo˙zliwo´s´c odpada, mamy wiec M = λyP , gdzie x : (p → q) → p, y : p ` P : q., Poniewa˙z aplikacja postaci xQ ani postaci yQ nie mo˙ze by´c typu q, wiec takiego termu nie ma., Poszukajmy wiec termu zamkni, etego typu ((((p → q) → p) → p) → q) → q. Powinien wygl, ada´, c tak:

λx.xM , gdzie x : ((p → q) → p) → p) → q ` M : ((p → q) → p) → p. Zatem M = λy N gdzie x : ((p → q) → p) → p) → q, y : (p → q) → p ` N : p. Dalej N = yQ, gdzie Q jest takie, ˙ze

x : (((p → q) → p) → p) → q, y : (p → q) → p ` Q : p → q.

Bez straty og´olno´sci mo˙zemy przyja´,c Q = λz.R i ostatecznie mamy do rozwiazania zadanie, x : (((p → q) → p) → p) → q, y : (p → q) → p, z : p ` R : q.

Oczywi´scie powinni´smy mie´c R = xM0 gdzie M0 jest znowu typu ((p → q) → p) → p i osoba ma lej wiary mo˙ze sie w tym miejscu zniech, eci´, c. Ale teraz sytuacja jest inna, bo mamy deklaracje z : p, wi, ec, wystarczy przyja´,c M0= λu.z i ju˙z. Dostali´smy takiego inhabitanta: λx.x(λy.y(λz.x(λu.z))).

36: Je´sli zmienna p ma warto´s´c logiczna jeden, to ka˙zda formu la implikacyjna zbudowana z p te˙z, ma warto´s´c jeden. Dlatego taka formu la jest tautologia wtedy i tylko wtedy, gdy jest spe lniona przez, warto´sciowanie v(p) = 0. Poniewa˙z formu la τ1 → · · · → τn → p jest spe lniona przez v wtedy i tylko wtedy, gdy kt´ora´s z formu l τi nie jest spe lniona, wiec mamy r´, ownowa˙zno´s´c, o kt´orej mowa w przypisie.

Teraz udowodnimy przez indukcje, ˙ze typ σ = τ, 1→ · · · → τn→ p jest niepusty wtedy i tylko wtedy, gdy jest klasyczna tautologi, a., (⇒) Za l´o˙zmy, ˙ze M : σ. Je´sli σ nie jest tautologia, to wszystkie τ, i sa tau-, tologiami i z za lo˙zenia indukcyjnego istnieja kombinatory N, 1: τ1, . . . , Nn : τn. Zatem M N1. . . Nn: p, czyli zmienna typowa p ma inhabitanta. Ale wtedy istnia lby tak˙ze kombinator typu p w postaci nor- malnej, a takiego przecie˙z nie ma. (⇐) Je´sli σ jest tautologia, to kt´, ore´s τi= ρ1→ · · · → ρr→ p nie

(13)

jest tautologia, wi, ec tautologiami s, a wszystkie ρ, 1, . . . , ρr. Z za lo˙zenia indukcyjnego mamy kombinatory M1: ρ1, . . . , Mr: ρr, a wiec σ ma inhabitanta λx, 1. . . xn. xiM1. . . Mr.

37: Niech a 6∈ FV(τ ). Wtedy στ = (τ → a) → a → a. Ten typ ma zawsze inhabitanta λf x. x. Drugi musi mie´c d luga posta´, c normalna λf x. f M , gdzie f : τ → a, x : a ` M : τ . Ale poniewa˙z w typie τ, nie wystepuje w og´, ole zmienna a, wiec ani f ani x nie s, a wolne w M . Zatem ` M : τ .,

39: Mi = λyzx1. . . xn. yx1. . . xi((λv xi+1)(xi+1z)) . . . ((λv xn)(xnz))) oraz τi = σi → p → σi, gdzie σi= p → · · · → p → (p → p) → · · · → (p → p) → p i przes lanka (p → p) wystepuje n − i razy w σ, i. W systemie BCD wszystkie termy Mimaja typ τ, n, bo beta-konwersja zachowuje typy. Aplikacjom xjz mo˙zna przypisa´c typ ω tak˙ze wtedy, gdy xj ma typ p.

40: Mo˙zliwe rozwiazanie jest takie: λu.Kx(λv, 0v1v2z.v0(v1(zx))(v1y)(v2(uz))(v2x)). Istotnie, typ termu Kx . . . musi by´c taki jak typ x, czyli p. Natomiast typ u musi by´c postaci α → β gdzie α jest typem z oraz β = p, bo ta sama zmienna v2 jest aplikowana zar´owno do x jak i do uz, wiec te, dwa termy musza mie´, c te same typy. Podobnie, typem z musi by´c p → q, co jest zdeterminowane przez dwa pierwsze argumenty zmiennej v0(kt´ora odgrywa wy lacznie rol, e,

”kleju”, i kt´orej typ jest bez znaczenia).

41: Na przyk lad M = λxy. Ka(λzwv. w(x(λu. Kb(v(wa)(wu)(zy)(zb))))). Ten term musi mie´c typ postaci σ → τ → p, gdzie σ jest typem zmiennej x, a τ jest typem zmiennej y. Aplikacje zy i zb wymuszaja r´, owno´s´c τ = q. Podobnie, wszystkie wyra˙zenia, do kt´orych aplikowane jest w, musza by´, c typu p. Poniewa˙z Kb . . . ma typ q, wiec wyra˙zenie λu. Kb(v(wa)(wu)(zy)(zb)) jest typu p → q, sk, ad, wynika σ = (p → q) → p.

42: τn= (pn→pn→pn−1)→(pn−1→pn−1→pn−2)→· · ·→(p2→p2→p1)→(p1→p1→p0)→pn→p0. 43: Niech τ = p → p → p. Je´sli zmienne a1, a2, z1, z2 sa zawsze typu p, zmienne x, y sa typu τ ,, a zmienna f typu τ → τ , to F ma typ ωτ → ωτ. Wyra˙zenie F n redukuje sie do λf xa, 1a2. xa1a2, gdy n jest parzyste, i do λf xa1a2. f xa1a2, gdy n jest nieparzyste. Zatem postacia normaln, a termu F 5, ze wzgledu na beta-redukcje jest term λf xa, 1a2. f xa1a2, kt´ory jest eta-r´ownowa˙zny liczebnikowi 1.

Postacia βη-normaln, a jest kombinator I,

44a: Tak, jest definiowalna np. termem F = λn. n(λP hifzero(P π1)11, ifzero(P π1)23i)h0, 3iπ2, gdzie πi= λx1x2. xi oraz ifzero = λpqrλf x.p(λy.rf x)(qf x). Oczywi´scie hm, ni oznacza λz. zmn.

44b: Nie. Ta funkcja nie jest wielomianem warunkowym. Istotnie, dla argument´ow wiekszych od, zera, wielomian warunkowy jest po prostu wielomianem o wsp´o lczynnikach naturalnych, wiec jest, monotoniczny. Tymczasem f (1) = 3 > 2 = f (2). Poniewa˙z funkcja g jest wielomianem warunkowym, wiec w tym punkcie odpowiedzi si, e r´, o˙znia.,

44c: Tak. Funkcja F w zadaniu 44a ma typ ωτ → ωp, gdzie τ = (ωp→ ωp→ ωp) → ωp jest typem pary uporzadkowanej hm, ni, dla m, n : ω, p.

44d: Term λnf xa1a2a3. n(λyz1z2z3. yz2z3z3)(λz1z2z3. z1)(f2(x)a1a2a3)(f3(x)a1a2a3)(f2(x)a1a2a3) ma typ ωτ → ωτ, gdzie τ = p → p → p → p.

45: 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 de-, finiuje kombinator G = λx : ωτ. G0 typu ωτ → ωp. Jest ona te˙z definiowalna w systemie F, bo wystarczy G przerobi´c na polimorficzny term GF = λx : ω. Λp. G0[x := xτ ]. Pozostaje zdefiniowa´c G0 := x(λc : τ. hcπ24, cπ43, add (cπ34)(cπ44), succ(succ(cπ44))i)h4, 1, 0, 1iπ14, gdzie liczebniki sa typu ω, p, oraz πi4= λx1x2x3x4: ωp.xi.

46a: Beztypowy β-test parzysto´sci to na przyk lad term λn. n(λf xy. f yx)K01.

46b: Nie istnieje β-test parzysto´sci typu ωp → ωp, bo funkcja charakterystyczna parzysto´sci nie jest wielomianem warunkowym.

Aby to udowodni´c, nale˙zy zauwa˙zy´c, ˙ze ka˙zdy wielomian warunkowy o zmiennych ~x = x1, . . . , xn

mo˙zna przedstawi´c w postaci instrukcji warunkowej if xi = 0 then f (~x) else g(~x), gdzie f i g sa, wielomianami (o wsp´o lczynnikach naturalnych) lub wielomianami warunkowymi. Dlatego test parzys-

Cytaty

Powiązane dokumenty

Jeśli funkcja całkowita f powstaje przez składanie λ−definiowalnych funkcji całkowitych, to też jest

1C) (5 pkt) Obs luga dzia la artyleryjskiego ma 3 pociski. Prawdopodobie´nstwo trafienia do celu jednym pociskiem wynosi 0.6. Strzelanie ko´nczy si¸e w chwili trafienia do celu

, Na ile sposob´ ow mo˙zna jej nada´ c taki zwrot, aby po trzykrotnym odbiciu, nie przechodz ac , przez ´srodek, pi leczka przesz la przez po lo˙zenie pocz

57 Opisa´ c rozklad Hodge’a kohomologii produktu rozmaito´ sci rozmaito´ sci

Zadania o rozmaito´ sciach zespolonych

Kolokwium z Matematyki dla Chemik´ ow Przyk ladowe zadania.. (1) Definicja granicy

[r]

Wynik pomiaru pozwala znale´ z´ c okres r z prawdopodobie´ nstwem 24 proc.