4. Lambda Kalkül

Lambda Kalkül

  • ?

    Hallo Forum,

    ich komme im Lambda Kalkül bei der Auswertung nicht weiter. Es geht um die Anleitung aus dem Lambda Wiki Artikel: http://www.jugglink.de/external/lambda/lambda.zip

    Frage 1:
    Wahr := Lx.Ly.x
    Falsch := Lx.Ly.y
    AND := La.Lb.ab(Lx.Ly.y)

    Was ist nun "W AND F"?

    AND W F
    (La.Lb.ab(Lx.Ly.y)) (Lx.Ly.x) (Lx.Ly.y)

    Ich könnte doch jetzt das F in das erste x von W einsetzen?
    (La.Lb.ab(Lx.Ly.y)) (Ly.(Lx.Ly.y))
    Nun den zweiten Klammerausdruck in das a:
    Lb.((Ly.(Lx.Ly.y)) b (Lx.Ly.y))

    Frage2 zur Lambda Auswertung auf Folie 40:
    True:= Lxy.x
    False:= Lxy.y

    Dieses soll If-Then-Else sein:
    Lbxy.bxy // Wobei b entweder True oder False ist.

    In Klammerschreibweise würde doch dann das y auf das b abgebildet werden?
    (Lb.(Lx.(Ly.b)x)y)
    Auf Folie 37/38 steht nähmlich:
    Die Funktionsabstraktion ist rechtsassoziativ:
    Lxyz.A = (Lx (Ly (Lz.A)))
    Die Funktionsapplikation ist linksassoziativ:
    Fxyz = (((F x) y) z)

    Genauso müsste man doch auch True auswerten?
    True:= Lx(Ly.x)

    Wie man den Ausdruck "richtig" auswertet steht dann auf Folie 41. Aber widerspricht das nicht den Regeln auf Folie 37/38?

    Wie es "richtig" gehen sollte steht dabei. Das widerspricht jedoch meiner Meinung nach den Regeln!?

    Vielen Dank

    Tim

    0
  • X

    Ich habe gerade nicht genug Zeit es genau anzuschauen, aber auf den ersten Blick sieht es aus als würdest du die "heimliche" Klammerung missachten: Lambda-Terme der Form t1 t2 t3 ... tn werden von Links nach rechts geklammert: ((((t1 t2) t3) ...) tn)
    Das erste wäre also:

    (((La.Lb.ab(Lx.Ly.y)) (Lx.Ly.x)) (Lx.Ly.y))

    .
    Du setzt also als erstes das #t für a ein:

    (((Lb.(Lx.Ly.x)b(Lx.Ly.y))(Lx.Ly.y))

    Dann das #f für b:

    (Lx.Ly.x)(Lx.Ly.y)(Lx.Ly.y)

    Auch hier gilt die Klammerung von Links nach Rechts:

    (((Lx.Ly.x)(Lx.Ly.y))(Lx.Ly.y))

    <=>

    (Ly.(Lx.Ly.y))(Lx.Ly.y)

    Jetzt löst du das letzte Lambda auf. Da an das y des äußersten Lambdas des ersten Terms keine Variablen mehr gebunden sind, fliegt das einfach raus und übrig bleibt:

    (Lx.Ly.y)

    => #f, passt also.

    Zum zweiten Teil:
    Lbxy.bxy

    Die "rechtsassoziative Abstraktion" wäre in dem Fall:

    (Lb.(Lx.(Ly.bxy)))

    Nach deiner Regel (Lxyz.A = (Lx (Ly (Lz.A)))) wäre also A = bxy.
    A wäre jetzt eine Applikation, die linksassoziativ geklammert wird: ((b x) y)

    Setzt du das jetzt für dein "A" ein kriegst du sowas:

    (Lb.(Lx.(Ly.((bx)y))))

    Dann sollte das if auch funktionieren...
    Verzeih' mir eventuell falsch abgezählte Klammern 😃

    0
  • ?

    Die Einsetzungsregel habe ich bisher nicht wahrgenommen. Jetzt hat es Klick gemacht. Vielen Dank XDVD 🙂

    0
Anmelden zum Antworten