Slidy_2007

e ˆ tr ue not tr ue ˆ false
M ˆ N
not M ˆ not N
36
Vy ˇcíslitelné funkce
ˇCíselné funkce: N n 99K− N (pr vního ˇrádu)
Def: Pr imitivn ˇe vy ˇcíslitelné jsou funkce
• z n : N n → N , ∀ x ∈ N . z n ( x ) = 0 (n ulo vá)
• succ : N → N (následník)
• proj n,k : N n → N , proj n,k ( x 1 , . . . , x n ) = x k (projekce)
• Jsou-li g : N m → N , h 1 , . . . , h m : N n → N pr imitivn ˇe vy ˇcíslitelné,
pak f : N n → N tak o vá, že
f ( x 1 , . . . , x n ) = g ( h 1 ( x 1 , . . . , x n ) , . . . , h m ( x 1 , . . . , x n )) ,
je pr imitivn ˇe vy ˇcíslitelná. (dosaz ení)
37
• Jsou-li g : N n → N , h : N n +2 → N pr imitivn ˇe vy ˇcíslitelné, pak f : N n +1 → N
tak o vá, že
f (0 , x 1 , . . . , x n ) = g ( x 1 , . . . , x n )
f ( y + 1 , x 1 , . . . , x n ) = h ( f ( y , x 1 , . . . , x n ) , y , x 1 , . . . , x n ) ,
je pr imitivn ˇe vy ˇcíslitelná. (pr imitivní rekurse)
• Každá pr imitivn ˇe vy ˇcíslitelná funkce je vy ˇcíslitelná .
• Je-li funkce g : N n +1 99K− N vy ˇcíslitelná, pak f : N n +1 99K− N tak o vá, že
f ( y , x 1 , . . . , x n ) = µz .( g ( z , x 1 , . . . , x n ) = y ) , je vy ˇcíslitelná. (µ -rekurse)
38
Lambda vy ˇcíslitelnost
Def: P arciální funkce f : N n 99K− N je λ -defino v atelná , práv ˇe když e xistuje ter m
F ∈ tak o vý, že pro všechn y n -tice ( k 1 , . . . , k n ) z defini ˇcního obor u funkce f platí
F k 1 k 2 . . . k n ≈ f ( k 1 , k 2 , . . . , k n )
a pro n -tice ( k prime1 , . . . , k primen ) , v nichž funkce f není defino vána, ter m F k prime1 k prime2 . . . k primen
nemá nor mální for m u.
P oznámka: Z k onfluence vyplývá, že když nor mální for ma e xistuje , tak
F k 1 k 2 . . . k n ˆ ∗ f ( k 1 , k 2 , . . . , k n ) ,.
39
V ˇeta: Každá parciální vy ˇcíslitelná funkce je λ -defino v atená.
D ˚ukaz:
(1) Každá totální vy ˇcíslitelná funkce je λ -defino v atelná:
n ula
následník
pr ojekce
dosaz ení: Jsou-li funkce g : N m → N , h 1 , . . . , h m : N n → N λ -defino v atelné
pomocí ter m ˚u G, H 1 , . . . , H m , pak funkce f : N n → N tak o vá, že
f ( x 1 , . . . , x n ) = g ( h 1 ( x 1 , . . . , x n ) , . . . , h m ( x 1 , . . . , x n )) , je
λ -defino v atelná pomocí ter m u
F = λx 1 . . . x n .G ( H 1 x 1 . . . x n ) . . . ( H m x 1 . . . x n ) .
40
primitivní rekur se: Jsou-li g : N n → N , h : N n +2 → N λ -defino v atelné pomocí
ter m ˚u G, H , pak funkce f : N n +1 → N tak o vá, že
f (0 , x 1 , . . . , x n ) = g ( x 1 , . . . , x n )
f ( y + 1 , x 1 , . . . , x n ) = h ( f ( y , x 1 , . . . , x n ) , y , x 1 , . . . , x n ) ,
je λ -defino v atelná pomocí ter m u
F = Y
¡
λf y x 1 . . . x n . if ( isz ero y )( G x 1 . . . x n )
( H ( f ( pred y ) x 1 . . . x n )( pred y ) x 1 . . . x n ))
¢
41
obecná (µ ) rekur se: Je-li g : N n +1 → N λ -defino v atelná pomocí ter m u G , pak
funkce f : N n +1 → N totální a tak o vá, že
f ( y , x 1 , . . . , x n ) = µz .( g ( z , x 1 , . . . , x n ) = y ) ,
je λ -defino v atelná pomocí ter m u
F = λy x 1 . . . x n . Y
¡
λhz . if ( eq y ( G z x 1 . . . x n )) z ( h ( succ z ))
¢
0
(2) Každá parciální vy ˇcíslitelná funkce je λ -defino v atelná:
P odobn ˇe jak o pro totální funkce , ale je t ˇreba „ nasim ulo v at str iktní redukci “ , ab y
ter m y , které str iktn ˇe nenor malizují, b yly p ˇre v eden y na ter m y bez nf .
42
V ˇeta: Každá λ -defino v atelná funkce je vy ˇcíslitelná:
T echnic ké detaily d ˚ukazu pr acné a zdlouha vé, idea prostá: Sestrojíme TM (nebo
RAM, prog r am v Hask ellu, . . . ), který pro každý ter m F , který λ -defin uje funkci
f : N n → N , a pro každou n -tici ( x 1 , . . . , x n ) ∈ N n inter pretuje aplikaci
F x 1 . . . x n pomocí nor mální reduk ˇcní str ategie .
43
Jednoduše typo v aný lambda kalkul
T yp y
Základní typ: ι
Jsou-li σ , τ typ y , pak σ → τ je typ .
T er m y
Pro každý typ σ defin ujeme množin u σ ter m ˚u typu σ :
pr om ˇenné x σ , x σ1 , . . . , y σ , · · · ∈ σ
¡
k onstanty c σ1 , . . . , c σk ∈ σ
¢
abstrakce x σ ∈ σ prom ˇenná, M ∈ τ , pak λx σ .M ∈ σ → τ
aplikace M ∈ σ → τ , N ∈ σ , pak M N ∈ τ
Místo M ∈ σ ˇcasto píšeme M : σ .
44
Redukce ˆ se defin uje stejn ˇe jak o v netypo v aném lambda kalkulu:
( λx σ .M ) N ˆ β [N /x ]M M ∈ τ , N ∈ σ
FV ( N ) ∩ BV ( M ) = ∅
λx σ .M x σ ˆ η M pokud x σ negationslash∈ FV ( M )
M ∈ σ → τ
V ˇeta: Redukce v jednoduše typo v aném lambda kalkulu je k onfluentní.
V ˇeta: Redukce v jednoduše typo v aném lambda kalkulu je fundo v aná.
D ˚ukaz viz [H. Barendregt – Lambda Calculus , Its Syntax and Semantics].
D ˚usledek: V jednoduše typo v aném lambda kalkulu nelz e vyjád ˇrit k ombinátor pe vného
bodu s vlastností
∀ F . F ˆ ∗ F ( F )
45
Nor malizace v jednoduše typo v aném lambda kalkulu (fundo v anost redukce)
V ˇeta: (o k om utaci β -η )
ˆ β ◦ ˆ η ⊆ ˆ η ∗ ◦ ˆ β ∗
D ˚ukaz roz epsáním všech p ˇrípad ˚u vzájemného zano ˇrení β -rede x ˚u a η -rede x ˚u.
V ˇeta: (o odložení η -redukcí)
ˆ ∗ ⊆ ˆ η ∗ ◦ ˆ β ∗
D ˚ukaz indukcí podle po ˇctu η -redukcí následo v aných β -redukcemi, užitím V ˇety
o k om utaci β -η .
V ˇeta: Má-li ter m β -nor mální for m u, pak má i nor mální for m u.
46
Def: Stupe ˇn typu
δ ( ι) = 1
δ ( σ → τ ) = max { δ ( σ ) , δ ( τ )} + 1
Def: Stupe ˇn β -rede xu
δ
¡
( λx σ .M τ ) N σ
¢
= δ ( σ → τ )
Def: Stupe ˇn ter m u d ( M ) je 0, pokud ter m M neobsahuje β -rede xy , jinak je d ( M )
maxim um z e stup ˇn ˚u všech β -rede x ˚u obsažených v ter m u M .
P oznámka: Pro β -rede x R platí δ ( R ) ≤ d ( R ) .
47
Lemma: (o stupni substituce)
d ([ N /x σ ]M ) ≤ max { d ( M ) , d ( N ) , δ ( σ )}
D ˚ukaz: V ter m u [N /x σ ]M jsou rede xy
1. ter m u M (s N na míst ˇe x )
2. ter m u N (p ˇrípadn ˇe namnožené)
3. p ˇrípadn ˇe no vé rede xy tv ar u N Q , pokud v M b yl podter m x Q a N = λy .P
48
V ˇeta: (o slabé nor malizaci) Každý ter m jednoduše typo v aného lambda kalkulu má
nor mální for m u
D ˚ukaz: Necht ’ M je ter m a R je tak o vý jeho rede x maximálního stupn ˇe, který obsahuje
rede xy už jen nižších stup ˇn ˚u, tj.
(i) δ ( R ) = d ( M )
(ii) R neobsahuje rede xy stupn ˇe δ ( R )
P ˇri redukci ter m u M v rede xu R :
• rede xy vn ˇe R z ˚ustanou
• rede xy uvnit ˇr R z ˚ustanou, p ˇrípadn ˇe se i namnoží; ale dle Lemmatu o stupni
substituce ne vzroste d ( M )
• rede x R zmizí; je-li nahr az en jinými rede xy , b udou mít ost ˇre nižší stupe ˇn
T edy: ne vzroste stupe ˇn ter m u a klesne po ˇcet rede x ˚u stupn ˇe d ( M ) .
49
V ˇeta: (o silné nor malizaci) Každý ter m jednoduše typo v aného lambda kalkulu je siln ˇe
nor malizující, tj. redukce v jednoduše typo v aném lambda kalkulu je fundo v aná.
D ˚ukaz: Za v edeme množin y R σ pro každý typ σ :
R ι = { M :: ι | SN( M )}
R σ → τ = { M :: σ → τ | ∀ N ∈ R σ .M N ∈ R τ }
Vyšet ˇrujeme následující implikace:
(i) M ∈ R σ ⇒ SN( M )
(ii) M ∈ R σ & M ˆ N ⇒ N ∈ R σ
(iii) M není abstr akce & ∀ N .( M ˆ N ⇒ N ∈ R σ ) ⇒ M ∈ R σ
50
PCF — p ˇríklad jednoduchého funkcionálního jazyka
T yp y: základní typ y Bool , Nat
pro každé dv a typ y σ , τ je σ → τ typ
Místo M ∈ σ píšeme M :: σ
T er m y: pro každý typ σ máme spo ˇcetn ˇe mnoho prom ˇenných x σ1 , x σ2 , . . . :: σ
x :: σ , M :: τ ⇒ λx.M :: σ → τ
M :: σ → τ , N :: σ ⇒ M N :: τ
n p ˇriroz ené ˇcíslo ⇒ n :: Nat , T r ue :: Bool , F alse :: Bool
succ :: Nat → Nat , pred :: Nat → Nat , isz ero :: Nat → Bool
pro každý typ σ je if σ :: Bool → σ → σ → σ
pro každý typ σ je Y σ :: ( σ → σ ) → σ
51
Redukce: ( λx.M ) N ˆ [N /x ]M
if σ T r ue M N ˆ M , if σ F alse M N ˆ N
M ˆ N ⇒ if σ M P Q ˆ if σ N P Q
succ n ˆ n + 1 , pred n + 1 ˆ n, ( pred 0 ˆ pred 0)
M ˆ N ⇒ pred M ˆ pred N , succ M ˆ succ N
isz ero M ˆ isz ero N
isz ero 0 ˆ T r ue , isz ero n + 1 ˆ F alse
Y σ M ˆ M ( Y σ M )
M ˆ N ⇒ M P ˆ N P
52
Def: Prog r am v PCF je uza v ˇrený ter m typu Bool nebo Nat (základního typu).
V ˇeta: PCF je vnit ˇrn ˇe deter ministic ký, tj. pro každý ter m M e xistuje nejvýše jeden ter m
N tak o vý, že M ˆ N .
D ˚ukaz indukcí podle délky ter m u M , roz epsáním jednotlivých p ˇrípad ˚u (tv ar ˚u ter m u).
D ˚usledek: Redukce v PCF je sou ˇcasn ˇe reduk ˇcní str ategií.
V ˇeta: Je-li M prog r am v PCF r ˚uzný od n , T r ue , F alse , pak ho lz e reduk o v at práv ˇe
jedním zp ˚usobem.
D ˚usledek: Je-li M prog r am v PCF , pak nastane práv ˇe jedna z následující možností:
M ˆ ∗ n pro n ˇejaké n ∈ N
M ˆ ∗ T r ue
M ˆ ∗ F alse
M ˆ M 1 ˆ M 2 ˆ . . .
53
Syntaktic ká rozší ˇrení PCF
Lokální definice k onstant
let x = M in N ≡ ( λx.N ) M
nebo obecn ˇeji funkcí
let f x 1 . . . x k = M in N ≡ ( λf .N )( λx 1 . . . x k .M )
Rekursivní definice k onstant a funkcí
letrec f x 1 . . . x k = M in N ≡ ( λf .N )
¡
Y ( λf λx 1 . . . x k .M )
¢
54
Uspo ˇrádané dv ojice
K onstr uktor ( ,) σ τ ( M , N ) ≡ ( ,) σ τ M N
Selektor y fst σ τ , snd σ τ
δ -pr a vidla M ˆ P ⇒ ( M , N ) ˆ ( P , N )
N ˆ P ⇒ ( M , N ) ˆ ( M , P ) pro M negationslashˆ , tj. M tv ar u
x, y , . . . , λx.Q, T r ue , F alse , 0 , 1 , . . . ,
succ , pred , isz ero , if σ , Y σ , if Q, if Q Q prime
fst ( M , N ) ˆ M
snd ( M , N ) ˆ N
55
Definice podle vz or u
Def: Vz or v PCF je prom ˇenná nebo T r ue nebo F alse nebo 0 nebo 1 nebo . . . nebo
( p, q ) , kde p , q jsou vz or y .
Syntaktic ká zkr atka λ ( p 1 , p 2 ) .M ≡ λz .( λp 1 p 2 .M )( fst z )( snd z )
Lokální rekursivní definice
letrec f 1 x 1 . . . x n = M 1
f 2 x 1 . . . x n = M 2
.
.
.
f m x 1 . . . x n = M m
in N
≡
¡
λ ( f 1 , . . . , f m ) .N
¢¡
Y ( λ ( f 1 , . . . , f m ) .( λx 1 . . . x n .M 1 , . . . , λx 1 . . . x n .M m ))
¢
56
P olymorfní lambda kalkul
T yp y
- spo ˇcetná množina typo vých prom ˇenných α 1 , α 2 , . . .
- každá typo vá prom ˇenná je typ
- jsou-li σ , τ typ y , je také σ → τ typ
- je-li α typo vá prom ˇenná, σ typ , pak ∀ α .σ je typ
- typ y se vytvá ˇrejí v oln ˇe
P oznámka: Impredikativní (Gir ard ˚uv-Re ynolds ˚uv) typo vý systém:
σ ::= α | σ → σ | ∀ α .σ
Predikativní (Hindle y ˚uv-Millner ˚uv) typo vý systém:
σ ::= τ | ∀ α .σ
τ ::= α | τ → τ
57
T er m y
- každá prom ˇenná x σ je ter m typu σ
- x :: σ prom ˇenná, M :: τ ter m, pak λx.M :: σ → τ ter m
- M :: σ → τ , N :: σ ter m y , pak M N :: τ je ter m
- M :: σ ter m, pak α .M :: ∀ α .σ (gener alizace)
- M :: ∀ .σ ter m, τ typ , pak M τ :: [τ /α ]σ (specializace)
Redukce
Za vádí se stejn ˇe jak o v jednoduše typo v aném lambda kalkulu, na víc B , H .
B -redukce: ( α .M ) τ ˆ [τ /α ]M
H -redukce: α . M α ˆ M pro α /∈ FV ( M )
V ˇeta: Redukce v polymorfním lambda kalkulu je k onfluentní a fundo v aná.
D ˚ukaz fundo v anosti (SN) podal Dag Pr a witz.
58
Def: Uza v ˇrené typ y – typo vé ter m y bez v olných typo vých prom ˇenných
Uza v ˇrené hodnoty – ireducibilní uza v ˇrené ter m y uza v ˇreného typu
n -ár ní typo vé k onstr uktor y – typo vé ter m y s n v olnými typo vými prom ˇennými,
nad nimiž je pro v edena typo vá abstr akce
Lemma:
Každý uza v ˇrený ter m typu σ → τ v nor mální for m ˇe má tv ar λx.M , kde x :: σ , M :: τ .
Každý uza v ˇrený ter m typu ∀ α .σ v nor mální for m ˇe má tv ar α .M , kde M :: σ .
D ˚ukaz: ob ˇe tvrz ení se dokazují naráz indukcí podle str uktur y ter m u.
59
Definice základních uza v ˇrených typ ˚u, typo vých k onstr uktor ˚u a jejich
(uza v ˇrených) hodnot v polymorfním labda kalkulu
Bool = ∀ α .α → α → α
dv ˇe uza v ˇrené hodnoty: T r ue = α λx :: α λy :: α . x
F alse = α λx :: α λy :: α . y
not = λz :: Bool . z Bool F alse T r ue
and = λu :: Bool λv :: Bool . u Bool v F alse
or = λu :: Bool λv :: Bool . u Bool T r ue v
if = α λc :: Bool λx :: α λy :: α . c α x y
60
Nat = ∀ α .α → ( α → α ) → α
spo ˇcetn ˇe mnoho uza v ˇrených hodnot:
n = α λx :: α λy :: α → α . y ( y ( . . . ( y ( y
| {z }
n -krát
x )) . . .))
succ = λn :: Nat λx :: α λy :: α → α . y ( n α x y )
isz ero = λn :: Nat . n Bool T r ue ( λz :: Bool . F alse )
61
σ × τ = ∀ α .( σ → τ → α ) → α
( M , N ) = α λx :: σ → τ → α . x M N , kde M :: σ , N :: τ
fst = σ τ λp :: σ × τ . p σ ( λx :: σ λy :: τ . x )
snd = σ τ λp :: σ × τ . p σ ( λx :: σ λy :: τ . y )
List σ = ∀ α .α → ( σ → α → α ) → α
Nil = σ α λx :: α λy :: σ → α → α . x
(:) = σ λu :: σ λt :: List σ α λx :: α λy :: σ → α → α . y u ( t α x y )
62
Churcho v a vs . Curr yho v ar ianta polymorfního lambda kalkulu
Church – kalkul s e xplicitním typo váním
x σ :: σ
M :: τ ⇒ λx :: σ . M :: σ → τ
M :: σ → τ , N :: σ ⇒ M N :: τ
M :: σ ⇒ α . M :: ∀ α .σ
M :: ∀ α .σ , τ typ ⇒ M τ :: [τ /α ]σ
63
Churcho v a vs . Curr yho v ar ianta polymorfního lambda kalkulu
Curr y – kalkul s implicitním typo váním
x :: σ
x :: σ , M :: τ ⇒ λx. M :: σ → τ
M :: σ → τ , N :: σ ⇒ M N :: τ
M :: σ ⇒ M :: ∀ α .σ
M :: ∀ α .σ , τ typ ⇒ M :: [τ /α ]σ
64
Otypo vání
Def: K one ˇcná množina = { ( x 1 :: σ 1 ) , . . . , ( x k :: σ k )} dv ojic (prom ˇenná :: typ)
tak o vá, že prom ˇenné x 1 , . . . , x k jsou na vzájem r ˚uzné, se nazývá typo vý k onte xt .
Def: Necht ’ je typo vý k onte xt, M je ter m, σ je typ . Zápis turnstileleft M :: σ se nazývá
otypo vání ter m u M v typo vém k onte xtu .
Otypo váním ter m u M rozumíme jeho otypo vání v prázdném typo vém k onte xtu, tj.
∅ tur