Ich versuche, besser zu verstehen, wie Typen im Lambda-Kalkül ins Spiel kommen. Zugegebenermaßen ist eine Menge des Typs Theorie über meinen Kopf. Lisp ist eine dynamisch typisierte Sprache, würde das in etwa dem untypisierten Lambda-Kalkül entsprechen? Oder gibt es eine Art "dynamisch typisierten Lambda-Kalkül", von dem ich nichts weiß?Welche Art von Lambda-Kalkül würde Lisp locker ein Beispiel sein?
Lisp ist eine dynamisch typisierte Sprache, würde das etwa dem untypisierten Lambda-Kalkül entsprechen?
Ja, aber nur grob. Im "reinen" untypisierten Lambda-Kalkül ist alles als Funktion kodiert. (Sie können nach der beliebten "Church encoding" und der weniger populären "Scott encoding" googeln.) Lisp hat nicht-funktionale Daten, wie Atome und Zahlen und so, so würde dies als "untypisierte Lambda-Kalkül mit Konstanten erweitert" zählen.
Ein weiterer wichtiger Unterschied ist in Reihenfolge der Bewertung. Regeln zum Reduzieren von Lambda-Kalkül-Termen sind hochgradig nicht deterministisch. (Es gibt ein Theorem, das Church-Rosser-Theorem, das locker sagt, dass, solange Dinge enden, die Reihenfolge der Bewertung keine Rolle spielt.) In der Praxis werden Lambda-Terme typischerweise mit der äußersten linken äußersten Aka-Reduktion "normaler Ordnung" reduziert, weil beliebig Reduktions-Strategie beendet, dass man tut. Dies unterscheidet sich sehr von Lisp, das Argumente immer in die normale Form vor einer Beta-Reduktion auswertet. Diese Bewertungsreihenfolge wird als "Aufruf nach Wert" bezeichnet.
Zusammenfassend entspricht Lisp ein untypisierter Call-by-Value-Lambda-Kalkül erweitert mit Konstanten.
John McCarthy eingeführt LISP in his April, 1960 paper "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I". Der folgende Absatz ist von Seite 6:
e. Funktionen und Formulare. In der Mathematik ist es üblich - außerhalb der mathematischen Logik -, das Wort "Funktion" ungenau zu verwenden und es auf die Formen wie y + x anzuwenden. Weil wir später mit den Ausdrücken für Funktionen rechnen müssen, brauchen wir eine Unterscheidung zwischen Funktionen und Formen und eine Notation für diese Unterscheidung. Diese Unterscheidung und eine Notation zur Beschreibung von , von der wir trivial abweichen, wird von Church [3] gegeben.
...
3. A. KIRCHE, Die Kalküle der Lambda-Umwandlung (Princeton University Press, Princeton, N. J., 1941).
Die Wikipedia article on lambda-calculus hat eine Geschichte der Publikationen der Kirche. Das Papier von 1941, auf das McCarthy Bezug nimmt, scheint über die getippte lambda-Kalkül zu sein, im Gegensatz zu der Einleitung des Wikipedia-Artikels.
Das Schlüsselwort lambda in Lisp kann nur durch Analogie auf den Lambda-Kalkül bezogen werden. Ein Lisp-Lambda-Ausdruck ist ein Typ von anonymous function.
Das ist, was ich dachte, aber ich bin trainiert zu denken, dass untypisiert! = Dynamisch getippt. :-) –
@Heath: Das Zitat sagt jedoch ausdrücklich, dass das, was aus dem Papier entnommen wurde, die "Unterscheidung zwischen Funktionen und Formen und eine Notierung für das Ausdrücken dieser Unterscheidung" ist, anstatt das in dem Papier beschriebene System zu implementieren. – outis
Lisp ist nicht 'ein Lambda-Kalkül', ich weiß nicht, was 'ein Lambda-Kalkül' ist.
Wenn Sie Lambda-Kalküle nach Typ-Typ-System identifizieren möchten, ist Lisp natürlich seine eigene. Das "Lambda" -Schlüsselwort in jedem Lisp vor Scheme ist sicherlich protzig, und nach Schema gibt es auch Raum, um es zu sagen.Nur "Func" zu verwenden, wäre bescheidener gewesen. Lisp ist ein Listenprozessor hauptsächlich, kein 'Lambda-Kalkül'
Ich habe auch einen ziemlich ausführlichen Artikel darüber einmal geschrieben, der versucht zu demonstrieren, warum A: der Begriff 'funktionale Programmierung' bedeutungslos ist und B: warum das Sprechen von ' ein Lambda-Kalkül und nicht 'ein Typ-System' ist so zu:
http://blog.nihilarchitect.net/archives/289/on-functional-programming/
auch dasseinziges Argument in Lisp, alle Funktionen sind in der Tat im Auge behalten und nur Listen haben können als ihre Argumente.
Ihr Konto wurde gesperrt! Somit ist die Verbindung tatsächlich tot –
Wenn wir über Lisp sprechen, sollte es nicht (Lambda (Calculus)) sein ;-) –
Solange Sie nicht über Clojure sprechen. Dann wäre es '(fn [Calculus])': –
Das Problem mit dieser Frage ist, dass es keine einzige, einzigartige Lisp-Sprache gibt, sondern eine ganze Familie von ihnen. Auf welche Lisp (s) beziehen Sie sich? – outis