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

né
from = Y(λfλn.n : f (succ n))
Příklad 1:
data Bitlist = Nil | ConsOn Bitlist | ConsOff Bitlist
zvolíme si nějaký typ, který bude reprezentovat typ Bitlist, např: τ
Bitlist = Vτ.τ→(τ→τ)→(τ→τ)→τ
Příklad 2:
data Tree = Empty | Node [Int] Tree Tree
t = f [] where f s = Node s (f(0:s)) (f(1:s))
nejprve vezmeme funkci f
f = Y(λφλs.Node s (φ(0:s)) (φ(1:s)))
pak pomocí f vyjádříme funkci t
t = Y(λφλs.Node s (φ(0:s)) (φ(1:s))) []
Příklad 3:
data Trojice a b c = T a b c
Trojice α β γ = Vτ.(α→β→γ→τ)→τ
Příklad 2:
data Either a b = Left a | Right b
Either α β = Vτ.(α→τ)→(β→τ)→τ
Příklad 3:
Y(λx."Pes...slov:„"++x++"”")
Příklad 4:
cycl :: [a]→[a], cycl s = s ++ cycl s
chceme ziskat definici funkce cycl ve tvaru: cycl =Y(________),
v definici ‘cycl s = s ++ cycl s‘ převedeme s doprava a zavedeme
novou funkci f, kterou nahradíme funkci cycl.
λfλs.s ++ f s, cycl = Y(λfλs.s ++ f s)
λx.M → KM, λx.Mx → M, λx.x → I
λx.y → Ky, λx.E
1
E
2
→ S(λx.E
1
)(λx.E
2
)
λx.PQ → S(λx.P)(λx.Q) →* S(KP)(KQ)
λx.Mx → S(λx.M)(λx.x) →* S(KM)I
IMPREDIKATIVNÍ TYPOVÝ SYSTÉM II
Odvozovací pravidla pro predikativní typový
systém a termy s let.
Axiom proměnné (VAR)
Let-výraz (LET)
Aplikace (APP)
Specializace (SPEC)
Generalizace (GEN)
Zeslabení (W)
Abstrakce (ABS)
Axiomy konstant (CON)
Γ,x :: σ ▷ x :: σ
Γ ▷ let x = N in M :: τ
Γ ▷ NM :: τ
Γ ▷ M :: [τ/α]σ
Γ ▷ M :: Vα.σ
Γ,x :: τ ▷ M :: σ
Γ ▷ λx.M :: σ→τ
(τ typ)
α≠FV(Γ)
x≠FV(M)Γ ▷ N :: σ Γ,x :: σ ▷ M :: τ
Γ ▷ λxλy.x y 0 :: VαVβ.(α → Nat → β) → α → β Δ ▷ f f (+) :: Nat
Δ ▷ f f :: (Nat→Nat→Nat) → Nat Δ ▷ (+) :: Nat→Nat→Nat
Δ ▷ f :: [*1]((Nat→Nat→Nat) → Nat → Nat) → (Nat→Nat→Nat) → Nat Δ ▷ f :: [*2](Nat→Nat→Nat) → Nat → Nat
[*1] = [Nat→Nat→Nat/α, Nat/β]
[*2] = [Nat/α, Nat/β]
Δ ▷ f :: VαVβ.(α → Nat → β) → α → βΔ ▷ f :: VαVβ.(α → Nat → β) → α → β
Γ ▷ N :: σ→τ Γ ▷ M :: σ
Γ ▷ M :: Vα.σ
Γ ▷ M :: σ
Γ ▷ M :: σ
Γ,x :: σ ▷ M :: τ
▷ 0 :: Nat ▷ False :: Bool
Příklad 1:
0 :: Nat, (+) :: Nat → Nat → Nat. Výraz: let f = λxλy.x y 0 in f f (+), Δ = {f :: VαVβ.(α → Nat → β) → α → β}
Příklad 2:
0 :: Nat, succ :: Nat → Nat. Výraz: let f = λxλy.x(x y) in f f succ 0, Δ

Stáhnout celý tento materiál

Předchozí

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í