- Stahuj zápisky z přednášek a ostatní studijní materiály
- Zapisuj si jen kvalitní vyučující (obsáhlá databáze referencí)
- Nastav si své předměty a buď stále v obraze
- Zapoj se svojí aktivitou do soutěže o ceny
- Založ si svůj profil, aby tě tví spolužáci mohli najít
- Najdi své přátele podle místa kde bydlíš nebo školy kterou studuješ
- Diskutuj ve skupinách o tématech, které tě zajímají
Studijní materiály
Zjednodušená ukázka:
Stáhnout celý tento materiálFunkcionální pr ogramo vání
IA014
P ˇrednášky: ˇctvr tek 16.00–18.40, B011
K onsultace: úterý 16.00–17.45, B419
Zk oušky: ˇcer v en 2006
1
Liter atur a
• Anthon y J . Field, P eter G. Harr ison: Introduction to Functional Prog r amming ,
Addison W esle y , 1988
• Greg Michaelson: An Introduction to Functional Prog r amming through Lambda
Calculus , Addison W esle y , 1989
• Simon L. P e yton Jones: The Implementation of Functional Prog r amming Languages ,
Prentice Hall, 1987
• Simon L. P e yton Jones , Da vid Lester : Implementation Functional Languages:
a tutor ial
Inf or mace , odkazy
http://www.fi.muni.cz/~libor/vyuka/IA014/
2
Nápl ˇn kursu
- Netypo v aný a typo v aný lambda kalkul. Silná nor malizace , Churcho v a-Rossero v a
vlastnost.
- Rekurse , v ˇeta o pe vném bod ˇe.
- J azyk PCF a jeho sémantika.
- T yp y . Prob lém otypo vání, par ametr ic ký polymorfism us .
Impredikativní typo vé systém y .
Otypo vání v predikativních typo vých systémech.
- K ombinátoro vý po ˇcet. K ombinátor y S , K , I . K ombinátor y B , C .
3
- Implementace funkcionálních jazyk ˚u.
P ˇreklad definic podle vz or u, strážených klauzulí, intensionálních seznam ˚u.
- Gr af o vá redukce . G-stroj. Super k ombinátor y , vynášení.
- Optimální redukce , plná lenost, pln ˇe líné vynášení.
- Imper ativní pr vky , vstup/výstup , ošet ˇrení výjimek, nedeter minism us , p ˇrepiso v atelná
pole , sta v . P okr a ˇco vání.
- Monády . Monadic ký dato vý typ pro vstup/výstup . Monadic ké k ombinátor y pro
syntaktic k ou analýzu.
- Funkcionální dato vé str uktur y .
Binár ní haldy , binomiální haldy , vyhledáv ací strom y .
4
Sem pat ˇrí str ana 4. Motiv a ˇcní p ˇríklad.
5
Netypo v aný lambda kalkul
Syntax
Dána spo ˇcetná množina symbol ˚u, tzv . prom ˇenných x 1 , x 2 , x 3 , . . . , x, y , z , t, u, v , . . .
Množina lambda ter m ˚u (výr az ˚u) je defino vána induktivn ˇe:
• Každá prom ˇenná je ter m
• M , N ter m y ⇒ M N ter m (aplikace)
• x prom ˇenná, M ter m ⇒ λx.M ter m (abstr akce)
6
K on v ence:
M 1 M 2 M 3 . . . M n ≡ ( . . . (( M 1 M 2 ) M 3 ) . . .) M n
λx 1 x 2 . . . x n .M ≡ λx 1 .λx 2 . . . λx n .M ≡ λx 1 .( λx 2 .( . . . ( λx n .M ) . . .))
V olné prom ˇenné FV ( M )
Vázané prom ˇenné BV ( M )
Substituce [P /x ] : →
P odter m
7
Def: P odter m
Je-li M ter m, je M svým podter mem.
T er m M N má podter m y M , N .
T er m λx.M má podter m M .
Má-li ter m M podter m N a ter m N má podter m P , pak P je také podter mem ter m u
M .
Lemma: Uza v ˇrené ter m y jsou in v ar iantní v ˚u ˇci substitucím:
∀ M ∈ ∀ substituci σ : → . FV ( M ) negationslash= ∅ ⇒ σ M = M
8
Def: V olné prom ˇenné
FV ( x ) = { x }
FV ( M N ) = FV ( M ) ∪ FV ( N )
FV ( λx.M ) = FV ( M ) − { x }
Def: Vázané prom ˇenné
BV ( x ) = ∅
BV ( M N ) = BV ( M ) ∪ BV ( N )
BV ( λx.M ) = BV ( M ) ∪ { x }
9
Def: Substituce
P . . . ter m
x . . . prom ˇenná
[P /x ] : → . . . substituce
[P /x ]x = P
y negationslash= x ⇒ [P /x ]y = y
[P /x ]( M N ) = ([ P /x ]M )([ p/x ]N )
[P /x ]λx.M = λx.M
y negationslash= x, y negationslash∈ FV ( P ) ⇒ [P /x ]λy .M = λy .[P /x ]M
y negationslash= x, y ∈ FV ( P ) ⇒ [P /x ]λy .M = λy 1 .[P /x ]([ y 1 /y ]M ) ,
kde y 1 je ˇcerstvá.
10
Sémantika
Sémantiku lz e zadat b ud ’ denota ˇcn ˇe ( [[ _ ]] : − → D , kde D je doména hodnot),
anebo stylem oper a ˇcní sémantiky: na ter mech za v edeme relaci jednokrok o vé redukce
ˆ ⊆ 2 a vytv o ˇríme p ˇrepiso v ací systém .
β -redukce: ( λx.M ) N ˆ β [N /x ]M ( FV ( N ) ∩ BV ( M ) = ∅ )
η -redukce: λx.M x ˆ η M pro x /∈ FV ( M )
11
Jednokrok o vá redukce ˆ je pak k ompatibilní uzáv ˇer relace ˆ β ∪ ˆ η vzhledem
k relaci podter m:
Pro všechn y ter m y M , N , P a všechn y prom ˇenné x
M ˆ β N ⇒ M ˆ N
M ˆ η N ⇒ M ˆ N
M ˆ N ⇒ M P ˆ N P
M ˆ N ⇒ P M ˆ P N
M ˆ N ⇒ λx.M ˆ λx.N
Vícekrok o vá redukce ˆ ∗ je refle xivním a tr ansitivním uzáv ˇerem jednokrok o vé redukce .
12
α -k on v erz e
Systematic ké p ˇrejmeno vání vázaných prom ˇenných ∼ α
Výpo ˇcetní ekviv alence ter m ˚u
≈ = (∼ α ∪ ˆ ∪ ˆ − 1 ) ∗
Rede x , k ontr akt , redukt
Necht ’ M , N jsou ter m y , M ˆ N , necht ’ e xistuje ter m U s jediným výskytem
prom ˇenné x tak, že M = [P /x ]U , N = [Q/x ]U , P ˆ β Q , resp . P ˆ η Q . P ak P
je rede x (β -rede x resp . η -rede x) v M , Q je jeho redukt (β -redukt resp . η -redukt).
13
Fundo v anost
Relace −I ⊆ A 2 je fundo v aná , práv ˇe když nee xistuje nek one ˇcná posloupnost
( a 1 , a 2 , . . .) ∈ A ω tak o vá, že a 1 −I a 2 −I · · · .
Nor mální for ma pr vku a ∈ A .
V ˇeta: Relace redukce ˆ v netypo v aném lambda kalkulu není fundo v aná.
D ˚ukaz: Nap ˇríklad ter m ( λx.x x )( λx.x x ) nemá n.f .
14
K onfluence
Relace −I ⊆ A 2 je k onfluentní , práv ˇe když −I ∗ ◦ J− ∗ ⊆ J− ∗ ◦ −I ∗
V ˇeta: Relace redukce ˆ v lambda kalkulu je k onfluentní.
D ˚usledek: Každý ter m v má nejvýše jedn u n.f .
15
Reduk ˇcní str ategie
Reduk ˇcní str ategie je ˇcáste ˇcné z obr az ení ϕ : − → , které je defino váno práv ˇe na
reducibilních ter mech a pro každý reducibilní ter m M ∈ platí M ˆ ϕ ( M ) .
Necht ’ ϕ je reduk ˇcní str ategie . P ak ϕ -reduk ˇcní posloupnost ter m u M je
b ud ’ k one ˇcná posloupnost M 0 , M 1 , . . . , M k tak o vá, že M 0 = M , M k je n.f .,
∀ i, 0 < i ≤ k .M i = ϕ ( M i− 1 ) ,
anebo nek one ˇcná posloupnost M 0 , M 1 , M 2 , . . . tak o vá, že M 0 = M ,
∀ i > 0 .M i = ϕ ( M i− 1 ) .
16
Nor mální reduk ˇcní str ategie
Nor mální reduk ˇcní str ategie je defino vána:
ϕ n ( M ) = N ⇔ M ˆ N v nejle v ˇejším vn ˇejším rede xu
V ˇeta: Má-li ter m M nor mální for m u N , pak e xistuje k ∈ N tak o vé, že N = ϕ kn ( M ) .
T edy: m ˚uže-li výpo ˇcet sk on ˇcit, pak p ˇri nor mální str ategii sk on ˇcí.
D ˚ukaz viz [Barendregt – Lambda Calculus]
Str iktní reduk ˇcní str ategie
Str iktní reduk ˇcní str ategie je defino vána:
ϕ s ( M ) = N ⇔ M ˆ N v nejle v ˇejším vnit ˇrním rede xu
V ˇeta: Má-li ter m M nek one ˇcné reduk ˇcní posloupnosti, pak ϕ ks ( M ) je defino váno pro
všechna k ∈ N . T edy: m ˚uže-li se výpo ˇcet zacyklit, pak p ˇri str iktní str ategii se zacyklí.
17
Kódo vání dat v ˇcistém lambda kalkulu
Logic ké hodnoty a spojky
Uspo ˇrádané dv ojice
Uspo ˇrádané trojice
Seznam y
P ˇriroz ená ˇcísla a ar itmetic ké oper ace
Strom y
18
Pr a vdiv ostní hodnoty
T r ue = λxλy .x
F alse = λxλy .y
Logic ké spojky
not = λy .y F alse T r ue
if = λxλy λz .x y z
and = λuλv .u v F alse
or = λuλv .u T r ue v
19
Uspo ˇrádané dv ojice
( M , N ) = λz .z M N
fst = λp.p T r ue
snd = λp.p F alse
Uspo ˇrádané trojice
( M , N , P ) = λz .z M N P
proj31 = λt.t ( λxλy λz .x )
proj32 = λt.t ( λxλy λz .y )
proj33 = λt.t ( λxλy λz .z )
20
Seznam y
[ ] = λz .z T r ue F alse F alse
(:) = λxλy λz .z F alse x y
head = λp.p ( λxλy λz .y )
tail = λp.p ( λxλy λz .z )
n ull = λp.p ( λxλy λz .x )
21
Binár ní strom y s ohodnocenými uzly
empty = λg .g T r ue ( λx.x )( λx.x )( λx.x )
for k = λxλy λz λg .g F alse x y z
isempty = λt.t ( λuλxλy λz .u )
root = λt.t ( λuλxλy λz .x )
left = λt.t ( λuλxλy λz .y )
r ight = λt.t ( λuλxλy λz .z )
22
Kódo vání p ˇriroz ených ˇcísel pomocí Churcho vých ˇcíslo v ek
0 = λs z .z
1 = λs z .s z
2 = λs z .s ( s z )
3 = λs z .s ( s ( s z ))
n = λs z .s n z
isz ero = λn.n ( λx. F alse ) T r ue
succ = λn.λs z .n s ( s z )
add = λm n.λs z .m s ( n s z )
m ult = λm n.λs z .m ( n s ) z
po w = λm n.λs z .n m s z (= λm n.n m )
23
succ n ˆ λs z . n s ( s z )
= λs z .( λs z .s n z ) s ( s z )
ˆ λs z .s n ( s z )
= n + 1
add m n ˆ λs z .( λs z .s m z ) s (( λs z .s n z ) s z )
ˆ λs z .( λs z .s m z ) s ( s n z )
ˆ λs z .s m ( s n z )
= m + n
24
m ult m n ˆ λs z .m ( n s ) z
= λs z .( λs z .s m z )(( λs z .s n z ) s ) z
ˆ λs z .( λs z .s m z ) ( λz .s n z ) z
= λs z .( λs z .s m z ) s n z
ˆ λs z .s mn z
= mn
25
po w m n ˆ λsz . n m s z
= λsz .( λsz .s n z )( λsz .s m z ) s z
ˆ λsz .( λsz .s m z ) n s z
ˆ λsz .( λsz .s m z ) n − 1 s m z
ˆ λsz .( λsz .s m z ) n − 2 s m
2
z
ˆ λsz .( λsz .s m z ) n − 3 s m
3
z
.
.
.
ˆ λsz .( λsz .s m z ) s m
n − 1
z
ˆ λsz .s m
n
z
= m n
26
pred = λn.f ( n a b )
a = λq .p ( g q ) ( succ ( g q ))
b = p 0 0
p = λx y z .z x y
f = λz .z T r ue
g = λz .z F alse
27
V ˇeta o pe vném bod ˇe
V ˇeta: Pro každý ter m F e xistuje ter m X tak o vý, že F X ≈ X .
D ˚ukaz: P oložme Y = λf .( λx.f ( x x ))( λx.f ( x x )) , X = Y F .
P ak F X ˆ ◦ ˆ◦ ˆX
P oznámka: T edy každý ter m F má pe vný bod Y F . T er m u Y se ˇríká k ombinátor
pe vného bodu.
P oužití
Necht ’ M je ter m s v olnými výskyty prom ˇenné z a máme rekurzivní definici z = M .
Utv o ˇríme ter m F = λz .M , tj. rekurzivn ˇe defino v anou prom ˇennou z (v olnou v M )
vážeme abstr akcí, takže v F už v olná není. P ˚uv odní rekurzivní definice je ekviv alentní
zápisu z ≈ F z , tj. defino v aná prom ˇenná z m usí vyho v o v at této ekviv alenci. P odle v ˇety
o pe vném bod ˇe je z = Y F = Y ( λz .M )
28
add ≈ λxλy . if isz ero x then y else add ( pred x )( succ y )
add ≈
¡
λf λxλy . if isz ero x then y else f ( pred x )( succ y )
¢
add
add = Y
¡
λf λxλy . if isz ero x then y else f ( pred x )( succ y )
¢
mul t = Y
¡
λf λxλy . if isz ero x then 0 else add ( f ( pred x ) y )
¢
= Y
‡
( λf λxλy . if isz ero x then 0 else
¡
Y ( λg λuλv . if isz ero u then v else g ( pred u )( succ v ))
¢
( f ( pred x ) y )
·
f act = Y
¡
λf λn. if isz ero n then 1 else mul t n ( f ( pred n ))
¢
z er oes = Y ( λs. (:) 0 s )
29
V ˇeta o vícenásobném pe vném bod ˇe
V ˇeta: Pro každých n ter m ˚u F 1 , F 2 , . . . , F n e xistuje n ter m ˚u X 1 , X 2 , . . . , X n tak,
že
X 1 ≈ F 1 X 1 X 2 . . . X n
X 2 ≈ F 2 X 1 X 2 . . . X n
.
.
.
X n ≈ F n X 1 X 2 . . . X n
30
Vícenásobná ( „ vzájemná “ ) rekurz e
X 1 = M 1
.
.
.
X n = M n
X = ( X 1 , . . . , X n ) ≈ ( M 1 , . . . , M n )
X ≈
¡
( λx 1 . . . x n .M 1 ) x 1 . . . x n , . . . , ( λx 1 . . . x n .M n ) x 1 . . . x n
¢
≈
¡
F 1 ( p 1 X ) . . . ( p n X ) , . . . , F n ( p 1 X ) . . . ( p n X )
¢
kde F i = λx 1 . . . x n .M i , p j jsou selektor y .
P odle V ˇety o (jednoduchém) pe vném bod ˇe je
X = Y
‡
λz .
¡
F 1 ( p 1 z ) . . . ( p n z ) , . . . , F n ( p 1 z ) . . . ( p n z )
¢·
31
Vy ˇcíslitelné funkce
ˇCíselné funkce: N n − → 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á)
• (1+) : N → N (následník)
• pr oj n,k : N n → N , pr oj 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í)
32
• 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í rekurz e)
• Každá pr imitivn ˇe vy ˇcíslitelná funkce je vy ˇcíslitelná .
• Je-li funkce g : N n +1 − → N vy ˇcíslitelná, pak f : N n +1 − → N tak o vá, že
f ( y , x 1 , . . . , x n ) = µz .( g ( z , x 1 , . . . , x n ) = y ) , je vy ˇcíslitelná. (µ -rekurz e)
33
Lambda vy ˇcíslitelnost
Def: Funkce f : N n → 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 ) ∈ N n platí
F k 1 k 2 . . . k n ≈ f ( k 1 , k 2 , . . . , k n ) .
P oznámka: Z k onfluence vyplývá F k 1 k 2 . . . k n ˆ f ( k 1 , k 2 , . . . , k n ) .
34
V ˇeta: Každá vy ˇcíslitelná funkce je λ -defino v atená a naopak.
D ˚ukaz:
(1a) Každá totální vy ˇcíslitelná funkce je λ -defino v atelná:
n ula: λx 1 . . . x n . 0
následník: succ
pr ojekce: Jsou-li g : N m → N , h 1 , . . . , h m : N n → N λ -defino v atelné ter m y
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á ter mem
F = λx 1 . . . x n .G ( H 1 x 1 . . . x n ) . . . ( H m x 1 . . . x n ) .
35
primitivní rekurz e: Jsou-li g : N n → N , h : N n +2 → N λ -defino v atelné ter m y
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á ter mem
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 ))
¢
36
obecná (µ ) rekurz e: Je-li g : N n +1 → N λ -defino v atelná ter mem 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á ter mem
F = λy x 1 . . . x n . Y
¡
λhz . if ( eq y ( G z x 1 . . . x n )) z ( h ( succ z ))
¢
0
(1b) 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 .
37
(2) Každá λ -defino v atelná funkce je vy ˇcíslitelná:
T echnic ké detaily d ˚ukazu pr acné a zdlouha vé, nicmén ˇe idea prostá: Sestrojíme TM
(nebo RAM, prog r am v Hask ellu, . . . ), který pro každý ter m F λ -defin ující 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 .
38
Lambda kalkul s k onstantami
Do jazyka p ˇridáme nejvýše spo ˇcetn ˇe mnoho k onstant c 1 , c 2 , . . .
Každá tak o vá k onstanta je ter m.
Definici jedno- a vícekrok o vé redukce rozší ˇríme o δ -redukci :
Pro každou k onstantu c j za v edeme tzv . δ -pr a vidla tv ar u
M 1 ˆ N 1 . . . M k ˆ N k
M ˆ N
P okud p ˇridané k onstanty λ -defin ují vy ˇcíslitelné funkce , tak se vyjad ˇro v ací síla takto
rozší ˇreného lambda kalkulu nezvýší.
P ˇríklad: P ˇridáme k onstanty false , tr ue , not a δ -pr a vidla
not false ˆ tr ue not tr ue ˆ false
M ˆ N
not M ˆ not N
39
Jednoduše typo v aný lambda kalkul
T yp y (typo vé ter m 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 σ
Vloženo: 26.04.2009
Velikost: 335,40 kB
Komentáře
Tento materiál neobsahuje žádné komentáře.
Copyright 2024 unium.cz