Slidy_2007

nstileleft 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 .
65
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 onstant (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 :: σ → τ
66
Aplikace (APP)
turnstileleft M :: σ → τ turnstileleft N :: σ
turnstileleft M N :: τ
Gener alizace (GEN)
turnstileleft M :: σ
turnstileleft M :: ∀ α .σ
α /∈ FTV ( )
Specializace (SPEC)
turnstileleft M :: ∀ α .σ
turnstileleft M :: [τ /α ]σ
67
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 onstant (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 :: σ → τ
68
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 :: ∀ α .σ
turnstileleft M :: [τ /α ]σ
τ typ
69
, 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
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 ter m u 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 /β ], [ Char ] → Bool )
typ’ (∅ , elem ’*’ "-*-" ) = ( ρ 3 ◦ ρ 2 ◦ ρ 1 , ρ 3 β ) , kde
ρ 1 = [[ Char ] → Bool /β ], τ = [ Char ] → Bool
ρ 2 = id, ϕ = [ Char ]
ρ 3 = mgu ([ Char ] → Bool )([ Char ] → γ ) = [ Bool /γ ]
tj. ([[ Char ] → Bool /β , Bool /γ ], Bool ])
76
Význam typo vání
• v ˇcasná detekce v ˇetšin y prog r amo vých ch yb
• pro oper ace s hodnotami známých typ ˚u lz e genero v at ef ektivn ˇejší kód
• dokumentace
P oužití v typo v aných jazycích
• typ , který uživ atel nedeklar uje , je odv oz en a použit
• typ , který uživ atel deklar uje je také odv oz en a zk ontroluje se , zda je stejný nebo
obecn ˇejší než deklaro v aný; deklaro v aný je použit
77
K ombinátor y S , K , I
Def: K ombinátoro vý ter m je ter m obsahující pouz e k ombinátor y ( S , K , I ) a aplikace:
S , K , I jsou k ombinátoro vé ter m y
jsou-li M , N , P k ombinátoro vé ter m y , je S M N P k ombinátoro vý ter m
jsou-li M , N k ombinátoro vé ter m y , je K M N k ombinátoro vý ter m
je-li M k ombinátoro vý ter m, je I M k ombinátoro vý ter m
T yp y k ombinátor ˚u v typo v aném kalkulu:
S :: ( α → β → γ ) → ( α → β ) → α → γ
K :: α → β → α
I :: α → α
78
Def: K ombinátoro vá redukce
S M N P ˆ S M P ( N P )
K M N ˆ K M
I M ˆ I M
ˆ je k ompatibilní uzáv ˇer relace ˆ S ∪ ˆ K ∪ ˆ I
∼ je refle xivní, symetr ic ký a tr ansitivní uzáv ˇe relace ˆ
Ekviv alence k ombinátor ˚u s λ -ter m y:
S ≈ λf λg λx.f x ( g x )
K ≈ λxλy .x
I ≈ λx.x
79
V ˇeta: ∼ ⊆ ≈
D ˚ukaz: p ˇrekladem S mapsto→ λxy z .xz ( y z ) , K mapsto→ λxy .x .
P oznámka: Inkluz e je vlastní, tj. ∼ negationslash= ≈
D ˚ukaz: S K K negationslash∼ S K S .
P ˇridání pr a vidla e xtensionality:
∀ P .M P ∼ prime N P
M ∼ prime N
M ∼ N
M ∼ prime N
80
V ˇeta: ∼ prime ⊆ ≈
D ˚ukaz indukcí p ˇres po ˇcet použití pr a vidla e xtensionality .
V ˇeta: Každý uza v ˇrený λ -ter m M lz e p ˇre vést na ≈ -ekviv alentní k ombinátoro vý
ter m N .
D ˚usledek: ∼ prime = ≈
D ˚ukaz vyplývá z p ˇredchozích dv ou v ˇet a z tr ansitivity ≈ .
81
K ombinátoro vá báz e je nejmenší (vzhledem k inkluzi) množina k ombinátor ˚u, jimiž lz e
vyjád ˇrit všechn y uza v ˇrené λ -ter m y .
V ˇeta: { S , K } je k ombinátoro vá báz e .
D ˚ukaz:
(i) Každý uza v ˇrený ter m lz e vyjád ˇrit pomocí S , K , I
(ii) I ≈ S K K
(iii) S nelz e vyád ˇrit pomocí K
(iv) K nelz e vyád ˇrit pomocí S
82
P ˇríklad: Necht ’ X je k ombinátor defino v aný pr a vidlem X M ˆ M K S K .
P ak { X } je k ombinátoro vá báz e .
D ˚ukaz:
X X X ˆ X K S K X ˆ K K S K S K X ˆ K K S K X ˆ K K X ˆ K
X ( X X ) ˆ X X K S K ˆ X K S K K S K ˆ K K S K S K K S K ˆ
K K S K K S K ˆ K K K S K ˆ K S K ˆ S
83
V netypo v aném k ombinátoro vém kalkulu lz e vyjád ˇrit k ombinátor pe vného bodu:
Y = S ( C B ( S I I )) ( C B ( S I I ))
84
Sem pat ˇrí str an y 55, 56, 57, 58.
Curr yho-Ho w ard ˚uv isomorfism us , g r af o vá redukce , optimalizace k ombinátoro vé sady
(k ombinátor y B , C ).
85
Super k ombinátor y
Motiv ace pro λ -lifting:
P = ( λx. (+) x (( λy .(∗ ) x y ) 3)) 4
Q = ( λxy .(+) x ( (∗ ) x y ) ) 4 3
P ∼ prime Q , ale p ˇreklad Q do k ombinátor ˚u je snažší než p ˇreklad P .
86
Super k ombinátor y
Idea: Každém u ter m u (funkcionálním u prog r am u) „ ušít na mír u “ jeho sadu k ombinátor ˚u
– tzv . super k ombinátor ˚u . P ˇrepiso v ací pr a vidlo pro každý super k ombinátor lz e
implemento v at jak o podprog r am v cílo vém jazyce (strojo vém nebo b yto vém kódu).
Def: Uza v ˇrený ter m S = λx 1 λx 2 . . . λx n .E je super k ombinátor když
n ≥ 0
E není λ -abstr akce
všechn y λ -abstr akce v E jsou super k ombinátor y
ˇCíslo n je tzv . ar ita super k ombinátor u S .
87
Super k ombinátoro vý rede x je tv ar u S M 1 M 2 . . . M n .
Reduk ˇcní pr a vidlo S x 1 x 2 . . . x n ˆ E neobsahuje v olné prom ˇenné, takže ho lz e
vyjád ˇrit pe vným podprog r amem v cílo vém kódu (G stroj).
Def: Super k ombinátor y ar ity 0 se nazýv ají k onstantní aplikativní for m y (CAF).
P ˇríklady super k ombinátor ˚u
α = 3 α = 3
β = (+) 25 β = (+) 25
γ = λx.x γ x = x
δ = λx. (+) x 1 δ x = (+) x 1
ε = λx. (∗ ) x x ε x = (∗ ) x x
ζ = λxλy .(− ) y x ζ x y = (− ) y x
η = λf .f ( λx. (∗ ) x x ) η f = f ε
88
P ˇríklady nesuper k ombinátor ˚u
λx.y není uza v ˇrený
λy .(− ) y x není uza v ˇrený
λf .f ( λx.f x 2) vnit ˇrní abstr akce není super k ombinátor (není uza v ˇrená)
λx.x ( λy .y ( λz .z y )) nejvnit ˇrn ˇejší abstr akce není super k ombinátor (není uza v ˇrená)
89
Algor itm us p ˇre v odu λ -ter m u do super k ombinátoro vého ter m u
Algor itm us: S C
Vstup: ter m M
Výstup: dv ojice ( D , M ) , kde D je množina definic super k ombinátor ˚u
M je super k ombinátoro vý ter m ekviv alentní M
S C ( M ) = T (∅ , M )
T ( D , M ) = jestliže M neobsahuje žádnou λ -abstr akci
pak ( D , M )
jinak T ( D ∪ {〈 α x 1 . . . x n x = N 〉} , M prime)
kde λx.N je ne vnit ˇrn ˇejší abstr akce v M
{ x 1 , . . . , x n } = FV ( λx.N )
M prime vznikne z M náhr adou abstr akce λx.N ter mem α x 1 . . . x n
P oznámka: Krok ˚um tr ansf or mace T se ˇríká „ vynášení lambda “ (lambda-lifting).
90
V ˇeta: Algor itm us p ˇre v odu λ -ter m u do super k ombinátoro vého ter m u k on v erguje a
výsledný ter m M je (p ˇri definicích z D ) ekviv alentní p ˚uv odním u ter m u M .
D ˚ukaz:
K on v ergence – v každém kroku ub ude λ -abstr akce , algor itm us k on ˇcí, když v ter m u už
žádné abstr akce nejsou. Každý krok zacho vává ekviv alenci:
λx.N ≈ λx.α x 1 . . . x n x (protože „α x 1 . . . x n x = N “ p ˇridáváme do D ), takže
λx.N ≈ λx.α x 1 . . . x n (po η -redukci)
91
V ˇeta: P ˇri p ˇre v odu λ -ter m u M v elik osti k do super k ombinátoro vého ter m u M b ude
mít ter m M v elik ost nejvýše k a celk o vá v elik ost všech ter m ˚u v D b ude v O ( k ) .
D ˚ukaz:
1. ter m α x 1 . . . x n není delší než λx.N , protože všechn y v olné prom ˇenné
x 1 , . . . , x n se v N vyskytují.
2. v každém kroku je p ˇrír ustek k celk o vé v elik osti nejvýše ro v en po ˇctu v olných
prom ˇenných ter m u N .
92
Modifikace vynášecího algor itm u na pln ˇe líné vynášení
Def: P odvýr az M abstr akce L je v olný , když všechn y prom ˇenné v M jsou v olné v L .
Maximální v olný výr az v L je tak o vý v olný výr az, který není vlastním podter mem
žádného výr azu v olného v L .
P ˇríklad: λxλy .y + sqr t x
Ab y b ylo zar u ˇceno , že po lambda-vynesení b ude zacho vána plná lenost, je n utné
vynášet místo v olných prom ˇenných maximální v olné výr azy .
93
Dato vé str uktur y v e funkcionálním prog r amo vání
Binomiální haldy
Def: Binomiální strom je (k o ˇreno vý) strom obecné ar ity s uzly ohodnocenými klí ˇci.
- binomiální strom stupn ˇe 0 je jednouzlo vý strom
- binomiální strom stupn ˇe r + 1 vznikne z e dv ou binomiálních strom ˚u t 1 , t 2 stupn ˇe r
tzv . spojením: strom t 1 se stane no vým, nejle v ˇejším, následník em strom u t 2
- uspo ˇrádání klí ˇc ˚u na všech v ˇetvích binomiálních strom ˚u je rostoucí
94
Každý binomiální strom je dán svým k o ˇrenen se stupn ˇem, ohodnocením (klí ˇcem) a
seznamem následnic kých podstrom ˚u. Následnic ké podstrom y jsou v po ˇradí s klesajícím
stupn ˇem.
data (Ord a) => BTree a = Node Int a [BTree a]
rank (Node r _ _) = r
root (Node _ x _) = x
P ˇri spojo vání se haldo vé ˇraz ení klí ˇc ˚u udržuje tím, že se p ˇripojuje vždy strom s k o ˇrenem
s v ˇetším klí ˇcem pod strom s k o ˇrenem s menším klí ˇcem. Spojo v ané strom y mají vždy
stejný stupe ˇn.
link :: (Ord a) => BTree a -> BTree a -> BTree a
link t1@(Node r x1 s1) t2@(Node _ x2 s2)
= if x1 a -> BHeap a -> BHeap a
insert x h = insBT (Node 0 x []) h
insBT :: (Ord a) => BTree a -> BHeap a -> BHeap a
insBT t [] = [t]
insBT t h@(t’:s)
= case compare (rank t1) (rank t2) of
LT -> t : h
GT -> t’: insBT t s
EQ -> insBT (link t t’) s
V ˇeta: Cena vložení klí ˇce do binomiální haldy v elik osti n je v (log n ) .
P oznámka: Amor tiz o v aná cena je dok once v (1) .
97
Slu ˇco vání
merge :: (Ord a) => BHeap a -> BHeap a -> BHeap a
merge h [] = h
merge [] h = h
merge h1@(t1:s1) h2@(t2:s2)
= case compare (rank t1) (rank t2) of
LT -> t1 : merge s1 h2
GT -> t2 : merge h1 s2
EQ -> insBT (link t1 t2) (merge s1 s2)
V ˇeta: Cena slou ˇcení dv ou binomiálních hald v elik osti n je v (log n ) .
98
Nalez ení a zr ušení nejmenšího pr vku
findMin :: (Ord a) => BHeap a -> a
findMin = root . fst . remMinT
deleteMin :: (Ord a) => BHeap a -> BHeap a
deleteMin h = merge (reverse s) s’
where (Node _ _ s, s’) = remMinT h
P omocná funkce remMinT vyjme z e seznam u strom s nejmenším k o ˇrenem.
remMinT :: (Ord a) => BHeap a -> (BTree a, BHeap a)
remMinT [t] = (t,[])
remMinT (t:s) = if root t