Studijní materiály

Zpět

Hromadně přidat materiály

Vzorovy_tahak_2007_06_06

IA014 - Funkcionální programování

Hodnocení materiálu:

Zjednodušená ukázka:

Stáhnout celý tento materiál

β-redukce
(λx.M)N ≈ [N/x]
M
η-redukce
(λx.Mx) ≈ M
Definice
True = λxλy.x
False = λxλy.y
not = λy.y False
True
if = λxλyλz.xyz
and=λuλv.u v
False
or=λuλv.u True v
(M,N)=λz.z MN
fst = λp.p True
snd = λp.p False
[]= λz.z T F F
(:)=λxyz.z F x y
zeroes=Y(λz.(:)
0 s)
Churchovy čísl.
0 = λs.z z
1 = λs.z sz
n = λs.z s
n
z
KOMBINÁTORY S,K,I,B,C
S :: (α→β→γ)→(α→β)→α→γ
S gfx → fx(gx), S ≈ λfλgλx.fx(gx)
K :: α→β→α, K xy → x, K ≈ λxλy.x
I :: α→α, I x → x, I ≈ λx.x
KOMBINÁTOR PEVNÉHO BODU
Pro každý term F existuje term X takový,
že F X ≈ X.
YF ≈ F(YF), YF → F(YF) → F(F(YF)) ...
z ≈ F z, z = YF = Y(λz.M)
IMPREDIKATIVNÍ TYPOVÝ SYSTÉM I
Vícenásobná rekurze
X = Y(λz.(F
1
(p
1
z)...(p
n
z), ..., F
n
(p
1
z)...(p
n
z))) p ... selektor
Příklad 1:
even = λn. if (iszero n) then True else (odd(pred n))
odd = λn. if (iszero n) then False else (even(pred n))
nejprve vezmeme novou funkci z, která bude tvořena dvojicí (podle
počtu vzájemně rekurzivních funkcí)
z = (even, odd) = (λn. if (iszero n) then True else (odd(pred n)),
λn. if (iszero n) then False else (even(pred n)))
nahradíme funkce odd a even selektory na typu z
z = (λn. if (iszero n) then True else (snd z (pred n)),
λn. if (iszero n) then False else (fst z (pred n)))
z = Y(λz.(λn. if (iszero n) then True else (snd z (pred n)),
λn. if (iszero n) then False else (fst z (pred n))))
SUPERKOMBINÁTORY, λ-lifting
Příklad: Převod termu do superkomb. termu
λxλy.F(λz.Fxz)(λz.Fzzy)(λz.Fzzx)
1. α x z = F x z
λxλy.F(αx)(λz.Fzzy)(λz.Fzzx)
2. β y z = F z z y
λxλy.F(αx)(βy)(λz.Fzzx)
3. γ x z = F z z x
pouhým přejmenováním x na y získáme β ≈
γ = β
λxλy.F(αx)(βy)(βx)
4. δ x y = F(αx)(βy)(βx)
λx.δx →
η
δ
výsledné superkombinátory: α, β, δ
IM → M, I ≈ SKK
SMNP → MP(NP)
KMN → M
BMNP → M(NP)
CMNP → MPN
S(KP)Q → BPQ
SP(KQ) → CPQ
S(KP)(KQ) → K(PQ)
S(KP)I → P
Příklad: Θ xyz → zxy
λxλyλz.zxy
λxλy.S(λz.zx)(λz.y)
λxλy.S(S(λz.z)(λz.x))(Ky)
λxλy.S(S(I)(Kx))(Ky)
λxλy.S(CIx)(Ky)
λxλy.C(CIx)y η-redukce
λx.C(CIx)
S(λx.C)(λx.CIx)
S(KC)(CI)
BC(CI)
Příklad 1:
from :: Int → [Int]
from n = n : from(succ n)
zafixovat funkci a její proměn

Stáhnout celý tento materiál

1 2 3

Další

Vloženo: 26.04.2009

Velikost: 61,35 kB

Stáhnout celý tento materiál

Komentáře

Tento materiál neobsahuje žádné komentáře.

Mohlo by tě zajímat:

Skupina předmětu IA014 - Funkcionální programování
Reference vyučujících předmětu IA014 - Funkcionální programování