Sind Lambda-Kalkül und kombinatorische Logik gleich?

26

Ich lese gerade " Lambda-Kalkül und Kombinatoren " von Hindley und Seldin. Ich bin kein Experte, habe mich aber immer für Lambda-Kalkül interessiert, weil ich mich mit funktionaler Programmierung befasst habe (angefangen mit Lisp und SICP, und jetzt mit R und Haskell).

In " Binary Lambda Calculus and Combinatory Logic" stellt John Tromp fest:

CL kann als Teilmenge der Lambda-Rechnung angesehen werden ... die Theorien sind weitgehend gleich und werden bei Vorhandensein der Extensionalitätsregel gleich.

Unter welchen Bedingungen würde man kombinatorische Logik anstelle von Lambda-Kalkül verwenden ?

Alle Referenzen wäre dankbar.

combinatory-logic functional-programming lambda-calculus Shane
quelle
Schauen Sie sich "Lambda-Kalkül: Syntax und Semantik" von HP Barendregt an.
Kaveh

Antworten:

15

Was die kombinatorische Logik auszeichnet, ist, dass sie frei von Variablen ist. Dies ist manchmal nützlich in der Metamathematik und der philosophischen Logik, wo der Status von Variablen schwierig ist.

Dies kann auch bei Implementierungen hilfreich sein, da das Verwalten von Variablen Kopfzerbrechen verursachen kann. Vgl. Z. B. Hughes, 1982, Superkombinatoren: Eine neue Implementierungsmethode für anwendbare Sprachen

Charles Stewart
quelle
3
Kombinatorische Logik wird in Implementierungen nicht mehr als nützlich angesehen und wurde nie verwendet, weil "das Verwalten von Variablen Kopfschmerzen bereiten kann". Kombinatoren und Varianten wurden verwendet, um die Diagrammverkleinerung für faule Sprachen zu implementieren, aber heutzutage verwendet Haskell (die bekannteste faule Sprache) viel vernünftigere Techniken, um die Diagrammverkleinerung zu implementieren.
Blaisorblade
Siehe z. B. S. Peyton Jones, 1992, "Implementierung fauler funktionaler Sprachen auf aktueller Hardware: die spineless tagless G-Maschine" - research.microsoft.com/copyright/accept.asp?path=/users/simonpj/…
Blaisorblade,
2
@Blaisorblade: Kombinatoren und Varianten wurden verwendet, um die Diagrammverkleinerung für faule Sprachen zu implementieren. - Vorsicht: Haskell und ghc sind nicht dasselbe, und die Literatur enthält mehrere Haskells, die auf Superkombinatoren basieren. Es stimmt jedoch, dass der Stand der Technik in der funktionalen Programmierung die Effizienzvorteile der Handhabung von Umgebungen gefunden hat, die die Komplexität überwiegen. Sie sehen immer noch Supercombinatoren, die z. B. in der Logikprogrammierung höherer Ordnung verwendet werden, wo dies nicht zutrifft. Superkombinatoren bleiben Teil des Inventars der Techniken, die bei der Implementierung von Programmen höherer Ordnung verwendet werden.
Charles Stewart
Supercombinatoren vermeiden nur freie Variablen, nicht gebundene, und können daher nicht als Anwendungen der kombinatorischen Logik an sich betrachtet werden. Sie sind meist spezielle Lambda-Begriffe. Es gibt viel kleinere Unterschiede zwischen Supercombinatoren, Lambda-Lifted-Programmen (falls vorhanden, nicht sicher) und der Implementierung von GHC (wo Zeiger von einem Closure zu seinen freien Variablen dank Reinheit von der Host-Funktion kopiert werden können). Allerdings habe ich auch an den kürzlich erschienenen Utrecht Haskell Compiler gedacht, der GHC sehr ähnlich ist, aber IIRC verwendet Lambda-Lifting; Trotzdem ist das nicht CL.
Blaisorblade
Ich wusste nichts über Logikprogrammierung höherer Ordnung - ich fand dieses Papier darauf: springerlink.com/content/t68777w270713p5n . Leider ist es unwahrscheinlich, dass ich Zeit habe, es zu lesen.
Blaisorblade
4

Unter Bezugnahme auf den Kommentar von John Tromp möchte ich bemerken, dass sich die kombinatorische Logik ganz anders anfühlt als die Lambda-Rechnung. Da Sie sich für funktionale Programmierung interessieren, möchten Sie wirklich nicht so viel über kombinatorische Logik wissen.

Mein Lieblingstutorial zur kombinatorischen Logik ist in diesen Vorlesungsskripten der Universität Cambridge.

Sie werden jedoch eingeführt, um die Implementierung sogenannter fauler (oder anwendungsbezogener) Sprachen zu erläutern. Wie in meinem vorherigen Kommentar erwähnt, sind solche Techniken mittlerweile veraltet.

Blaisorblade
quelle
Welche Techniken sind derzeit auf dem neuesten Stand, da kombinatorische Sprachen nicht mehr zur Implementierung von faulen / anwendungsbezogenen Sprachen verwendet werden? Und gibt es einen Namen / eine Kategorie, um diese Techniken zu klassifizieren?
CMCDragonkai
@CMCDragonkai Siehe Kommentare unter cstheory.stackexchange.com/a/306/989 zur Diskussion. Die kurze praktische Antwort lautet: "Sehen Sie, was GHC leistet": Es gibt eine Vielzahl verschiedener Techniken (einschließlich der STG-Maschine und Optimierungen wie der Strenge-Analyse), die kombiniert werden, um träge Programme schnell zu machen.
Blaisorblade