Warum ist es wichtig, dass Funktionen in der Lambda-Rechnung anonym sind?

19

Ich habe mir den Vortrag von Jim Weirich mit dem Titel " Adventures in Functional Programming " angesehen. In dieser Vorlesung stellt er das Konzept der Y-Kombinatoren vor, die im Wesentlichen den Fixpunkt für Funktionen höherer Ordnung finden.

Eine der Beweggründe, wie er es erwähnt, ist, rekursive Funktionen mit Lambda-Kalkül ausdrücken zu können, damit die Theorie der Kirche (alles, was effektiv berechenbar ist, kann mit Lambda-Kalkül berechnet werden) erhalten bleibt.

Das Problem ist, dass eine Funktion sich nicht einfach so aufrufen kann, weil die Lambda-Rechnung keine benannten Funktionen zulässt, dh

n(x,y)=x+y

kann den Namen ' ' nicht tragen , er muss anonym definiert werden:n

(x,y)x+y

Warum ist es für die Lambda-Rechnung wichtig, Funktionen zu haben, die nicht benannt sind? Welches Prinzip wird verletzt, wenn es benannte Funktionen gibt? Oder habe ich gerade das Video von Jim falsch verstanden?

Rohan Prabhu
quelle
4
Das klingt überhaupt nicht wichtig. Sie können einer Variablen zuweisen und dann der Funktion einen Namen geben. n(x,t)x+yn
Yuval Filmus
@YuvalFilmus Ja, Sie können einen Namen an eine Funktion binden. Ich denke, die eigentliche Frage hier, das Rätsel, ist, warum (in der Lambda-Rechnung) sich eine Funktion nicht so nennen kann. Warum brauchen wir eine Technik wie den Y-Operator, um rekursive Funktionen auszuführen? Ich hoffe meine Antwort hilft weiter.
Jerry101
1
@ Jerry101 Der historische Grund für das Fehlen der Selbstanwendung ist, dass -calculus eine Grundlage für die Mathematik sein sollte und die Fähigkeit zur Selbstanwendung eine solche Grundlage sofort inkonsistent macht. Diese offensichtliche Unfähigkeit (von der wir jetzt wissen, dass sie umgangen werden kann) ist ein Konstruktionsmerkmal von -calculus. λλλ
Martin Berger
@ MartinBerger bitte mehr sagen. Inkonsistent aus dem Grund in meiner Antwort? Oder aus einem anderen Grund?
Jerry101
1
@ Jerry101 Inkonsistent in dem Sinne, dass man in einem solchen mathematischen Fundament 0 = 1 nachweisen kann. Nachdem Kleene und Rosser die Inkonsistenz des reinen, untypisierten Kalküls gezeigt hatten, wurde der einfach typisierte Kalkül als Alternative entwickelt, die es uns nicht erlaubt, Fixpunktkombinatoren wie zu definieren . Wenn Sie jedoch dem einfach eingegebenen -calculus eine Rekursion hinzufügen, wird dieser wiederum inkonsistent, da in jedem Typ ein nicht abschließendes Programm enthalten ist. λ Y λλλYλ
Martin Berger

Antworten:

24

Der Hauptsatz zu diesem Thema stammt von einem britischen Mathematiker aus dem Ende des 16. Jahrhunderts, William Shakespeare . Sein bekanntester Aufsatz zu diesem Thema trägt den Titel " Romeo und Julia " und wurde 1597 veröffentlicht, obwohl die Forschungsarbeiten einige Jahre zuvor durchgeführt wurden, inspiriert aber solche Vorläufer wie Arthur Brooke und William Painter.

Sein Hauptergebnis, angegeben in Akt II. Szene II ist der berühmte Satz :

Was ist in einem Namen? das, was wir eine Rose
nennen, würde bei jedem anderen Namen so süß riechen;

Dieser Satz kann intuitiv als "Namen tragen nicht zur Bedeutung bei" verstanden werden.

Der größte Teil der Arbeit ist einem Beispiel gewidmet, das den Satz ergänzt und zeigt, dass Namen, obwohl sie keine Bedeutung haben, die Ursache für endlose Probleme sind.

Wie Shakespeare betonte, können Namen ohne Änderung der Bedeutung geändert werden. Diese Operation wurde später von Alonzo Church und seinen Anhängern als -Umwandlung bezeichnet . Infolgedessen ist es nicht unbedingt einfach zu bestimmen, was mit einem Namen bezeichnet wird. Dies wirft eine Reihe von Fragen auf, z. B. die Entwicklung eines Umgebungskonzepts, in dem die Namensbedeutungszuordnung angegeben ist, und Regeln, um die aktuelle Umgebung zu ermitteln, wenn Sie versuchen, die mit einem Namen verknüpfte Bedeutung zu bestimmen. Dies verwirrte die Informatiker für eine Weile und führte zu technischen Schwierigkeiten wie dem berüchtigten Funarg-Problemα. In einigen populären Programmiersprachen sind Umgebungen nach wie vor ein Problem, aber es wird allgemein als physikalisch unsicher angesehen, genauer zu sein, fast so tödlich wie das Beispiel, das Shakespeare in seinem Aufsatz herausgearbeitet hat.

Diese Frage steht auch in engem Zusammenhang mit den Problemen, die in der formalen Sprachtheorie aufgeworfen werden, wenn Alphabete und formale Systeme bis zu einem Isomorphismus definiert werden müssen, um zu unterstreichen, dass die Symbole der Alphabete abstrakte Einheiten sind , unabhängig davon, wie sie sich als "materialisieren" Elemente aus einem Satz.

Dieses Hauptergebnis von Shakespeare zeigt auch, dass die Wissenschaft damals von Magie und Religion abwich, wo ein Wesen oder eine Bedeutung einen wahren Namen haben könnte .

Die Schlussfolgerung daraus ist, dass es für theoretische Arbeiten oft bequemer ist, sich nicht von Namen belasten zu lassen, auch wenn es sich für die praktische Arbeit und den Alltag einfacher anfühlt. Aber denken Sie daran, dass nicht jeder, der Mama heißt, Ihre Mutter ist.

Hinweis :
Das Problem wurde in jüngerer Zeit von der amerikanischen Logikerin Gertrude Stein aus dem 20. Jahrhundert angesprochen . Ihre Mathematikerkollegen überlegen sich jedoch immer noch die genauen technischen Implikationen ihres Hauptsatzes :

Rose ist eine Rose ist eine Rose ist eine Rose.

veröffentlicht 1913 in einer kurzen Mitteilung mit dem Titel "Heilige Emily".

babou
quelle
3
Zusätzlicher Hinweis: In den letzten Jahrzehnten wurde "rose" (in der Informatik) zumeist durch "foobar" (und Teile davon) als kanonisches Beispiel für einen Namen ersetzt, der so gut ist wie jeder andere. Diese Präferenz wurde anscheinend von amerikanischen Eisenbahningenieuren eingeführt.
FrankW
Kanonische Namen für häufig verwendete Konzepte sind jedoch wichtig für eine effiziente Kommunikation.
Raphael
1
@Raphael Einverstanden, aber ich würde das in die Kategorie Alltag einordnen. Und woher kennen wir die Grenzen dessen, was wirklich kanonisch ist? Trotzdem bin ich oft besorgt, wenn ich sehe, dass Schüler alle Begriffe, Notationen und Definitionen (oder sogar die Art und Weise, wie einige Sätze angegeben sind) für eine von Gott gegebene unveränderliche Wahrheit verwenden. Sogar hier in SE stellen die Schüler Fragen, ohne zu wissen, dass wir ihre Notationen oder die Definitionen, die sie im Unterricht verwenden, nicht kennen. Die Magie der wahren Namen stirbt nicht so leicht.
Babou
10

Ich möchte eine Meinung wagen, die sich von der von @babou und @YuvalFilmus unterscheidet: Es ist wichtig, dass der reine Kalkül anonyme Funktionen hat. Das Problem mit nur benannten Funktionen besteht darin, dass Sie im Voraus wissen müssen, wie viele Namen Sie benötigen. Aber im reinen Kalkül ist die Anzahl der verwendeten Funktionen nicht von vornherein festgelegt (denken Sie an die Rekursion). Sie verwenden also entweder (1) anonyme Funktionen oder (2) Sie gehen den Kalkül-Weg und geben sie an ein Kombinator für neue Namen ( in -calculus), der zur Laufzeit ein unerschöpfliches Angebot an neuen Namen liefert.λλπνx.Pπ

Der Grund, warum der reine Kalkül keinen expliziten Mechanismus für die Rekursion hat, ist, dass der reine Kalkül ursprünglich eine Grundlage der Mathematik von A. Church sein sollte, und die Rekursion macht eine solche Grundlage trivial unsund. So kam es zu einem Schock, als Stephen Kleene und JB Rosser entdeckten, dass reiner Kalk als Grundlage der Mathematik ungeeignet ist ( Kleene-Rosser-Paradoxon ). Haskell Curry analysierte das Kleene-Rosser-Paradoxon und erkannte, dass sein Wesen das ist, was wir heute als Y-Combinator kennen.λλλ

Hinzugefügt nach @ babous Kommentar: Es ist nichts Falsches daran, Funktionen benannt zu haben. Sie können dies folgendermaßen tun: ist eine Abkürzung für im Call-by-Value -calculus.letf=MinN(λf.N)Mλ

Martin Berger
quelle
1
Ich denke, das OP wollte die Fähigkeit, Funktionen zu benennen, nicht anonyme zu verbieten. Das heißt, ich würde denken, dass jede Anforderung von λ-Kalkül in Bezug auf die Notwendigkeit anonymer Funktionen auch in Sprachen wie Lisp / Scheme oder ML angezeigt wird. Im Fall von Lisp / Scheme sollte es die Meta-Zirkularität der Bewerter ermöglichen, nach Bedarf neue Namen zu erstellen, obwohl ich nicht sicher bin, ob ich dies in einem formalen System so möchte. Die Verwendung einer unbegrenzten Anzahl von Funktionen ist nicht unbedingt ein Problem, wenn die Rekursion die lokale Wiederverwendung bereits verwendeter Namen ermöglicht.
Babou
λλ
Sollte die letzte Zeile (Lambda f. N) M lauten?
Joe die Person
@JoethePerson Ja, gut gesehen. Fest. Vielen Dank.
Martin Berger
4

Ich glaube, die Idee ist, dass Namen nicht notwendig sind. Alles, was anscheinend Namen erfordert, kann als anonyme Funktion geschrieben werden.

Sie können sich den Lambda-Kalkül als Assemblersprache vorstellen. Jemand in einem Assembly-Vortrag könnte sagen: "In der Assemblersprache gibt es keine objektorientierten Vererbungsbäume." Sie könnten sich dann eine clevere Möglichkeit überlegen, Vererbungsbäume zu implementieren, aber das ist nicht der Punkt. Der Punkt ist, dass Vererbungsbäume nicht auf der grundlegendsten Ebene der Programmierung eines physischen Computers erforderlich sind.

In der Lambda-Rechnung ist der Punkt, dass Namen nicht erforderlich sind, um einen Algorithmus auf der grundlegendsten Ebene zu beschreiben.

Echt John Connor
quelle
4

Ich genieße die drei Antworten hier, insbesondere die Shakespearen-Analyse von @ babou, aber sie geben keinen Aufschluss darüber, was meiner Meinung nach das Wesentliche dieser Frage ist.

λ-calculus bindet Namen an Funktionen, wenn Sie eine Funktion auf eine Funktion anwenden. Das Problem ist nicht der Mangel an Namen.

"Das Problem ist, dass eine Funktion sich nicht einfach selbst aufrufen kann", indem sie auf ihren Namen verweist.

(In Pure Lisp liegt die Bindung name -> function nicht im Gültigkeitsbereich des Funktionskörpers. Damit sich eine Funktion nach ihrem Namen aufruft, muss sich die Funktion auf eine Umgebung beziehen, die sich auf die Funktion bezieht. Pure Lisp hat keine zyklische Datenstrukturen. Unreines Lisp tut dies, indem es die Umgebung mutiert, auf die sich die Funktion bezieht.)

Wie @MartinBerger hervorhob, war der historische Grund, warum sich eine Funktion im λ-Kalkül nicht beim Namen nennen lässt, der Versuch, Currys Paradoxon auszuschließen , wenn man versucht, den λ-Kalkül als Grundlage der Mathematik einschließlich der deduktiven Logik zu verwenden. Dies hat nicht funktioniert, da Techniken wie der Y-Kombinator eine Rekursion auch ohne Selbstreferenz ermöglichen.

Aus Wikipedia:

Wenn wir Funktion definieren r = (λ.x x x ⇒ y)dann r r = (r r ⇒ y).

Wenn r res wahr ist, dann yist es wahr. Wenn r rfalsch r r ⇒ yist, dann ist wahr, was ein Widerspruch ist. So yist es wahr und wie yes jede Aussage sein kann, kann jede Aussage als wahr erwiesen werden.

r rist eine nicht abschließende Berechnung. Als Logik r rwird ein Ausdruck für einen Wert betrachtet, der nicht existiert.

Jerry101
quelle
λ.x xxxxx
@RohanPrabhu λ.x x xübersetzt in Lisp als (lambda (x) (x x))und in JavaScript als function (x) {return x(x);}. x⇒ybedeutet x implies yetwa das Gleiche wie (NOT x) OR y. Siehe en.wikipedia.org/wiki/Lambda_calculus
Jerry101
Vielen Dank für die Beantwortung dieser peinlichen Anfängerfrage!
Rohan Prabhu