- 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, B204
K onsultace: st ˇreda 18.30–20.00, B419
Zk oušky: ˇcer v en 2007
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 a jejich vlastnosti. 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
P ˇre v od k onstr ukcí funkcionálního jazyka do rozší ˇreného lambda kalkulu
let length [] = 0
length (_:t) = 1 + length t
u = [1,2,3]
in length u
definice podle vz or u → definice s par ametr y
let length s = if null s then 0 else 1 + length (tail s)
u = [1,2,3]
in length u
if je funkce
let length s = if (null s) 0 (1 + length (tail s))
u = [1,2,3]
in length u
5
„ syntaktic ký cukr “ (infixo vé operátor y , seznamo vá syntax . . . )
let length s = if (null s) 0 ((+) 1 (length (tail s)))
u = (:) 1 ((:) 2 ((:) 3 []))
in length u
definice funkce do tv ar u jméno = lambda abstr akce
let length = λ s. if (null s) 0 ((+) 1 (length (tail s)))
u = (:) 1 ((:) 2 ((:) 3 []))
in length u
rekursivní definice → použití k ombinátor u pe vného bodu
let length = Y ( λlscript λ s. if (null s) 0 ((+) 1 ( lscript (tail s)))
u = (:) 1 ((:) 2 ((:) 3 [])))
in length u
6
(lokální) definice s let → výr az s abstr akcí a aplikací
( λ length λ u. length u)
( Y ( λlscript λ s. if (null s) 0 ((+) 1 ( lscript (tail s)))))
( (:) 1 ((:) 2 ((:) 3 [])))
k onstanty → sim ulace v ˇcistém lambda kalkulu
7
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)
8
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 ) . . .))
9
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 ) = ∅ ⇒ σ M = M
10
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 }
11
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á.
12
Sémantika
Sémantiku lz e zadat b ud ’ denota ˇcn ˇe ( [[ _ ]] : 99K− 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 )
13
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 .
14
α -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 , redukt (k ontr aktum)
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 , a Q je jeho redukt (β -redukt resp . η -redukt).
15
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 je tak o vý pr v ek b ∈ A , pro který platí a −I ∗ b
a sou ˇcasn ˇe nee xistuje pr v ek c ∈ A , pro který b y platilo b −I c .
P ˇríklad: T er m ( λxλy .y x ) t u má nor mální for m u u t .
T er m ( λy .u ) (( λx.x x )( λx.x x )) má n. f. u , ale i nek one ˇcnou reduk ˇcní posloupnost.
T er m ( λx.x x )( λx.x x ) nemá nor mální for m u.
D ˚usledek: Relace redukce ˆ v netypo v aném lambda kalkulu není fundo v aná.
16
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 nor mální for m u.
17
Reduk ˇcní str ategie
Reduk ˇcní str ategie je ˇcáste ˇcné z obr az ení ϕ : 99K− , 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 ) .
18
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í.
19
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 ).
20
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 .
Každá hnf je také whnf . Opak neplatí, nap ˇr. λx. ( λy .y ) z není hnf .
P oznámka: Pr aktic ky použív ané systém y redukují do slabé hla v o vé nor mální for m y ,
tj. neredukují v t ˇelech lambda abstr akcí.
21
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
22
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
23
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 )
24
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 )
25
Binár ní strom y s ohodnocenými uzly
empty = λg .g T r ue ( λx.x )( λx.x )( λx.x )
node = λ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 )
26
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 )
27
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
28
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
29
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
30
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
31
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 rekursivní definici tv ar u
z = M . Utv o ˇríme ter m F = λz .M , tj. rekursivn ˇ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í rekursivní 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 )
32
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 )
¢
m ult = Y
¡
λf λxλy . if isz ero x then 0 else add ( f ( pred x ) y ) 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 ) y
·
fact = Y
¡
λf λn. if isz ero n then 1 else m ult n ( f ( pred n ))
¢
z eroes = Y ( λs. (:) 0 s )
33
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
34
Vícenásobná (vzájemná) rekurse
X 1 = M 1
.
.
.
X n = M n
X ≈ ( M 1 , . . . , M n )
X ≈
¡
F 1 X 1 . . . X n , . . . , F n X 1 . . . X n
¢
X ≈
¡
F 1 ( p 1 X ) . . . ( p n X ) , . . . , F n ( p 1 X ) . . . ( p n X )
¢
X ≈
‡
λz .
¡
F 1 ( p 1 z ) . . . ( p n z ) , . . . , F n ( p 1 z ) . . . ( p n z )
¢·
X
kde X = ( X 1 , . . . , X n ) , F i = λx 1 . . . x n .[x 1 /X 1 , . . . , x n /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 )
¢·
35
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 fals
Vloženo: 26.04.2009
Velikost: 360,09 kB
Komentáře
Tento materiál neobsahuje žádné komentáře.
Copyright 2024 unium.cz