Lambda-Kalkül schien nicht abstrakt zu sein. Und ich kann den Sinn nicht erkennen

18

Die zugrunde liegende Frage:

Was macht die Lambda-Rechnung für uns, was wir mit den in der Mittelschulalgebra allgemein erlernten Grundfunktionseigenschaften und der Notation nicht anfangen können?

Was bedeutet abstrakt im Zusammenhang mit der Lambda-Rechnung? Mein Verständnis des Wortes abstrakt ist etwas, das von der Maschinerie, der konzeptuellen Zusammenfassung eines Konzepts, getrennt ist.

Lambda-Funktionen verhindern jedoch eine bestimmte Abstraktionsebene, indem sie auf Funktionsnamen verzichten. Beispielsweise:

f(x) = x + 2
h(x, y) = x + 5 y

Aber auch ohne die Maschinerie dieser Funktionen zu definieren, können wir leicht über ihre Zusammensetzung sprechen. Beispielsweise:

1. h(x, y) . f(x) . f(x) . h(x, y) or 
2. h . f . f . h

Wir können die Argumente einbeziehen, wenn wir wollen, oder wir können vollständig abstrahieren, um einen Überblick darüber zu geben, was passiert. Und wir können sie schnell auf eine einzige Funktion reduzieren. Schauen wir uns Komposition 2 an. Ich kann Schüler-Detailebenen haben, mit denen ich je nach Schwerpunkt schreiben kann:

g = h . f . f . h
g(x, y) = h(x, y) . f(x) . f(x) . h(x, y)
g(x, y) = h . f . f . h = x + 10 y + 4

Lassen Sie uns das Obige mit Lambda-Kalkül durchführen oder zumindest die Funktionen definieren. Ich bin mir nicht sicher, ob dies richtig ist, aber ich glaube, dass der erste und der zweite Ausdruck um 2 erhöht werden.

(λuv.u(u(uv)))(λwyx.y(wyx))x

Und mit 5y multiplizieren.

(λz.y(5z))

Anstatt abstrakt zu sein, scheint dies in die Maschinerie dessen zu geraten, was es bedeutet, zu addieren, zu multiplizieren usw. Abstraktion bedeutet in meinen Augen eher eine höhere Ebene als eine niedrigere Ebene.

Außerdem kämpfe ich darum, warum Lambda-Kalkül überhaupt eine Sache ist. Was ist der Vorteil von

(λuv.u(u(uv)))(λwyx.y(wyx))x

Über

h(x) = x + 5 y

oder eine kombinierte Notation

Hxy.x+5y

oder sogar Haskells Notation

h x y = x + 5 * y

Wiederum, was macht Lambda-Kalkül für uns, was wir mit den Eigenschaften und der Notation der f (x) -Stil-Funktion, mit denen viele vertraut sind, nicht tun können.

JDG
quelle
9
Es ist lustig, dass Sie ein Beispiel von Haskell geben, da Haskell auf der Lambda-Rechnung basiert. Bei der Lambda-Rechnung geht es nicht um eine bestimmte Notation. Es ist ein Rechenmodell, das Turing-Maschinen entspricht, in denen "alles eine Funktion ist".
Yuval Filmus
2
Ja, mir wurde gesagt, dass es auf Lambda-Kalkül basiert. Die Frage, die ich noch auf eine für mich sinnvolle Weise beantworten muss, ist, warum haskell auf Lambda-Kalkül basiert und nicht auf gerechtem. . . die grundlegenden Eigenschaften von Funktionen, die ich in der Grundschule gelernt habe. Das ist wirklich der Kern dieser ganzen Frage.
JDG
6
Kommt nicht "kein Zweck sofort in den Sinn" fast die Definition von "abstrakt"? :-)
David Richerby
1
Ich würde nicht sagen, dass es abwertend ist. Diese Behandlung von Funktionen ist durch Kalkül brauchbar. Aber ich kann sehen, wie eine Kennzeichnung als Mittelschule so interpretiert werden kann. Ich werde es anpassen.
JDG
6
Ich bezweifle, dass Sie tatsächlich eine formale Definition der "Algebra-Funktionsnotation der Mittelschule" haben. Wenn Sie eine Definition für solche Funktionen haben, ist dies wahrscheinlich die Mengenlehre, die keine rechnerische Bedeutung hat. Ein Teil des Lambda-Kalküls besteht darin, eine solche Notation nach ihren eigenen Begriffen zu verstehen und, wie ich sage, von bestimmten Anwendungen wie Polynomfunktionen oder Kalkül abstrahiert zu werden.
Derek Elkins verließ SE

Antworten:

24

Es gibt viele Gründe, warum die Lambda-Rechnung so wichtig ist.

Ein sehr wichtiger Grund ist, dass die Lambda-Berechnung ein Berechnungsmodell ermöglicht, in dem berechenbare Funktionen erstklassige Bürger sind.

Funktionen höherer Ordnung kann man in der Sprache der Mittelschulalgebra nicht ausdrücken .

Nehmen Sie als Beispiel den Lambda-Ausdruck

λf.λg.λx.f(g(x))

Dieser einfache Ausdruck zeigt uns, dass im Lambda-Kalkül die Funktionszusammensetzung selbst eine Funktion ist. In der Mittelschulalgebra ist dies nicht leicht auszudrücken.

Im Lambda-Kalkül ist es sehr einfach auszudrücken, dass eine Funktion als Ergebnis eine Funktion zurückgibt.

Hier ist ein kleines Beispiel. Der Ausdruck (wobei ich hier einen angewandten Lambda-Kalkül mit Additions- und Integer-Konstanten annehme)

(λf.λg.λx.f((g(x)))(λx.x+2)

reduziert sich auf

λg.λx.g(x)+2

Beachten Sie auch, dass im Lambda-Kalkül Funktionen Ausdrücke und keine Definitionen der Form . Dies befreit uns von der Notwendigkeit, Funktionen zu benennen und zwischen einer syntaktischen Kategorie von Ausdrücken und einer syntaktischen Kategorie von Definitionen zu unterscheiden.f(x)=e

Auch wenn es unmöglich (oder nur notativ umständlich) wird, Funktionen höherer Ordnung auszudrücken, wird man Probleme haben, Ausdrücken Typen zuzuweisen.

Die Funktionszusammensetzung hat den polymorphen Typ

α.β.γ.(βγ)((αβ)γ)

im Hindley-Milner-Typ-System.

Ein sehr starkes Verkaufsargument für den Lambda-Kalkül ist der Begriff des typisierten Lambda-Kalküls . Die verschiedenen Typsysteme für funktionale Programmiersprachen wie Haskell und die ML-Familie basieren auf Typsystemen für Lambda-Kalküle, und diese Typsysteme bieten starke Garantien in Form von mathematischen Theoremen:

Wenn ein Programm gut typisiert ist und sich auf den Rest reduziert , dann ist auch gut typisiert.e e ' e 'eeee

Und wenn gut getippt ist, zeigt keine bestimmten Fehler.eee

Besonders hervorzuheben sind die Nachweise als Programmkorrespondenz . Der Curry-Howard-Isomorphismus (siehe zB https://www.rocq.inria.fr/semdoc/Presentations/20150217_PierreMariePedrot.pdf ) zeigt, dass es eine sehr genaue Entsprechung zwischen der einfach typisierten Lambda-Rechnung und der intuitionistischen Aussagenlogik gibt: Zu jeder Art entspricht einer logischen Formel . Ein Proof von entspricht einem Lambda-Term vom Typ , und eine Beta-Reduktion dieses Terms entspricht einer Schnitteliminierung im Proof.ϕ T ϕ T TTϕTϕTT

Ich fordere diejenigen, die glauben, dass die Mittelschulalgebra eine gute Alternative zur Lambda-Rechnung ist, auf, einen Bericht über die polymorph getypte Mittelschulalgebra höherer Ordnung zusammen mit einem entsprechenden Begriff des Curry-Howard-Isomorphismus zu entwickeln. Wenn Sie sogar einen interaktiven Proofassistenten auf der Grundlage der Mittelschulalgebra ausarbeiten können, der es uns ermöglicht, die vielen Theoreme zu beweisen, die unter Verwendung von Beweisassistenten auf Lambda-Basis wie Coq und Isabelle formalisiert wurden, ist dies sogar noch besser. Ich würde dann anfangen, Mittelschulalgebra zu verwenden, und so würden sicher viele andere mit mir.

Hans Hüttel
quelle
Das ist eine großartige Erklärung. Es ist hilfreich zu hören, dass Funktionen höherer Ordnung (wie die Komposition) und die Eingabe im Lambda-Kalkül besser dargestellt werden. Dies ist sogar ermutigend, um Beweise und nachweisbaren Code zu ermöglichen. Ich sehe nicht die Konsequenzen vieler Ihrer Erwähnungen und warum die traditionelle Notation unangemessen ist (z. B. dass keine separate Definitionssyntax f (x) = e benötigt wird), aber es ist hilfreich, dass Sie einige dieser Gründe und genannt haben Es gibt einen Eindruck davon, welche Bereiche durch die Lambda-Berechnung verbessert werden.
JDG
Man kann natürlich lokale Definitionen der Form aber diese können bereits in der Syntax des Lambda - Kalkül ausgedrückt werden . Der Lambda-Kalkül erlaubt es uns, Funktionen auszudrücken, ohne sie benennen zu müssen, so wie man (in der Mittelschulalgebra!) Von der Zahl sprechen kann, ohne sie durch eine Variable benennen zu müssen. letx=eine 4(λx.e)e4
Hans Hüttel
5

Wenn Funktionen zum ersten Mal für Jugendliche beschrieben werden, werden sie im Wesentlichen mit Diagrammen (Plots) oder vielleicht mit Formeln identifiziert; Auf diese Weise wurden Funktionen historisch verstanden, bevor formalistische Trends in der Mathematik aufkamen. Heutzutage sind Funktionen, wie sie in der ersten Jahresrechnung gelehrt werden, echte Funktionen, dh Funktionen von bis .RRR

Die Funktionen in der Lambda-Rechnung sind viel allgemeiner. Die genaue Definition hängt davon ab, ob Ihr Lambda-Kalkül typisiert oder nicht typisiert ist. In der reinen untypisierten Lambda-Rechnung ist alles eine Funktion. Dies ist viel allgemeiner als die eigentlichen Funktionen des Kalküls.

Sogar prozedurale Sprachen verwenden manchmal Ideen aus der Lambda-Rechnung. Die Sortierfunktion in C akzeptiert als Parameter eine Vergleichsfunktion , mit der Elemente verglichen werden. Die Lambda-Rechnung geht noch viel weiter - Funktionen akzeptieren Funktionen nicht nur als Eingaben, sondern können sie auch ausgeben.

Die Lambda-Rechnung ist ein Berechnungsmodell, das der Leistung von Turing-Maschinen entspricht. Es ist ein System für sich. In der reinen Lambda-Rechnung gibt es keine "5" oder "+" als Grundbegriffe - sie können innerhalb der Rechnung definiert werden, genau wie "5" und "+" keine Grundbegriffe der Mengenlehre sind. (Praktische Programmiersprachen implementieren natürliche Zahlen aus Gründen der Effizienz.)

Ich vermute, einer der Gründe, warum Sie von Lambda nicht beeindruckt sind, ist, dass seine Ideen den Programmierdiskurs so durchdrungen haben, dass er nicht mehr innovativ aussieht.

Yuval Filmus
quelle
"Ich vermute, einer der Gründe, warum Sie nicht von Lambda-Kalkül beeindruckt sind." Darin liegt die Frage, die ich stelle: Was macht Lambda-Kalkül für uns? Mit anderen Worten, wenn wir keinen Lambda-Kalkül verwenden, was passiert dann? Was gewinnen wir, wenn wir Lambda-Kalkül verwenden? Wenn die Menschen zum ersten Mal an Lambda-Kalkül dachten, was wäre, wenn Funktionen selbst Funktionen erzeugen könnten, dann ist das beeindruckend? Zu meinen ersten Python-Programmen gehörte Text, der Funktionen enthielt, die ich später auswertete, ähnlich wie das Delegieren der Aufgabe der Entscheidungsfindung an eine andere Person. Scheint offensichtlich?
JDG
das war, bevor ich viel von irgendetwas wusste. Ich dachte nur, dass das wiederholte Schreiben von Code ärgerlich ist und dass die Programmierung mir dabei helfen sollte, automatisch Funktionen zu generieren, einschließlich der Funktionen selbst.
JDG
2
Python unterstützt die funktionale Programmierung. Die ersten Programmiersprachen haben es nicht getan. Wenn Sie in FORTRAN programmiert hätten, hätten Sie keine Programme mit Text erstellt, der Funktionen enthält, die Sie später auswerteten. Ohne es zu bemerken, haben Sie die Möglichkeiten genutzt, die Ideen aus der Lambda-Rechnung bieten.
Yuval Filmus
2
Eval entstand in LISP , das stark vom Lambda-Kalkül beeinflusst wurde. So etwas ist in FORTRAN, C, COBOL und vielen anderen Programmiersprachen nicht möglich.
Yuval Filmus
Ja, Python unterstützt funktionales Programmieren --- aber ich bin nicht sicher, ob es sich um eval () handelt, das von λCalc inspiriert wurde --- Sie können λCalc nicht denken: Ich möchte automatisch Code generieren, den ich später auswerten kann. Das ist, als würde man sagen, dass λCalc denken muss: "Ich werde Miranda sagen, dass sie ihr bestes Urteil darüber treffen soll, wie sie ihre Abteilung führen soll." Sie brauchen λCalc nicht, um über das Delegieren übergeordneter Aufgaben nachzudenken. Wenn Sie über das Zeichnen von Inspirationen aus λCalc sprechen möchten, ist es sinnvoller, auf Lambda-Funktionen, Verständnis usw. zu verweisen
JDG,
4

Eine der grundlegenden Ambiguitäten der allgemeinen mathematischen Notation ist, dass manchmal verwendet wird, um eine Zahl zu bezeichnen (das Quadrat der Zahl ), und manchmal verwendet wird, um eine Funktion zu bezeichnen (die Funktion, die das Quadrat ihrer zurückgibt Streit). x x 2x2xx2

Lambda-Kalkül beseitigt diese Mehrdeutigkeit; Sie können schreiben , um auf die Funktion zu verweisen, was es eindeutig macht, dass auf eine Zahl verweist, wie es sollte.x 2λx.x2x2

Ja, Sie können den Fluss eines Arguments oder einer Berechnung unterbrechen, indem Sie sagen "Jetzt definiere durch " und dann , aber das wird schnell umständlich. Mit der Lambda-Abstraktion können Sie dies inline tun, ohne eine Unterbrechung vorzunehmen.f ( x ) = x 2 fff(x)=x2f

Die Verwendung von Lambda-Ausdrücken in Programmiersprachen hat einen ähnlichen Vorteil. Sie können schreiben, was die Funktion genau dort tut, wo sie benötigt wird, anstatt an anderer Stelle in Ihrem Programm eine ganz neue Funktion definieren zu müssen.

Sie können sogar die in der Mathematik implizite Lambda-Abstraktion sehen; ZB werden die Studenten der Analysis nur in Ableitungen von Funktionen unterrichtet. Um die Leibniz-Notation mit Ableitungen von Funktionen in Einklang zu bringen , können Sie so interpretieren, dass sie implizit eine Lambda-Abstraktion durchführen auf , um es als Funktion zu interpretieren. Sie sind mehr oder weniger gezwungen, dies zu tun, wenn Sie die im ersten Absatz beschriebene Mehrdeutigkeit nicht haben möchten.dddxx2 x2ddxx2


Außerdem fühlen sich Menschen mit funktionsbewerteten Funktionen in traditioneller Notation oft unwohl. zB ist die übliche Abbildung , die einen endlichdimensionalen Vektorraum mit seinem doppelten Dual identifiziert, durch definiertθ:VV

θ(v)(f)=f(v)

Viele Menschen empfinden diese doppelte Bewertungsnotation als verwirrend und / oder beunruhigend sowie die rekursive Verwendung der punktweisen Definition einer Funktion. Die Lambda-Abstraktionsversion

θ=λv.λf.f(v)

hat dieses Problem nicht.


Schließlich gibt es einen Satz des abstrakten Unsinns, der besagt, dass "einfach typisierte Lambda-Rechnung" im Grunde genommen dasselbe ist wie "kartesische geschlossene Kategorie". Wenn Sie also jemals in einer kartesischen geschlossenen Kategorie rechnen wollen, ist es wahrscheinlich eine gute Idee, ihn zu verwenden tippte einfach Lambda-Kalkül, um dies zu tun.


quelle
Ich komme auf diese Frage zurück und finde diese Antwort großartig. Vielen Dank. Die Antworten hier sind im Allgemeinen sehr interessant.
JDG
4

Ich sage ganz vorne, ich bin kein Experte für dieses Thema, aber ich habe ein bisschen Zeit damit verbracht, es zu studieren, und eines der faszinierendsten Dinge für mich in jedem Thema ist die Geschichte dahinter. Wenn ich ein bisschen die Geschichte hinter der Lambda-Rechnung verstehe, kann ich erklären, warum sie nützlich ist.

Die kurze Zusammenfassung ist, dass in den frühen 1900er Jahren, nachdem die Mengenlehre zu beginnen begann und die Mathematik auf der Grundlage von Mengen neu gedacht wurde, einige Mathematiker bemerkten, dass eine Mengenlehre-Definition es Ihnen erlaubt, zu behaupten, dass eine bestimmte Struktur existiert, aber nicht sagt, wie um es zu konstruieren und zu berechnen. Mengen-theoretische Definitionen sind also nicht konstruktiv . Mathematiker begannen sich zu fragen, ob es einen Weg gibt, konstruktive Definitionen zu entwickeln , die über den Nachweis hinausgehen, dass etwas ist, und stattdessen beweisen, wie es ist .

Aus Wikipedia :

In der Mathematik ist ein konstruktiver Beweis eine Beweismethode, die die Existenz eines mathematischen Objekts durch Erstellen oder Bereitstellen einer Methode zum Erstellen des Objekts demonstriert. Dies steht im Gegensatz zu einem nicht konstruktiven Beweis (auch als Existenzbeweis oder reines Existenztheorem bezeichnet), der die Existenz einer bestimmten Art von Objekt beweist, ohne ein Beispiel anzugeben.

Turing entwickelte die Turing-Automaten, um die Frage zu beantworten, und Church entwickelte die Lambda-Rechnung, um die Frage zu beantworten. Kleene entwickelte auch eine Methode mit dem Kleene Star , die in reguläre Ausdrücke übernommen wurde, und es gab jemanden (den man nicht ohne weiteres zurückrufen kann), der noch eine andere Methode entwickelte. All dies wurde entwickelt, um ein mathematisches System aufzubauen, das von Anfang an konstruktive Definitionen zulässt.

Dann wurde gezeigt, dass Lambda-Kalkül und die Turing-Maschine jede berechenbare Funktion darstellen können und somit äquivalent sind.

Theoretisch kann jede mathematische Funktion oder jedes mathematische Konzept in Form einer Lambda-Rechnung kodiert und berechnet werden. Dies bedeutet, dass die Lambda-Berechnung eine völlig separate, wenn auch offensichtlich äußerst mühsame Grundlage für die Mathematik sein kann.

Lambda-Kalkül ist nicht "nützlich" in dem Sinne, dass Sie keinen Code damit schreiben werden, aber es bildet die Grundlage für die Denotationssemantik, die zur Beschreibung von Programmen und ihren dynamischen Effekten verwendet wird. Dies wird in Diskussionen über Programmkorrektheit und semantische Bedeutung verwendet. Es hat natürlich auch die Entwicklung funktionaler Programmiersprachen stark beeinflusst, die ihr gesamtes Ausführungskonzept aus der Lambda-Rechnung beziehen.

Ich hoffe, das hilft.

Bearbeiten, um hinzuzufügen: Ich wurde gerade auf dieses Papier verwiesen, das die Beziehung zwischen Topologie, Lambda-Kalkül und Physik zeigt. Beim kurzen Überfliegen bin ich auf diese fantastische Aussage gestoßen:

Während eine Turing-Maschine als idealisiertes, vereinfachtes Modell der Computerhardware angesehen werden kann , ist die Lambda-Berechnung eher ein einfaches Modell der Software . ... Der Lambda-Kalkül beschreibt poetisch gesehen ein Universum, in dem alles ein Programm und alles Daten sind: Programme sind Daten .

Der Punkt ist, dass die Lambda-Rechnung ein idealisiertes Modell der Software-Berechnung ist und als solches nicht an eine bestimmte Implementierung in irgendeiner Programmiersprache gebunden ist. Es modelliert die reine Berechnung .

Dave
quelle
Mehr zur Geschichte: Kurze Geschichte der λ-Rechnung in der Stanford Encyclopedia of Philosophy. Sie haben mehr Einträge, als man in einem Leben verarbeiten kann.
David Tonhofer
3

Wie Yuval in den Kommentaren betonte, basiert Haskell auf dem Kalkül. Ein weiterer Grund, warum die Lambda-Rechnung so wichtig ist, ist der Church-Rosser-Satz , der die Existenz einer faulen Bewertung rechtfertigt. (Welches ist eines der vielen coolen Features von Haskell?)λ

Aristu
quelle
3

Lambda-Kalkül war nicht als Programmiersprache konzipiert. Tatsächlich wurde es in den 1930er Jahren erstellt, Jahrzehnte bevor wir überhaupt programmierbare Computer hatten. Es wurde vielmehr als formales Modell für das Studium der Berechnung selbst geschaffen. Wenn Sie enttäuscht sind, wie einfach es ist, Code oder mathematische Funktionen auszudrücken, dann ist das nicht das, wofür es ist.

Andrew
quelle
1
"Jahrzehnte bevor wir überhaupt programmierbare Computer hatten" - falsch. Programmierbare Computer gab es schon früher (wenn nicht sogar universelle) und die ersten universellen Computer wurden in den 1930er Jahren gebaut.
Raphael
-2

Lambda-Kalkül existiert, so dass anonyme (alias Lambda) Funktionen erstellt werden können. Wenn Sie die Funktionsnamen nicht weglassen, kann der Namespace überfüllt sein und die verfügbaren Funktionsnamen können knapp werden. Dies ist besonders wichtig, wenn es sich um sogenannte "Funktionen höherer Ordnung" handelt, die aus offensichtlichen Gründen Funktionen (oder Funktionszeiger) zurückgeben.

Im Wesentlichen entsprechen Lambda-Funktionen Variablen mit lokalem Gültigkeitsbereich. Funktionale Programmierung ohne Lambda-Funktionen ist analog zur prozeduralen Programmierung ohne lokale Variablen, dh eine schreckliche Idee.

"Warum Lambda-Kalkül überhaupt eine Sache ist" Mathematiker lieben Redundanz. Lambda-Kalkül wird in der Mathematik selten verwendet, da die Notation, wie Sie festgestellt haben, nicht sehr nützlich ist.

"Wenn Sie sogar einen interaktiven Proofassistenten auf der Grundlage der Mittelschulalgebra ausarbeiten könnten, der es uns ermöglicht, die vielen Sätze zu beweisen, die mit Proofassistenten auf Lambda-Basis wie Coq und Isabelle formalisiert wurden, wäre das noch besser. Ich würde Fangen Sie dann an, die Mittelschulalgebra zu verwenden, und ich bin sicher, dass viele andere mit mir gehen würden. " Hast du von Metamath gehört? Da keine Lambda-Rechnung beteiligt ist, können viele der Coq / Isabelle-Theoreme bewiesen werden

sn
quelle
Was bietet diese Antwort, abgesehen von einigen Meinungen?
Raphael
@ Raffael Fehlinformationen. Der größte Teil dieser Antwort ergibt nicht einmal einen Sinn. An Namen mangelt es nicht. "Lambda-Funktionen" entsprechen nicht Variablen mit lokalem Gültigkeitsbereich. das ergibt nicht einmal einen sinn. Ich gehe davon aus, dass dies gemeint ist let, aber während letes mit anonymen Funktionen codiert werden kann, können Sie eindeutig nicht den anderen Weg gehen. Funktionale Programmierung ist nicht erforderlich „Lambda - Funktionen“, zB Backus' FP oder Sisal .
Derek Elkins verließ SE
meistens wollte ich einen kommentar zu hans 'antwort schreiben, hatte aber nicht genug karma. Also habe ich beschlossen, den Kommentar in eine vollständige Antwort
umzuwandeln