3. Lambda Kalkül

Lambda Kalkül

  • B

    Christoph schrieb:

    Mathematisch ist das kein Problem, weil Funktionen Objekte sind, die man vergleichen kann. Nur wenn man zu nah an einer Programmiersprache bleibt, kann man Funktionen nicht sinnvoll vergleichen.

    Wie vergleicht man denn Funktionen im Lambda-Kalkül? Da stellen sich einige Probleme auf. Man definiert ja die Gleichheit folgendermaßen: f=g <=> forall h fh=gh.
    Erstes Problem: Das ist ja rekursiv definiert. Ist das überhaupt *wohldefiniert*?
    Zweites Problem: Falls ja, ist diese Definition berechenbar, d.h. kann es überhaupt eine Funktion im Lambda-Kalkül geben, die zwei Funktionen vergleicht? (Wäre AFAICS äquivalent zum Halteproblem.)

    0
  • C

    Bashar schrieb:

    Christoph schrieb:

    Mathematisch ist das kein Problem, weil Funktionen Objekte sind, die man vergleichen kann. Nur wenn man zu nah an einer Programmiersprache bleibt, kann man Funktionen nicht sinnvoll vergleichen.

    Wie vergleicht man denn Funktionen im Lambda-Kalkül? Da stellen sich einige Probleme auf. Man definiert ja die Gleichheit folgendermaßen: f=g <=> forall h fh=gh.
    Erstes Problem: Das ist ja rekursiv definiert. Ist das überhaupt *wohldefiniert*?

    Das ist genau das Problem, eine denotationale Semantik zu finden.

    Eine denotationale Semantik ordnet jedem lambda-Term ein mathematisches Objekt (Funktion) zu, die man dann auf natürliche Weise vergleichen kann. Die Schwierigkeit liegt darin, so eine Zuordnung "lambda-Term -> mathematisches Objekt" zu finden. Ich hab das mal beim typisiertem lambda-Kalkül mit Basistyp "integer" gesehen; dort lief es darauf hinaus, für jeden Typ eine spezielle partiell geordnete Menge zu definieren und jeden Term auf ein Objekt der vom Typ passenden Menge abzubilden.

    Die Menge vom Typ "nat" (natürliche Zahlen) war $$\mathbb{N} \cup {\bot}$$, wobei $$\bot$$ die Semantik des nicht-terminierenden Programms ist. Die partielle Ordnung darauf ist:
    Für $$n \in \mathbb{N}$$ gilt $$\bot < n$$ und für nichts sonst gilt $$a < b$$.

    Die Menge vom Typ "nat -> nat" war dann definiert als die Menge aller stetigen Funktionen von "nat" nach "nat". Stetigkeit bedeutet hier, dass die Funktion gerichtete Suprema erhält (Continuity).

    Alles in allem wird das eine relativ aufwendige Konstruktion, vor allem, wenn man möchte, dass die denotationale Semantik bestimmte Eigenschaften hat.

    Bashar schrieb:

    Zweites Problem: Falls ja, ist diese Definition berechenbar, d.h. kann es überhaupt eine Funktion im Lambda-Kalkül geben, die zwei Funktionen vergleicht? (Wäre AFAICS äquivalent zum Halteproblem.)

    Stimmt. Berechenbar wird die Gleichheit nicht werden, auch wenn man eine gute denotationale Semantik gefunden hat.

    0
  • B

    Christoph schrieb:

    Eine denotationale Semantik ordnet jedem lambda-Term ein mathematisches Objekt (Funktion) zu, die man dann auf natürliche Weise vergleichen kann.[...]

    Die Menge vom Typ "nat -> nat" war dann definiert als die Menge aller stetigen Funktionen von "nat" nach "nat". Stetigkeit bedeutet hier, dass die Funktion gerichtete Suprema erhält (Continuity).

    Uff, da muss ich erstmal schlucken. Aber danke, das sieht sehr interessant aus, kommt definitiv auf die TODO-Liste.

    0
  • H

    Lambda ist ne Weile her bei mir, aber ich versuche es mal.

    Ishildur schrieb:

    @knivil
    Folie 42: Natürliche Zahlen
    ------------------------------
    F^n(A) (die n-malige Anwendung von F auf A) wird induktiv blah blah blah...
    Ok, das verstehe ich, aber wo steht geschrieben, dass F den Wert A um genau 1 inkrementiert?

    Nirgens. Du musst dich von der mathematischen Sichtweise von Funktionen ein bisschen lösen und im Kalkül denken. Es gibt keine Zahlen. Es gibt Objekte und Terme aus solchen Objekten, die ich nach den bekannten Regeln umschreiben darf. Um nun Zahlen zu modellieren macht man einfach folgendes, man einigt sich auf eine Kodierung durch die im Kalkül vorhandenen Objekte. Dafür gibt es dann aber auch verschiedene Varianten.
    Analog dazu ist die Turingmaschine. Diese hat auch nur ein Bandalphabet und keine Zahlen in dem Sinne zur Verfügung. Auch dort einigen wir uns auf eine Kodierung der Zahlen um ein Problem zu lösen. Z.B. a = 1, aa = 2, etc ...

    Ishildur schrieb:

    Auf der gleichen Folie steht: z_n ≡ λfx.f^n(x)
    Moment mal, plötzlich ist der gebundene Parameter f eine Funktion oder was?

    Da wir uns im ungetypten Kalkül bewegen, kann ein gebundener Parameter grundsätzlich jeder beliebige Term sein, denn du kannst jeden beliebigen Term applizieren. Wenn du nun einen Term mit gebundenen Variablen als Funktion interpretierst und diesen applizierst, ja dann ist f eine Funktion. An der Stelle glaube zumindest ich, dass die Interpretation einer Zahl als Funktion die n mal auf sich selbst angewendet wird zwar ein schönes Bild ist, aber nicht 100% stimmt. In Wirklichkeit sagen wir dort einfach, die Zahl n hat folgende Form. Wenn wir dann nach 20 Umformungen mal etwas in dieser Form übrig haben, können wir das Ergebnis wieder als Zahl interpretieren.

    Ishildur schrieb:

    Folie 43: Beispiele für Zahlen
    ------------------------------
    Meinen wir die Zahl Drei (z_3), so schreiben wir also:
    (λfx.f(f(f(x)))
    Irgendwie geht dieser Term davon aus, dass x = 0 ist? Aber wo steht das geschrieben? Ich meine ich kann ja an einer Mathprüfung auch nicht einfach einer Funktion eine uninitialisierte Variable x übergeben und anschliessend (Bei der Prüfungsbesprechung) behaupten, x wäre natürlich 3.1415 gewesen, das wäre doch klar...

    Der Term geht davon aus, das x eben x ist. Applizieren wir da noch was drauf, bekommen wir höchst wahrscheinlich einen Term, der sich nichtmehr als Zahl interpretieren lässt. Eine Variable steht im Lambda Kalkül nicht für eine Zahl sondern ist einfach ein Objekt (Das sich dann natürlich abhängig von seiner Form interpretieren lässt).

    Ishildur schrieb:

    Folie 10 Funktionsapplikation:
    ------------------------------
    F A beutet, dass die Funktion F auf den Ausdruck A angewandt wird.

    Wird in der Regel so interpretiert.

    Ishildur schrieb:

    Wieso schreibt man nun plötzlich überall: 3 ≡ λfx.f(f(f(x))) ?
    Müsste es dann nicht wenn schon: 3 ≡ λfx.(f (f (f x))) geschrieben sein?

    Das ist beides äquivalent. Wir können fx.(f (f (f x))) auch als fx.f (f (f x)) schreiben, denn es gibt eine Regel, wie in so einem Fall der Term zu interpretieren ist. Diese besagt, dass alles was rechts vom Punkt kommt zusammengehört, soweit wie möglich. Will man etwas anderes müsste man eben Klammern setzen. Schließlich kannst du jederzeit statt x ein (x) schreiben und wir sind bei fx.f (f (f (x))). Ich bevorzuge aber auch deine Klammerweise.

    0
  • ?

    Verständnisfrage:

    Die Zahl 3 sei (λfx.f(f(f(x))) . Kann ich das in Analogie sehen zu dem, was manche Interpreter "introspektiv" nennen? Also Interpreter, die eine Möglichkeit bieten, in ein Objekt hineinzuschauen, zB wenn's eine Funktion ist, die Definition oder die "geclosurten" Werte zu sehen. Mit so einer Möglichkeit könnte ich nämlich durchaus in manchen Fällen prüfen, ob zwei Funktionen gleich sind, zB sind sie gleich, wenn ihre Definitionen gleich sind.

    Stimmt das zumindest ein bisschen?
    🙂

    0
  • C

    µngbd schrieb:

    Verständnisfrage:

    Die Zahl 3 sei (λfx.f(f(f(x))) . Kann ich das in Analogie sehen zu dem, was manche Interpreter "introspektiv" nennen? Also Interpreter, die eine Möglichkeit bieten, in ein Objekt hineinzuschauen, zB wenn's eine Funktion ist, die Definition oder die "geclosurten" Werte zu sehen. Mit so einer Möglichkeit könnte ich nämlich durchaus in manchen Fällen prüfen, ob zwei Funktionen gleich sind, zB sind sie gleich, wenn ihre Definitionen gleich sind.

    Ja, das geht im Prinzip. Man kann in C++ z.B. auch Funktionszeiger vergleichen und sagen "wenn die gleich sind, sind die Funktionen gleich". Das sind alles Äquivalenzrelationen, aber aus mathematischer Sicht sind die eben nur selten nützlich.

    Man kann auch im lambda-Kalkül die Zahl 3 direkt darstellen oder als 1+1+1 schreiben, mit der Funktion für Addition. Ein Interpreter, der in den Code einer Funktion hineinschauen kann, wird diese beiden Darstellungen erstmal als unterschiedlich ansehen, obwohl beide dieselbe Zahl beschreiben.

    0
  • K

    Wie vergleicht man denn Funktionen im Lambda-Kalkül?

    Es gibt keinen Algorithmus, der entscheiden kann, ob zwei beliebige Lambda-Ausdruecke aequivalent sind.

    0
  • ?

    knivil schrieb:

    Es gibt keinen Algorithmus, der entscheiden kann, ob zwei Lambda-Ausdruecke aequivalent sind.

    Es gibt keinen Algorithmus, der in jedem Fall entscheiden kann, ob zwei Lambda-Ausdruecke aequivalent sind.
    🙂

    0
  • K

    Um ehrlich zu sein, habe ich auch ueber den Zusatz nachgedacht. Entschied mich aber dagegen, da "zwei Lambda-Ausdruecke" schon allgemein genug ist. Fuer dich habe ich es aber noch kurz hineineditiert. 🙂

    0
  • ?

    knivil schrieb:

    Fuer dich habe ich es aber noch kurz hineineditiert. 🙂

    Das finde ich nett.
    🙂

    0
  • I

    @knivil & µngbd
    Hei ihr beiden, ich habe da noch eine Frage zum Lambda Kalkül, die ich nicht verstehe:

    λx.(λx.xx)

    1. Welches x innerhalb des Funktionskörpers der rechten Funktion ist denn nun an den Parameter der linken Funktion gebunden?

    2. Was bedeutet überhaupt xx?
    Ich meine, es ist weder ein Symbol, noch eine Applikation? Müsste es nicht vielmehr x x heissen oder ist xx OK?

    Vielen Danke für eure Geduld

    0
  • C

    Ishildur schrieb:

    λx.(λx.xx)

    1. Welches x innerhalb des Funktionskörpers der rechten Funktion ist denn nun an den Parameter der linken Funktion gebunden?

    Es zählt immer die innerste lambda-Abstraktion. Deswegen ist "λx.(λx.xx)" das gleiche wie "λy.(λx.xx)".

    Ishildur schrieb:

    2. Was bedeutet überhaupt xx?
    Ich meine, es ist weder ein Symbol, noch eine Applikation? Müsste es nicht vielmehr x x heissen oder ist xx OK?

    Variablen bestehen in der Mathematik per Konvention immer aus einem Buchstaben (fast immer). Deswegen ist "xx" zu lesen als "x x", die Anwendungs der Funktion "x" auf den Parameter "x".

    0
  • I

    "λx.(λx.xx)" das gleiche wie "λy.(λx.xx)".

    Bist du dir da ganz sicher? Sollte das y nicht auch in der rechten Funktion vorkommen?

    0
  • ?

    Ishildur schrieb:

    Sollte das y nicht auch in der rechten Funktion vorkommen?

    Schwer zu sagen, oft schon. Man kann aber natürlich auch Argumente ignorieren, und muss das afaik auch manchmal tun.

    Wenn xx eine Variable sein soll, wäre sie frei, und müsste irgendwo im Kontext zu finden sein (oder sie ist absichtlich frei, damit sie in irgendeinem Kontext passend festgelegt wird).

    Christophs Interpretation halte ich für wahrscheinlicher, das könnte man durchaus maschinell interpretieren, Scheme: (lambda (x) (x x)) , in CL braucht man wahrscheinlich noch ein funcall . Das könnte man sicher sinnvoll verwenden, zB für den Y-Kombinator.
    🙂

    0
  • I

    Ich stelle die Frage mal anders:
    λxy.xy <=> [λx.(λy.yx) od. λx.(λy.xy)]

    0
  • ?

    Ishildur schrieb:

    Ich stelle die Frage mal anders:
    λxy.xy <=> [λx.(λy.yx) od. λx.(λy.xy)]

    Sowas wie λxy.xy ist (wie erwähnt) eine Erweiterung auf mehrere Parameter. Man kann das immer auch durch Currying machen (Schönfinkeln klingt besser), in dem die innere Funktion ein Argument nimmt und eine Funktion zurückgibt, die noch ein Argument nimmt und dann die Arbeit erledigt.

    Unter diesem Siegel ist λxy.(...) das gleiche wie λx.(λy.(...)), das gilt auch für deine Frage.

    Ich empfehle, neben Stift und Papier auch einen Computer zu verwenden. In Sprachen wie Haskell geht Currying von Haus aus, in den üblichen Lisp-Varianten könnte man die zusätzlichen Klammern mit einem Makro entfernen. Common Lisp ist btw nicht die beste Wahl wenn's um den Lambda-Kalkül geht, weil es verschiedene Namensräume für Funktionen und Variablen hat (und sonst auch noch einige).

    Weiterführend ist auch lustig:
    http://www.madore.org/~david/programs/unlambda/
    🙂

    0
  • I

    Ja das habe ich schon verstanden, aber welches Symbol ist denn nun an welchen Parameter gebunden?

    0
  • ?

    Achso. y ist üblicherweise der zweite, x der erste. Aber das ist reine Konvention, man kann es auch umgekehrt machen.
    🙂

    0
  • K

    Mich wuerde mal interessieren, wo du diese Beispiele her hast.

    0
  • P

    Hier mal eine humorvolle Darstellung, die mir gut geholfen hatte:
    http://www.soton.ac.uk/~doctom/teaching/lambda/lambda.pdf

    0
Anmelden zum Antworten