M : τ → σ Γ ` M : τ → σ Γ ` N : τ Γ ` M N : σ Γ ` B : int Γ ` M : τ Γ ` N : τ Γ ` ifzero B then M else N : τ Γ, x : τ ` M : τ Γ ` fix x:τ

P. Urzyczyn: Materia ly do wyk ladu z semantyki Uproszczony¹ jezyk PCF_,

Sk ladnia: Poni˙zej Γ oznacza otoczenie typowe, czyli zbi´or deklaracji postaci (x : τ ).

Γ, x : τ ` x : τ Γ ` 0 : int Γ ` succ : int → int Γ ` pred : int → int Γ, x : τ ` M : σ

Γ ` λx : τ. M : τ → σ

Γ ` M : τ → σ Γ ` N : τ Γ ` M N : σ Γ ` B : int Γ ` M : τ Γ ` N : τ

Γ ` ifzero B then M else N : τ

Γ, x : τ ` M : τ Γ ` fix x:τ. M : τ

Skr´oty: Ω_τ = fix x:τ. x, n = succⁿ(0). Tam gdzie mo˙zna pomijamy typy w wyra˙zeniach.

Semantyka ma lych krok´ow:

W jezyku PCF (w wersji CBN) mamy sze´_, s´c rodzaj´ow redeks´ow : pred(n + 1) ⇒ n pred(0) ⇒ 0

(λx. M )N ⇒ M [N/x] fix x. M ⇒ M [fix x. M/x]

ifzero 0 then M else N ⇒ M ifzero n + 1 then M else N ⇒ N Konteksty ewaluacyjne definiujemy pseudo-gramatyka_,

E[ ] ::= [ ] | E[ ]N | succ E[ ] | pred E[ ] | ifzero E[ ] then M else N

Warto´s´c to liczebnik n, sta la pred lub succ, lub abstrakcja. Ka˙zdy term, kt´ory nie jest warto´scia, mo˙zna jednoznacznie przedstawi´_, c w postaci E[R], gdzie R jest redeksem lub zmien- na. (Dow´_, od przez latwa indukcj_, e.)_,

Zauwa˙zmy, ˙ze termy postaci E[Ω] redukuja si_, e same do siebie._,

Przyjmujemy M →<sub>`</sub> N , gdy M = E[R] oraz N = E[L] dla pewnej regu ly R ⇒ L. Jak zwykle, notacja ` oznacza domkniecie przechodnio-zwrotne relacji →_{, `</sub>, a notacja =<sub>`} odpowiednia_, relacje r´_, ownowa˙zno´sci. Indeks <sub>`</sub> opuszczamy tam, gdzie mo˙zna. Napis Γ ` M = N : τ oznacza, ˙ze M =<sub>`</sub>N oraz Γ ` M : τ i Γ ` N : τ .

Semantyka du ˙zych krok´ow (dla term´ow zamknietych):_, Definiujemy V ⇓ V , gdy V jest warto´scia, oraz:_,

M ⇓ 0 pred M ⇓ 0

M ⇓ n + 1 pred M ⇓ n

M ⇓ n succ M ⇓ n + 1 M ⇓ 0 P ⇓ V

ifzero M then P else Q ⇓ V

M ⇓ n + 1 Q ⇓ V ifzero M then P else Q ⇓ V

1Zwykle dodaje sie typ bazowy bool i normalny_,

”if”. Mo ˙zna te ˙z doda´c np. produkt kartezja´nski itp.

M ⇓ λx A A[N/x] ⇓ V M N ⇓ V

M [fix x. M/x] ⇓ V fix x. M ⇓ V

Semantyka ma lych krok´ow jest r´ownowa˙zna semantyce du˙zych krok´ow w nastepuj_, acym sensie:_, Fakt 1 Warunki M ⇓ V i M  V sa r´_, ownowa˙zne.

Dow´od: Z lewej do prawej prosta indukcja ze wzgledu na wyprowadzenie M ⇓ V . Z prawej_, do lewej indukcja ze wzgledu na liczb_, e krok´_, ow redukcji. Krok indukcyjny wymaga pokazania,

˙ze je´sli M → M⁰ ⇓ V to M ⇓ V .

Symulacje: Relacja aplikacyjnej symulacji M v^a N zachodzi pomiedzy zamkni_, etymi ter-_, mami M i N (tego samego typu), gdy dla dowolnych term´ow zamknietych ~_, N :

je´sli M ~N : int, oraz M ~N ⇓ n, to tak˙ze N ~N ⇓ n.

Domkniecie quasiporz_, adku v_, ^a do relacji r´ownowa˙zno´sci oznaczamy przez ≡^a i nazywamy r´ownowa˙zno´scia aplikacyjn_, a._,

Symulacja obserwacyjna M v N ma miejsce wtedy, gdy dla dowolnego kontekstu C_{[ ]}, z tego,

˙ze C_{[M ]} ⇓ n wynika C_{[N ]} ⇓ n. Napis M ≡ N oznacza, ˙ze zachodza obie symulacje M v N_, oraz N v M ; m´owimy wtedy, ˙ze M i N sa obserwacyjnie r´_, ownowa˙zne.

Fakt 2 (Lemat kontekstowy)

Relacje obserwacyjnej i aplikacyjnej symulacji (r´ownowa˙zno´sci) sa takie same._,

Dow´od: Za l´o˙zmy, ˙ze M v^a N i C_{[M ]} ⇓ n. Dowodzimy, ˙ze C_{[N ]} ⇓ n, przez indukcje_, ze wzgledu na definicj_, e relacji ⇓. S_, a dwa g l´_, owne przypadki. Pierwszy dotyczy kontekstu z redeksem czo lowym, np. C_{[M ]}= (λx P_{[M ]})Q_{[M ]}R~_{[M ]}. Wtedy mo˙zemy zastosowa´c za lo˙zenie indukcyjne do termu C_{[M ]}⁰ = P_{[M ]}[Q_{[M ]}/x] ~R_{[M ]} i otrzyma´c P_{[N ]}[Q_{[N ]}/x] ~R_{[N ]} ⇓ n.

Drugi przypadek jest wtedy, kiedy C_{[ ]} = [ ]P_{[ ]}Q~_{[ ]}, czyli C_{[M ]} = M P_{[M ]}Q~M. Rozpatrzmy kontekst D_{[ ]} = M P_{[ ]}Q~_{[ ]}. Wtedy D_{[M ]} = C_{[M ]} oraz D_{[N ]} = M P_{[N ]}Q~_{[N ]}. Poniewa˙z to nie jest liczebnik, wiec kontekst D_{, [ ]} musi mie´c redeks czo lowy i stosuje sie do niego poprzedni_, przypadek. Zatem D_{[N ]} ⇓ n. Teraz korzystamy z tego, ˙ze M v^a N i dostajemy C_{[N ]} ⇓ n.

Pozosta le przypadki sa latwe._,

Wniosek 3 Dla ka˙zdego M zachodzi Ω v M , bo zawsze Ω ~N 6⇓.

Semantyka denotacyjna: Dziedziny semantyczne to D_int= N⊥, oraz D_{τ →σ} = [D_τ → D_σ].

Poni˙zej zak ladamy, ˙ze ρ(x) ∈ Dτ, gdy (x : τ ) ∈ Γ.

[[x]]ρ= ρ(x), [[0]]ρ= 0, [[succ]]ρ(n) = n + 1, [[succ]]ρ(⊥) = ⊥ [[pred]]_ρ(n + 1) = n, [[pred]]_ρ(0) = 0, [[pred]]_ρ(⊥) = ⊥

[[M N ]]_ρ= [[M ]]_ρ([[N ]]_ρ), [[λx. M ]]_ρ(d) = [[M ]]_ρ[x7→d]

[[fix x:τ. M ]]_ρ= lfp(λλd. [[M ]]ρ[x7→d])

[[ifzero B then M else N ]]ρ=







⊥, je´sli [[B]]_ρ= ⊥;

[[M ]]_ρ, je´sli [[B]]_ρ= 0;

[[N ]]ρ, w przeciwnym przypadku.

Fakt 4 (Poprawno´s´c) Je´sli M =_` N , to [[M ]] = [[N ]].

Z powy˙zszego wynika w szczeg´olno´sci, ˙ze je´sli M ⇓ n, to [[M ]] = n.

Aproksymowanie punktu sta lego: Dla dowolnego M definiujemy fix⁰x. M = Ω, fix^k+1x. M = M [fix^kx. M/x].

Lemat 5 Dla dowolnego M i dowolnego k:

1. fix^kx. M v fix x. M ;

2. [[fix x. M ]] = sup_k[[fix^kx. M ]].

Dow´od: (1) Indukcja ze wzgledu na k. Korzystamy z tego, ˙ze zawsze Ω v N , i z tego, ˙ze_, N1v N₂ implikuje C[N1] v C[N2]. (2) Natychmiast z tw. o punkcie sta lym.

Termy obliczalne: Dla dowolnego τ definiujemy zbi´or term´ow zamknietych [τ ] typu τ :_,

• [int] = {M : int | M ⇓ lub [[M ]] = ⊥};

• [τ → σ] = {M : τ → σ | ∀N (N ∈ [τ ] → M N ∈ [σ]) }.

Elementy zbioru [τ ] nazywamy termami obliczalnymi w τ . Je´sli x : τ₁, . . . , x : τ_n` M : τ , to M jest obliczalny, gdy dla dowolnych N1 ∈ [τ₁], . . . , Nn∈ [τ_n] zachodzi M [N1/x1. . . Nn/xn] ∈ [τ ].

Term M [N1/x1. . . Nn/xn] ∈ [τ ] nazwiemy obliczalna instancj_, a termu M ._,

Lemat 6 Term M jest obliczalny wtedy i tylko wtedy, gdy dla dowolnej obliczalnej instancji M⁰ termu M i dowolnych obliczalnych i zamknietych term´_, ow ~N :

je´sli M⁰N : int, to albo [[M~ ⁰N ]] = ⊥ albo M~ ⁰N ⇓.~ Fakt 7 (S laba adekwatno´s´c) Je´sli [[M ]] = n to M ⇓ n.

Dow´od: Wystarczy udowodni´c, ˙ze ka˙zdy term jest obliczalny. Dow´od (opuszczony) jest przez indukcje ze wzgl_, edu na budow_, e termu. W przypadku termu postaci fix x. M , korzys-_, tamy z r´owno´sci [[fix x. M ]] = sup_k[[fix^kx. M ]].

Wniosek 8 (Adekwatno´s´c) Je´sli [[M ]] = [[N ]] to M i N sa obserwacyjnie r´_, ownowa˙zne.

Dow´od: Na mocy

”lematu kontekstowego” wystarczy wykaza´c r´ownowa˙zno´s´c aplikacyjna._, Ta wynika za s labej adekwatno´sci, bo [[M ~P ]] = [[N ~P ]] dla dowolnych ~P .

R´ownoleg la alternatywa: Funkcja por : N⊥→ N^⊥→ N^⊥ jest okre´slona tak:

por m n =







0, je´sli m = 0 lub n = 0;

1, je´sli m, n ∈ N i m, n > 0;

⊥, w przeciwnym przypadku.

Przyjmijmy, ˙ze zero interpretujemy jako true a liczby wieksze od zera jako false. Wtedy_, funkcja por to r´ownoleg la alternatywa (

”parallel or”), spe lniona zawsze gdy kt´ory´s ze sk lad- nik´ow jest spe lniony, nawet wtedy, gdy nieokre´slony jest drugi sk ladnik.

Lemat 9 Za l´o˙zmy, ˙ze M⁰ = M [ ~N /~x]  n, gdzie ~x to wszystkie zmienne wolne w M , a termy ~N sa zamkni_, ete. Wtedy albo M  n, albo M  E[x], gdzie x ∈ ~x i E[ ] jest_, kontekstem ewaluacyjnym.

Dow´od: Indukcja ze wzgledu na d lugo´_, s´c redukcji M⁰  n. Zak ladajac, ˙ze M = N ~_, R, gdzie term N nie jest aplikacja, mamy tu kilka mo˙zliwo´_, sci w zale˙zno´sci od N . Zbadanie ich pozostawiamy czytelnikowi.

Funkcja por nie jest definiowalna w jezyku PCF, co wynika z poni˙zszego lematu (dla m = 1)._, Lemat 10 Nie istnieje term M o zmiennych wolnych x i y, spe lniajacy jednocze´_, snie warunki:

M [0/x, Ω/y] =` 0 = M [Ω/x, 0/y] oraz M [1/x, 1/y] =`m, gdzie m > 0.

Dow´od: Z lematu 9 wynika, ˙ze wtedy M  E[x] lub M  E[y], niemo˙zliwe jest bowiem, aby term M redukowa l sie i do 0 i do m. Je´_, sli jednak M  E[x], to M [Ω/x, 0/y]  E[Ω]6⇓, i podobnie w drugim przypadku.

Stad wynika, ˙ze nie zachodzi twierdzenie odwrotne do adekwatno´_, sci.

Fakt 11 Semantyka denotacyjna dla PCF nie jest w pe lni abstrakcyjna: istnieja takie termy_, zamkniete T_, 0 i T1, ˙ze T0 ≡ T₁ ale [[T ]]0 6= [[T ]]₁.

Dow´od: Niech T_a, gdzie a ∈ {0, 1}, oznacza term:

λp. ifzero p 0 Ω then ifzero p Ω 0 then ifzero p 1 1 then Ω else a else Ω else Ω.

Latwo widzie´c, ˙ze [[T0]]por = 0 i [[T1]]por = 1, skad [[T_, 0]] 6= [[T1]]. Ponadto, gdyby T0M ⇓, dla jakiego´s M , to term M xy musia lby spe lnia´c warunki, o kt´orych mowa w lemacie 10. Skoro takiego nie ma, to zawsze T₀M 6⇓, czyli T₀ jest aplikacyjnie r´ownowa˙zne z Ω. Podobnie jest dla T0, wiec mamy aplikacyjn_, a r´_, ownowa˙zno´s´c term´ow T0i T1. A wiadomo, ˙ze z r´ownowa˙zno´sci aplikacyjnej wynika r´ownowa˙zno´s´c obserwacyjna.

Cwiczenia:´

1. Udowodni´c, ˙ze dla ka˙zdej funkcji cze´_,sciowo rekurencyjnej ϕ istnieje taki term Φ w jezyku PCF,_,

˙ze ϕ(n) = m wtedy i tylko wtedy, gdy Φ(n) ⇓ m. Inaczej: w PCF mo˙zna zdefiniowa´c ka˙zda_, funkcje cz_, e´_,sciowo rekurencyjna._,

2. Uzupe lni´c brakujace dowody._,