Ist Lambda Calculus rein syntaktisch?

Ich habe ein paar Wochen lang über den Lambda-Kalkül gelesen, aber ich habe noch nichts gesehen, das sich materiell von vorhandenen mathematischen Funktionen unterscheidet, und ich möchte wissen, ob es sich nur um eine Notationssache handelt oder ob es irgendwelche neuen gibt Eigenschaften oder Regeln, die von den Axiomen der Lambda-Rechnung erstellt wurden und nicht für jede mathematische Funktion gelten. So habe ich zum Beispiel gelesen, dass:

"Es kann anonyme Funktionen geben" : Lambda-Funktionen sind nicht anonym, sondern werden nur Lambda genannt. In der mathematischen Notation ist es zulässig, dieselbe Variable für verschiedene Funktionen zu verwenden, wenn der Name nicht wichtig ist. Beispielsweise werden die beiden Funktionen in einer Galois-Verbindung häufig als * bezeichnet.

"Funktionen können Funktionen als Eingaben akzeptieren" : Nicht neu können Sie dies mit normalen Funktionen tun.

"Funktionen sind Black Boxes" : Nur Ein- und Ausgänge sind auch gültige Beschreibungen mathematischer Funktionen ...

Dies mag wie eine Diskussion oder eine mit einer Meinung versehene Frage erscheinen, aber ich glaube, dass es eine "richtige" Antwort auf diese Frage geben sollte. Ich möchte wissen, ob die Lambda-Rechnung nur eine Schreibweise oder eine syntaktische Konvention für die Arbeit mit mathematischen Funktionen ist oder ob es wesentliche oder semantische Unterschiede zwischen Lambdas und gewöhnlichen Funktionen gibt.

Ironischerweise ist der Titel auf den Punkt gebracht, aber nicht so, wie Sie es zu meinen scheinen: "Ist der Lambda-Kalkül nur eine Notationskonvention?", Was nicht korrekt ist.

Lambda-Terme sind keine Funktionen ¹ . Sie sind Syntaxelemente, dh Symbolsammlungen auf einer Seite. Wir haben Regeln für die Manipulation dieser Symbolsammlungen, insbesondere für die Beta-Reduzierung. Sie können mehrere verschiedene Lambda-Terme haben, die der gleichen Funktion entsprechen. ²

Ich werde Ihre Punkte direkt ansprechen.

Erstens ist Lambda kein Name, der wiederverwendet wird. Dies wäre nicht nur äußerst verwirrend, sondern wir schreiben auch nicht $\lambda(x)$ (oder $(\lambda\ x)$ ), was wir tun würden, wenn $\lambda$ ein Name für eine Funktion wäre, genau wie wir $f(x)$ schreiben . In $f(x)$ konnten wir ersetzen $f$ mit dem Lambda - Term Herstellung von so etwas wie (wenn es von einem Lambda - Ausdruck definiert wurde) $(\lambda y.y)(x)$ bedeutet $(\lambda y.y)$ ist ein Ausdruck, der eine Funktion darstellen kann, keine Deklaration, die eine Funktion deklariert (mit dem Namen$\lambda$ oder etwas anderem). Wenn wir die Terminologie / Notation überladen, geschieht dies jedenfalls (so hofft man) auf eine Art und Weise, bei der eine eindeutige Zuordnung über den Kontext möglich ist, was bei Lambda-Begriffen sicherlich nicht der Fall ist.

Ihr nächster Punkt ist in Ordnung, aber etwas irrelevant. Dies ist kein Wettbewerb, bei dem es Team Lambda Terms und Team Functions gibt, und nur einer kann gewinnen. Eine Hauptanwendung von Lambda-Begriffen ist das Studieren und Verstehen bestimmter Arten von Funktionen. Ein Polynom ist keine Funktion, obwohl wir sie oft schlampig identifizieren. Das Studieren von Polynomen bedeutet nicht, dass man glaubt, dass alle Funktionen Polynome sein sollten, und es ist auch nicht so, dass Polynome etwas "Neues" tun müssen, um es wert zu sein, studiert zu werden.

Mengen-theoretische Funktionen sind keine Black Boxes, obwohl sie vollständig durch ihre Eingabe-Ausgabe-Beziehung definiert sind. (Sie buchstäblich sind ihre Input-Output - Relation.) Lambda Begriffe sind auch nicht schwarz - Boxen , und sie sind nicht durch ihr Input-Output - Verhältnis definiert. Wie ich bereits erwähnt habe, können Sie verschiedene Lambda-Terme verwenden, die die gleiche Eingabe-Ausgabe-Beziehung ergeben. Dies unterstreicht auch die Tatsache, dass Lambda-Terme keine Funktionen sein können, obwohl sie Funktionen auslösen können. ²

Tatsächlich ist die Analogie zwischen Polynomen und Lambda-Termen sehr ähnlich, und ich vermute, dass Sie die Unterscheidung zwischen einem Polynom und der Funktion, die es darstellt, nicht richtig einschätzen, weshalb ich etwas näher darauf eingehen werde. ³ Wenn Polynome eingeführt werden, normalerweise mit reellen Koeffizienten, werden sie typischerweise als reelle Funktionen eines bestimmten Typs behandelt. Betrachten Sie nun die Theorie der Linear-Feedback-Schieberegister (LFSRs). Es ist größtenteils die Theorie von (univariaten) Polynomen über $\mathbb F_2$ , aber wenn wir das als Funktion $\mathbb F_2\to\mathbb F_2$ , dann gibt es höchstens $4$ solcher Funktionen. Es gibt jedoch unendlich viele Polynome über $\mathbb F_2$ . ⁴Eine Möglichkeit, dies zu sehen, besteht darin, dass wir diese Polynome als etwas anderes als$\mathbb F_2\to\mathbb F_2$ -Funktioneninterpretieren können, was in der Tat jede$\mathbb F_2$ -Algebra tun wird. Für LFSR interpretieren wir die Polynome gewöhnlich als Operationen auf Bitströmen, die, wenn wir wollten, als Funktionen$\mathbf{2}^{\mathbb N}\to\mathbf{2}^{\mathbb N}$ könnten, obwohl die überwiegende Mehrheit dieser Funktionen nicht im Bild der Interpretation eines LFSR wäre.

Dies gilt auch für Lambda-Terme. Wir können beide als andere Dinge als Funktionen interpretieren. Sie sind auch beide viel leichter zu handhabende Objekte als die normalerweise unzähligen unendlichen Mengen von Funktionen. Sie sind beide viel rechenintensiver als beliebige Funktionen. Ich kann ein Programm schreiben, um Polynome (mit Koeffizienten, die zumindest berechenbar sind) und Lambda-Terme zu manipulieren. In der Tat sind untypisierte Lambda-Terme eines der ursprünglichen Modelle berechenbarer Funktionen. Diese symbolischere / syntaktischere, berechnendere / rechnendere Perspektive wird normalerweise stärker betont, insbesondere für den untypisierten Lambda-Kalkül, als für die semantischeren Interpretationen des Lambda-Kalküls. GetipptLambda-Terme sind weitaus handlichere Dinge und können normalerweise (aber nicht immer) leicht als Mengenfunktionen interpretiert werden, können aber auch normalerweise in eine noch breitere Klasse von Dingen interpretiert werden als der untypisierte Lambda-Kalkül. Sie haben auch eine reiche eigene syntaktische Theorie und eine sehr tiefe Verbindung zur Logik .

¹ Es ist möglich, dass das Problem in die andere Richtung geht. Vielleicht haben Sie ein Missverständnis darüber, was eine Funktion ist.

$D$$D$$D$$D^D\subseteq D$und für die Kategorie der Mengen gibt es keine nicht trivialen reflexiven Objekte. Die Geschichte ist für typisierte Lambda-Begriffe etwas anders , kann aber dennoch nicht trivial sein.

³ Wenn Sie sich über diese Unterscheidung klar sind, sollte die Analogie ziemlich informativ sein.

⁴ Dieses Problem tritt bei Feldern des Merkmals 0 wie komplexen Zahlen, Real, Rationalen oder Ganzzahlen nicht auf, sodass die Unterscheidung nicht so scharf ist, obwohl sie noch vorhanden ist.

Denken Sie über das Konzept der Variablen nach. In alten Sprachen wie Basic hatten Sie keine dynamische Zuordnung und benötigten einen Namen für jede Variable. (Dies ist nicht genau, da Sie Arrays hatten, aber die Idee ist, dass ...) In vielen Fällen müssen Sie in der Lage sein, so viele Variablen zuzuweisen, wie Sie möchten, ohne durch die Anzahl der von Ihrem Programm definierten Namen beschränkt zu sein.

Mit Lambda-Funktionen können Sie die gleiche Einschränkung bei Funktionsnamen aufheben, sodass Ihr Programm so viele Funktionen definieren kann, wie es benötigt, und diese in den gleichen komplexen Datenstrukturen wie andere Variablen "speichern" kann. Mit herkömmlichen benannten Funktionen ist dies nicht möglich.