ALP 1
Dozentin
Margarita Esponda
E-Mail:esponda@inf.fu-berlin.de
Homepage: http://www.inf.fu-berlin.de/~esponda
Sprechstunde: Fr. 10-12 Uhr
Modulhomepage: http://www.inf.fu-berlin.de/lehre/WS12/ALP1/index.htm
Inhalt des Moduls
(cp aus dem kvv)
Grundlagen der Berechenbarkeit:
- Lambda-Kalkül
- primitive Rekursion
- µ-Rekursion
Einführung in die Funktionale Programmierung (Haskell):
- Syntax (Backus-Naur-Form)
- primitive Datentypen, Listen, Tupel, Zeichenketten
- Ausdrücke, Funktionsdefinitionen, Rekursion und Iteration
- Funktionen höherer Ordnung, Polymorphie
- Typsystem, Typherleitung und –überprüfung
- Algebraische und abstrakte Datentypen
- Ein- und Ausgabe
- Such- und Sortieralgorithmen
Beweisen von Programmeigenschaften:
- Termersetzung
- strukturelle Induktion
- Terminierung
Implementierung und Programmiertechnik:
- Auswertungsstrategien für funktionale Programme
- Modularer Programmentwurf
Literatur
- "The Craft of Functional Programming"
- "Real World Haskell"
- "Programming in Haskell"
computer verbot |aufgehoben wenn man mitschreibt
ipad verbot
Warum funktionales programmieren?
warum haskell?
programmiersprach-kram. siehe folien:
http://www.inf.fu-berlin.de/lehre/WS12/ALP1/lectures.htm
S≡λwyz.y(wyx)
S(λsz.s^n z)
(λwyx.y(wyx))(λsz.s^n (z))
(λyx.y((λsz.s^n (z))yx)
(λyx.y((λz.y^n (z))x)
λyx.y(y^n (x))
λyx.y^(n+1)(x)=n+1
Multiplikation
λa.2(3a) |expandiere 2
λa.(λyx.y(y(x)))(3a)
λa.(λx.(3a)((3a)(x)))
λa.(λx.(3a)(3a((λik.i(i(i(k))))a)(x))
λa.(λx.(3a)(a(a(a(x)))))
λa.λx(λsz.s(s(s(z)))a))(a(a(a(x)))
λax.(λz.a(a(a(z)))(a(a(a(x))))
λax.a(a(a(a(a(a(x))))))
T≡λxy.x
F≡λxy.y
Λ=λxy.xyF
ΛTT=>(λxy.xyF)TT
=>TTF
=>T
v≡λxy.xTy
v=TF=>(λxy.xTy)TF
=>TTF
=>T
Z2=>(λx.xF!F)2
=>2F!F
=>(λsz.s(s(z)))F!F
=>(λz.F(F(z)))!F
=>(F(F(!)))F
!≡λx.xFT
=>(F(F(λx.xFT)))F
=>(F((λxy.y)(#x.xFT)))F
=>(F(λy.y))F
=>((λxy.y)(#y.y))F
=>(λy.y)F
=>F
λy.yx FV:y
λx.(λx.xa)x |x hinter der Klammer wird zu k
λk.(λx.xa)k
07.01.2013
Λ≡λxy.xyF T≡λxy.x
F≡λxy.y
T a b=>(λxy.x)ab
=>a
F a b=>(λxy.y)ab
=>b
ΛTT=>(vxy.xyF)TT
=>TTF
=>T
Λ≡λxy.λyx
ΛTT=>(λxy.xyx)TT
=>TTT
=>T
ΛFF=>(λxy.xyx)FF
=>FFF
=>F
ΛTF=>TFT=>F
ΛFT=>FTF=>F
(λxy.xyF)AB =>ABF
(λxy.xyx)AB=>ABA
A≡λx.x
B≡λx.x
(λxy.xyF)AA =>AAF
(λxy.xyx)AA=>AAA
(λx.x)(λx.x)F
=> (λx.x)F
=> F
(λx.x)(λx.x)(λx.x)
=>(λx.x)(λx.x)
=>(λx.x)
R≡(λrn.Zn(/) (nS(r(Pn))))
YR3=>R(YR)3
=>(λrn.Zn(/)(nS(r(Pn))))(YR)3
=>Z3(/)(3S((YR)(P3))))
=>F(/)(.....)
=>3S((YR)(P3)))
=>3S((R(YR))(P3)))
=>3S(((λrn.Zn(/)(nS(r(Pn))))(YR))(P3[2]))
=>3S(Z2(/)(2S((YR)(P2))))
=>3S(2S((YR)1))
=>3S(2S(1S(Z(/)(/).....)
=>3S(2S(1S((/)))
=>6
!≡ (λrn.Zn1(*n(r(Pn))))
Y!≡Y( || )
Y!=>!Y!=>(λrn.Zn1(*n(r(Pn))))(y!)0
=>Z01(*0((Y!)(0))))
=>1
FIB≡(λrn.=n0 0(=n1 1(+(r(Pn)(r(P(Pn))))))
YFIB 3=>FIB(Y FIB)3=>Y(λrn.=n00(=11(+(r(Pn)(r(P(Pn)))))))(Y FIB)3
=>=3 0 0[F](=3 1 1[F]......
=>+((Y FIB)(P3[2])((Y FIB)(P(P3)[1])))
=>+(........................................
0≡ λz.z 0 0
1≡λz.z 0 1
-1≡λz.z 1 0
T(/)
(λz.z 0 0)T
T 0 0 => 0
(a,b)+(c,d) => (a+c,b+d)
λxy.(λz.z(+(xT)(yT))(+(xF)(yF))
(λxy.(λz.z(+(xT)(yT))(+(xF)(yF))))1 2
=>(λz.z(+(1T)(2T))(+(1F)(2F)))
=>(λz.z(+ 0 0)(+ 1 2))
=>(λz.z 0 3)
09.01.2013
Listen im Lambda-Kalkül
(T,_, _) []
(F,a,a) :ab |erstes a ist der Kopf der Liste, das zweite a der Rest der Liste
NIL≡ (λx.xTFF) |Lambda-Ausdruck für die Leere Liste
TNIL≡(λx.x(λabc.a))
{TNIL}{NIL}
(λx.x(λabc.a)(λx.xTFF)
=>(λx.xTFF(λabc.a))
=>(λabc.a)TFF
=>T
[1]≡(λx.xF(λsz.s(z))(λx.xTFF))
:≡(λabz.zFab)
:1{NIL}≡(λabz.zFb)(λsz.(s(z))(λx.xTFF)
HEAD≡λx.x(λabc.b)
TAIL≡λx.x(λabc.c)
[1,2]≡λx.xF(λsz.s(z)(λx.xF(λsz.s(s(z)))(λx.xTFF))
LEN≡(λrl{TNIL}l(/)(S(r({TAIL}l))))
Y{LEN}{NIL}=>(/)
Y{LEN}{NIL}=>{LEN}(Y{LEN}){NIL}
=>(λrl.{TNL}l(/)(S(r({TAIL}l))))(Y{LEN}){NIL}
=>{TNIL}{NIL}(/)(S(Y{LEN})({TAIL}{NIL}))
=>(/)
"+xy(za)2"
alles was innerhalb der Klammer steht wird als Tupel gelesen
bei "Klammerschachtelung" ist ab der zweiten Klammer ein Zähler nötig
"(" ->Zähl+1, ")" ->Zähl-1
parser "xy"
=>parse Nil "xy"
=>parse(Var "x") "y"
=>parse (APP(Var "x")(Var "y")[])
=>APP(Var "x")(Var "y")
parse Nil "(xy)z"
("xy","z")=extract "xy)z"
λx.xy (in Parser (1. Version) möglich)
λxy.yz (in Parser (2. Version) möglich)
14.01.2013
(λx.xy) (λy.z(y))=>
E_2 E_1
(λx.x)E_1=>E_1
(λx.y)E_1=>y
(λx.(ab) (xy))E1=>
E_2 E_3
=>(ab)(E_1 y)
d)(λx.(λx.xy))E_1=>λx.xy
E_2 E_2
e)(λx.(λy.zy))E_1=>λy.zy
f)(λx.(λy.zyx))E_1=>λy.zyE_1 y!€FV(E_1)
E_2
g)(λx.(λy.zyx))(ya)=>
(λx.(λk.zkx))(ya)=>λk.zk(ya)
Call-By-Name
Λ, λ, ≡