3. Lambda Kalkül

Lambda Kalkül

  • I

    Ja davon gehe ich aus, aber eben, wie man es dreht und wendet, bei all diesen abstrusen Lambda Termen sehe ich einfach, dass am Ende noch Funktionen übrig bleiben, die nicht definiert sind... weil sie offenbar mit dem Lambda Kalkül schlicht nicht definierbar sind. Da heissts dann einfach "f" und lässt völlig offen, was f genau macht resp. was f für eine Abbildung ist => Weil man es schlicht nicht definieren kann?

    0
  • ?

    Ishildur schrieb:

    weil sie offenbar mit dem Lambda Kalkül schlicht nicht definierbar sind.

    Ich muss leider mit dir auf die Erklärung warten. Aber dass sie nicht definierbar sind, muss falsch sein; Beweis:

    In irgendeinem fühen Lisp-Paper werden Zahlen in unärer Weise in Lisp dargestellt, also zB die Zahl 3 als Liste mit Länge 3. Nachdem man die Cons-Zellen aus Lisp aber auf Funktionen abbilden kann (Beispiele in SICP und Wikipedia), müssen diese Dinge irgendwie im Lambda-Kalkül machbar sein.

    Abgesehen davon werd ich mal bis auf was Konkreteres abwarten.
    🙂

    0
  • I

    @µngbd
    Hehe, ja ich warte auch gespannt... 😉

    0
  • C

    Ishildur schrieb:

    Ja davon gehe ich aus, aber eben, wie man es dreht und wendet, bei all diesen abstrusen Lambda Termen sehe ich einfach, dass am Ende noch Funktionen übrig bleiben, die nicht definiert sind... weil sie offenbar mit dem Lambda Kalkül schlicht nicht definierbar sind. Da heissts dann einfach "f" und lässt völlig offen, was f genau macht resp. was f für eine Abbildung ist => Weil man es schlicht nicht definieren kann?

    Im Lambda-Kalkül muss man Funktionen nicht unbedingt aufrufen, um darüber zu reden. Das Endergebnis, die Zahl 3 in deinem Fall, ist die Funktion (λfx.f(f(f(x))).

    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. Einfaches Beispiel in C++ wäre ein Header mit den beiden Deklarationen:

    int f(int x);
int g(int x);

    Auch wenn du weißt, dass f und g beide keine Seiteneffekte haben (d.h. kein I/O, keine globalen oder statischen Variablen, etc.), kannst du innerhalb einer cpp-Datei mit Standard-C++ nicht entscheiden, ob f die gleiche Funktion wie g ist. Denn "Gleichheit" bei Funktionen ist meistens definiert als: f(x) = g(x) für alle x. Nur wer garantiert, dass f(x) und g(x) für alle Werte von x terminieren?

    Das Problem der nicht-terminierenden Funktionen hast du auch schon im lambda-Kalkül. Versuch z.B. mal den Term (λx.(x x))(λx.(x x)) auszuwerten.

    Oft betrachtet man den Lambda-Kalkül als Hilfsmittel für andere Dinge. Dann führt man wirklich Funktionen ein, die innerhalb des reinen Lambda-Kalküls nicht (nützlich) definierbar sind, wie zum Beispiel "if" oder eben primitive Datentypen wie "int".

    Sobald du jedenfalls die Möglichkeit nicht-terminierender Funktionen hast, kannst du innerhalb einer Programmiersprache Funktionen nicht mehr auf Gleichheit testen. In Lisp zum Beispiel wirst du keine Möglichkeit finden, zwei Funktionen auf Gleichheit zu testen, auch wenn beide frei von Seiteneffekten sind.

    Im reinen Lambda-Kalkül betrachtet man aber dennoch (λfx.f(f(f(x))) als Darstellung der natürlichen Zahl 3. Diesen lambda-Term muss man nicht anwenden, um 3 zu bekommen, dieser lambda-Term ist schon die Darstellung der Zahl 3.
    Wenn der Lambda-Kalkül aber nur ein Hilfsmittel in einer Programmiersprache ist, wird man diesen lambda-Term wahrscheinlich auf "successor" und "0" anwenden wollen, um eine nützlichere Darstellung der Zahl 3 zu bekommen.

    edit: Bisschen was durcheinandergebracht.

    (Nur der Vollständigkeit halber: Was ich oben "mathematisch" genannt habe, heißt normalerweise "denotationale Semantik".)

    0
  • 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
Anmelden zum Antworten