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: 
Einführung in die Funktionale Programmierung (Haskell): 
Beweisen von Programmeigenschaften: 
Implementierung und Programmiertechnik:

Literatur


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



Λ, λ, ≡