Slidy_2006

, x σ1 , . . . , y σ , · · · ∈ σ
¡
k onstanty c σ1 , . . . , c σk ∈ σ
¢
abstrakce x σ ∈ σ prom ˇenná, M ∈ τ , pak λx σ .M ∈ σ → τ
aplikace M ∈ σ → τ , N ∈ σ , pak M N ∈ τ
40
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í.
D ˚ukaz je stejný jak o v netypo v aném p ˇrípad ˇe.
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 ˇrít k ombinátor pe vného
bodu s vlastností
∀ F . F ˆ ∗ F ( F )
41
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 σ :: ( σ → σ ) → σ
42
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
43
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 ˆ . . .
44
Lambda ter m je v hla v o vé nor mální for m ˇe ( hnf ), práv ˇe když má tv ar
λx 1 λx 2 . . . λx k . v M 1 . . . M m
kde k ≥ 0 ,
m ≥ 0 ,
v je prom ˇenná nebo k onstanta, a
v M 1 . . . M p není rede x pro žádné p ≤ m .
T edy hnf je ter m, který tv o ˇrí prom ˇenná ˇci k onstanta aplik o v aná na p ˇríliš málo argument ˚u
(p ˇrípad k = 0 ), anebo lambda abstr akce , jejíž t ˇelo není reducibilní (p ˇrípad k > 0 ).
45
Slabá hla v o vá nor mální for ma ( whnf ) je lambda ter m v e tv ar u
v M 1 . . . M n
kde n ≥ 0 ,
v je prom ˇenná, k onstanta nebo lambda abstr akce , a
v M 1 . . . M p není rede x pro žádné p ≤ n .
T edy whnf je ter m, který tv o ˇrí prom ˇenná ˇci k onstanta aplik o v aná na p ˇríliš málo
argument ˚u, anebo lambda abstr akce .
P oznámka: Každá hnf je také whnf . Opak neplatí, nap ˇr. λx. ( λy .y ) z není hnf .
V ˇeta: Slabé hla v o vé nor mální for m y jsou ireducibilní vzhledem k redukci v PCF .
46
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 )
Rekurzivní definice k onstant a funkcí
letrec f x 1 . . . x k = M in N ≡ ( λf .N )
¡
Y ( λf λx 1 . . . x k .M )
¢
47
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
48
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í rekurzivní 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 ))
¢
49
Nor malizace v jednoduše typo v aném lambda kalkulu (fundo v anost redukce)
50
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 ) .
51
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.
52
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
53
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ží
• 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 ) .
54
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 σ
55
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 i σ → τ typ
je-li α typo vá prom ˇenná, σ typ , pak ∀ α .σ je typ
typ y se vytvá ˇrejí v oln ˇe
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: stejn ˇe jak o v jednoduše typo v aném lambda kalkulu, na víc B , H .
56
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
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.
58
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
59
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 )
60
σ × τ = ∀ α .( σ → τ → α ) → α
( 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 )
61
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 τ :: [τ /α ]σ
62
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 :: [τ /α ]σ
63
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.
∅ turnstileleft M :: σ , kde σ je typ . Zapisujeme turnstileleft M :: σ .
P oznámka: Je z ˇrejmé, že ne všechna otypo vání ter m u vyjad ˇrují jeho skute ˇcný typ . Za
platná b udeme po v ažo v at jen ta otypo vání, která lz e odv odit z axiom ˚u pomocí daných
odv oz o v acích pr a videl.
Def: T er m M je otypo v atelný , lz e-li odv odit jeho otypo vání (v prázdném typo vém
k onte xtu). T yp z tak o vého otypo vání je typem ter m u M .
64
Odv oz o v ací pr a vidla pro impredikativní typo vý systém
Axiom prom ˇenné (V AR)
, x :: σ turnstileleft x :: σ
Axiom y k onstanty (CON)
turnstileleft 0 :: Nat
,
turnstileleft F alse :: Bool
, . . .
Zeslabení (W)
turnstileleft M :: σ
, x :: τ turnstileleft M :: σ
x /∈ FV ( M )
Abstr akce (ABS)
, x :: σ turnstileleft M :: τ
turnstileleft λx.M :: σ → τ
65
Aplikace (APP)
turnstileleft M :: σ → τ turnstileleft N :: σ
turnstileleft M N :: τ
Gener alizace (GEN)
turnstileleft M :: σ
turnstileleft M :: ∀ α .σ
α /∈ FTV ( )
Specializace (SPEC)
turnstileleft M :: [τ /α ]σ
66
Odv oz o v ací pr a vidla pro predikativní typo vý systém a ter m y s let
Axiom prom ˇenné (V AR)
, x :: σ turnstileleft x :: σ
Axiom y k onstanty (CON)
turnstileleft 0 :: Nat
,
turnstileleft F alse :: Bool
, . . .
Zeslabení (W)
turnstileleft M :: σ
, x :: τ turnstileleft M :: σ
x /∈ FV ( M )
Abstr akce (ABS)
, x :: σ turnstileleft M :: τ
turnstileleft λx.M :: σ → τ
67
Aplikace (APP)
turnstileleft M :: σ → τ turnstileleft N :: σ
turnstileleft M N :: τ
Let-výr az (LET)
turnstileleft N :: σ , x :: σ turnstileleft M :: τ
turnstileleft let x = N in M :: τ
Gener alizace (GEN)
turnstileleft M :: σ
turnstileleft M :: ∀ α .σ
α /∈ FV ( )
Specializace (SPEC)
turnstileleft M :: [τ /α ]σ
τ typ
68
, x :: ∀ α .σ turnstileleft M :: τ
turnstileleft λx.M :: (∀ α .σ ) → τ
A B S turnstileleft N :: ∀ α .σ
turnstileleft ( λx.M ) N :: τ
A P P
turnstileleft N :: ∀ α .σ , x :: ∀ α .σ turnstileleft M :: τ
turnstileleft let x = N in M :: τ
L E T
( λx.M ) N ≈ let x = N in M
69
Sem pat ˇrí str ana 45 Impredikativní.
70
Existují ter m y , které lz e otypo v at v impredikativním typo vém systém u, ale nelz e je
otypo v at v predikativním typo vém systém u.
(∀ α.α → α )→ Nat × Bool
z }| {
( λ f
|{z}
∀ α.α → α
.( f
|{z}
∀ α.α → α
0 , f
|{z}
∀ α.α → α
T r ue )) ( λx.x )
| {z }
∀ α.α → α
:: Nat × Bool
71
Ab ychom mohli požív at výhod polymorfism u a p ˇritom zacho v ali jednoduchý (predikativní)
typo vý systém, rozší ˇríme kalkul o „ let “ výr azy , které spojují abstr akci s aplikací:
T er m y:
x, y , . . . prom ˇenné
c 1 , c 2 , . . . , c k k onstanty
M N aplikace
λx.M abstr akce
let x = M in N let výr az
72
Robinson ˚uv unifika ˇcní algor itm us
mgu σ τ =
jestliže σ == τ
pak je výsledk em identic ká substituce
jinak: Necht ’ ϕ resp . ψ jsou typo vé podvýr azy v σ resp . τ na nejle v ˇejší nejvyšší
pozici, na níž se σ liší od τ .
Jestliže ϕ a ψ jsou oba typo vé k onstr uktor y ,
pak typ y σ a τ nejsou unifik o v atelné (unifikátor je ⊥ )
jinak je-li ϕ typo vá prom ˇenná a ϕ /∈ FV ( ψ ) ,
pak unifikátor je mgu ( ρσ )( ρτ ) ◦ ρ , kde ρ = [ψ /ϕ ] ,
je-li ψ typo vá prom ˇenná a ψ /∈ FV ( ϕ ) ,
pak unifikátor je mgu ( ρσ )( ρτ ) ◦ ρ , kde ρ = [ϕ/ψ ] ;
pokud ϕ ∈ FV ( ψ ) nebo ψ ∈ FV ( ϕ ) , pak typ y σ a τ
nejsou unifik o v atelné (unifikátor je ⊥ ).
73
Algor itm us otypo vání v predikativním kalkulu s let
typ M = snd ( typ’ (∅ , M ))
typ’ ( , M ) = ( ρ, σ ) σ je nejobecn ˇejší typ ter m u M
ρ je substituce , tak o vá, že ρ je no vý typo vý k onte xt,
kde
(i) je-li M k onstanta, položíme
ρ = id
σ = type M
(ii) je-li M = x , položíme
ρ = id
pokud ( x :: τ ) ∈ , pak σ = τ , jinak σ = α , kde α je ˇcerstvá
74
(iii) je-li M = λx.N , položíme
( ρ, τ ) = typ’ ( ∪ { x :: α } , N ) , α je ˇcerstvá
σ = ρ ( α → τ )
(iv) je-li M = let x = N in P , položíme
( ρ 1 , ϕ ) = typ’ ( , N )
( ρ 2 , σ ) = typ’ ( ρ 1 ∪ { x :: ϕ } , P )
ρ == ρ 2 ◦ ρ 1
(v) je-li M = N P , položíme
( ρ 1 , τ ) = typ’ ( , N )
( ρ 2 , ϕ ) = typ’ ( ρ 1 , P )
ρ 3 = mgu ( ρ 2 τ )( ϕ → α ) , α ˇcerstvá
ρ = ρ 3 ◦ ρ 2 ◦ ρ 1
σ = ρ 3 α
75
P ˇríklad - typ elem ’*’ "-*-"
typ’( ∅ ,elem)=( id, α → [α ] → Bool)
typ’ (∅ ,’*’)=( id, Char)
typ’ (∅ ,"-*-")=( id, [ Char ] )
typ’ (∅ , elem ’*’) = ( ρ 3 ◦ ρ 2 ◦ ρ 1 , ρ 3 β ) , kde
ρ 1 = id, τ = α → [α ] → Bool
ρ 2 = id, ϕ = Char
ρ 3 = [[ Char ] → Bool /β ]
tj. ([[ Char ] → Bool /β ],