Lambda-Kalkül außerhalb der funktionalen Programmierung?

21

Ich bin ein Universitätsstudent und wir studieren derzeit Lambda Calculus. Es fällt mir jedoch immer noch schwer, genau zu verstehen, warum dies für mich nützlich ist. Mir ist klar, dass es nützlich sein kann, wenn Sie eine Menge funktionaler Programmierung durchführen. Ich bin jedoch der Meinung, dass dies nicht wirklich für das Erlernen funktionaler Programmierung erforderlich ist. Was denken Sie?

Zweitens, gibt es eine Verwendung für Lambda-Kalkül im Bereich der Informatik, jedoch außerhalb der funktionalen Programmiersprachen?

Jacob
quelle

Antworten:

15

Der Lambda-Kalkül ist grundlegend in der Logik, Kategorietheorie, Typentheorie, formalen Verifikation, ... Grundsätzlich alles, was mit Programmiersprachsemantik und formaler Logik zu tun hat. Es ist ein so grundlegender Formalismus, dass die Menschen, die in diesen Bereichen arbeiten, den Nutzen davon nicht einmal in Frage stellen.

Ich denke, dass es für das Verständnis der funktionalen Programmierung äußerst nützlich ist, weil es Ihnen die Essenz der funktionalen Programmierung gibt. Funktionen, Anwendung, Substitution. Darauf aufbauend können Sie Ihre Denkfähigkeiten in Bezug auf funktionale Programme und deren Transformationen erweitern. Funktionen höherer Ordnung sind ein Kinderspiel.

Sicher, Sie könnten funktionale Programmierung ohne den Lambda-Kalkül lernen, aber ohne ihn würden Sie funktionale Programmierung niemals wirklich verstehen.

Dave Clarke
quelle
Vielen Dank für Ihre Antwort, Dave. Ich denke, formale Verifizierung ist der beste Grund, warum Lambda-Kalkül für mich nützlich ist, und komischerweise werde ich im nächsten Semester einen Kurs über formale Verifizierung machen. Würden Sie Lambda-Kalkül auch verwenden, um eine formale Überprüfung einer Software durchzuführen, die in einer beliebigen Sprache geschrieben wurde, z. B. einer imperativen oder objektorientierten?
Jacob
1
Sie können den Lambda-Kalkül nicht direkt bei der formalen Überprüfung verwenden, er wird jedoch in den Grundlagen der formalen Überprüfung angezeigt. Das Schreiben von Spezifikationen umfasst häufig das Schreiben in einer funktionalen Sprache, auch für Imperativ- / OO-Code.
Dave Clarke
Okay, das ist interessant, danke, jetzt habe ich ein bisschen mehr Grund, das zu studieren. Wissen Sie, ob Lambda-Kalkül verwendet wird, um nicht funktionierende Sprachen (auf niedrigeren Ebenen) zu entwerfen?
Jacob
1
ALGOL. Scala. Letztendlich ist Ihre Frage schwer zu beantworten. Die Lambda-Rechnung ist für (die meisten) Sprachgestalter ein Teil des alltäglichen Wissens und beeinflusst daher das Sprachdesign, auch wenn sie nicht explizit verwendet wird. Betrachten Sie Blöcke in Smalltalk oder Ruby, anonyme Klassen in Java. Dies sind Abschlüsse, die eng mit Funktionen höherer Ordnung in der Lambda-Rechnung verbunden sind.
Dave Clarke
Okay, vielen Dank, Dave, das wird sehr geschätzt.
Jacob
17

Sie fordern eine Bewerbung außerhalb der Informatik und Logik. Das ist leicht zu finden, zum Beispiel in der algebraischen Topologie ist es zweckmäßig, eine kartesische geschlossene Kategorie von Räumen zu haben, siehe die bequeme Kategorie von topologischen Räumen in nLab. Die formale Sprache, die den kartesischen geschlossenen Kategorien entspricht, ist genau der Kalkulus. Lassen Sie mich anhand eines sehr einfachen Beispiels veranschaulichen, wie nützlich dies ist.λ

Stellen Sie sich zunächst als Aufwärmübung vor, jemand fragt Sie, ob die durch definierte Funktion ist differenzierbar. Das muss man eigentlich nicht beweisen, man stellt nur fest, dass es sich um eine Zusammensetzung differenzierbarer Funktionen handelt, also differenzierbar. Mit anderen Worten, Sie haben eine einfache Schlussfolgerung basierend auf der Form der Definition.f:RRf(x)=x2ex+log(1+x2)

Nun zum wirklichen Beispiel. Angenommen, jemand fragt Sie, ob die Funktion definiert ist durch ist stetig kann sofort mit "yes" antworten, da die Funktion mit dem -calculus definiert wird und von kontinuierlichen Maps , , usw. ausgeht .f:RRλ max sin

f(x)=(λf:C(R).xxf(1+t2)dt)(λy:R.max(x,sin(y+3))
λmaxsin

Verschiedene Erweiterungen des Kalküls ermöglichen es, dasselbe in anderen Bereichen zu tun. Da ein glatter Topos beispielsweise eine kartesisch geschlossene Kategorie ist, wird jede Karte, die mit dem Kalkül definiert wird, ausgehend von Ableitungen und der Ringstruktur der Reals (und Sie können die Exponentialfunktion einwerfen, wenn Sie dies wünschen) automatisch erstellt glatt. (Tatsächlich ist der Hauptschub des glatten Topos die Existenz von nullpotenten Infinitesimalen, mit denen man bedeutungsvoll Dinge wie "Wir zerlegen eine Scheibe in unendlich dünne gleichschenklige Dreiecke" sagen kann.)λλλ

Andrej Bauer
quelle
1
Vielen Dank für Ihre ausführliche Antwort. Eigentlich habe ich versucht, eine Verwendung für die Lambda-Berechnung in der Informatik zu finden, aber außerhalb der funktionalen Programmierung, entschuldige mich, wenn dies nicht klar war. Ich habe die Frage geändert, um dies klarer auszudrücken.
Jacob
Schade, ich hätte eine ausführliche Antwort darauf geschrieben.
Andrej Bauer
Entschuldigung dafür. Fühlen Sie sich frei, Kommentare hinzuzufügen, wenn Sie zusätzliche Informationen hinzufügen möchten :)
Jacob
2
Ich denke, Daves Frage ist in Ordnung, ich habe nichts hinzuzufügen. Wenn Sie sehen möchten, welche aufregenden Dinge Sie mit dem -calculus tun können, können Sie vielleicht einen Blick auf die unmöglichen Funktionalitäten werfen. Aber als allgemeine Antwort ist Daves sehr gut. λ
Andrej Bauer
7

Eine Sichtweise auf -calculus ist das einfache und knappe Modell von Parametrierprogrammen. Sie parametrisieren Code in fast jeder Programmiersprache, die Funktionen, Prozeduren oder Methoden enthält, und in jeder Sprache, die Module enthält oder die es Ihnen ermöglicht, Typen zu parametrisieren. Die Parametrisierung ist eine Form der Wiederverwendung. Da -calculus so einfach ist, treten die Gemeinsamkeiten vieler Programmiersprachen, mit denen Sie Code parametrisieren können, besonders deutlich in den Vordergrund.λλλ

Es ist sicherlich möglich, ein sehr guter Programmierer zu sein, ohne etwas über -calculus zu wissen , aber Sie verpassen etwas Schönes, das auch sehr nützlich ist.λ

Martin Berger
quelle
5

Microsoft LINQ (Language INtegrated Query) übersetzt funktionale Programmierfunktionen in prozedurale Sprachen. Sie verwendet -calculus in großem Umfang und ganz direkt , um Abhängigkeiten zu entwirren und Teile des Ausdrucksbaums zu trennen, die an den Datenbankserver delegiert werden können. Dies ist eine äußerst praktische Anwendung mit hohem kommerziellen Wert.λ

Ich habe eine kleine kommerzielle Anwendung unter Verwendung einer funktionalen Sprache geschrieben und kann Ihnen versichern, dass sie für Wissenschaftler und Forscher zwar lohnenswert, aber kommerziell weniger nützlich sind als ihre prozeduralen Verwandten. Es ist wirklich eine Frage von Pferden für Kurse, und am praktischsten ist eine Sprache, die je nach Bedarf prozedural oder funktional sein kann. Infolgedessen werden Funktionen, die zur Unterstützung von LINQ (in C #) eingeführt wurden, wie z. B. -Expressions, außerhalb des Kontexts von Datenbankabfragen häufig verwendet.λ

Wenn Sie also endlich gezwungen sind, schlechte Dinge zu tun, weil Sie bezahlt werden möchten , ist -calculus möglicherweise nützlicher als erwartet, obwohl Sie mit ziemlicher Sicherheit keine funktionierende Sprache verwenden.λ

Peter Wone
quelle