Kombinatorische Logik

Kombinatorische Logik (Abgekürzt CL für engl. Combinatory Logic) ist eine Notation, die von Moses Schönfinkel und Haskell Brooks Curry eingeführt wurde, um die Verwendung von Variablen in der Mathematischen Logik zu vermeiden. Sie wird besonders in der Informatik als theoretisches Modell für Berechnung, als auch als Grundlage zum Design funktionaler Programmiersprachen eingesetzt.

Kombinatorische Logik in der MathematikBearbeiten

Die Kombinatorische Logik war als einfachere Logik gedacht, die die Bedeutung von quantifizierten Variablen in der Notation von Logik klären und sie tatsächlich unnötig machen sollte.

Siehe Curry, 1958–1972.

Kombinatorische Logik in der InformatikBearbeiten

In der Informatik dient die kombinatorische Logik als einfaches Modell einer Berechnung. Dieses wird in der Berechenbarkeitstheorie und der Beweistheorie benötigt. In der Tat erfasst die kombinatorische Logik viele Aspekte natürlicher Berechnung.

Man kann die kombinatorische Logik als Variation des Lambda-Kalküls auffassen, wobei die Ausdrücke des Lambda-Kalküls durch einige wenige Kombinatoren ersetzt werden. Kombinatoren sind primitive Funktionen, die keine freien Variablen enthalten. Da es sehr einfach ist, Lambda-Ausdrücke in Terme der CL umzuwandeln, und sich die Reduktion von Kombinatoren wesentlich einfacher gestaltet als die Lambda-Reduktion, wird die CL gerne als Implementationsgrundlage für nicht-strikte Sprachen verwendet.

Man kann die CL auch auf viele andere Art und Weisen betrachten, so zeigen viele frühere Abhandlungen die Äquivalenz verschiedener Kombinatoren zu Axiomen der Logik. [Hindley and Meredith, 1990].

Eine kurze Zusammenfassung des Lambda-KalkülsBearbeiten

Eine ausführliche Beschreibung des Lambda-Kalküls findet sich unter dessen Artikel. Lambda-Terme bestehen aus

  • Variablen  ,
  • Abstraktionen  ,
  • Applikationen  ,

wobei   hier für einen beliebigen Variablennamen und  ,   und   wiederum für Lambda-Terme stehen. Lambda-Terme werden durch Beta-Reduktion vereinfacht, wobei die Applikation   ersetzt wird durch die Ersetzung  .

Die Kombinatorische Logik ist ein Berechnungsmodell, das äquivalent zum Lambda-Kalkül ist, aber ohne die Abstraktion auskommt.

Der kombinatorische KalkülBearbeiten

Da Abstraktion im Lambda-Kalkül verwendet wird, um Funktionen zu modellieren, muss es im kombinatorischen Kalkül etwas vergleichbares geben. Hier gibt es statt der Abstraktion einige wenige primitive Funktionen (Kombinatoren), aus denen nun weitere Funktionen zusammengesetzt werden können.

Kombinatorische TermeBearbeiten

Kombinatorische Terme bestehen aus

  • Kombinatoren  
  • Applikationen  

  und   sind wiederum kombinatorische Terme. Die Applikation ist, wie im Lambda-Kalkül, linksassoziativ, das heißt   ist gleichbedeutend mit  .

Beispiele von KombinatorenBearbeiten

 ,   usw. bezeichnen im Folgenden beliebige Terme.

Der einfachste Kombinator ist  , der Identitätskombinator. Für ihn gilt:

 

Ein weiterer, einfacher Kombinator ist  , der Konstantenkombinator.   modelliert eine Funktion, die für ein weiteres Argument immer   zurückgibt, also:

 

Ein dritter Kombinator ist  , er stellt eine generalisierte Version der Applikation dar:

 

  wendet   auf   an, setzt jedoch zuvor   in beide ein.

Eigentlich ist   unnötig, wenn man   und   hat, denn

 
 
 
 .

FixpunktkombinatorBearbeiten

Noch interessanter ist der Fixpunktkombinator  , der verwendet wird, um Rekursion zu implementieren.

 

Auch   ist unnötig. Es kann, falls keine Typisierung erforderlich ist, als

 

dargestellt werden.

Vollständigkeit der Grundlage S-KBearbeiten

Erstaunlich ist, dass man aus   und   allein Kombinatoren zusammensetzen kann, die extensional gleich jedem beliebigen Lambda-Term sind, und daher, gemäß der These von Church, extensional gleich jeder beliebigen berechenbaren Funktion. Als Beweis dient eine Transformation  , die Lambda-Terme in einen Äquivalenten CL-Term verwandelt. Einzige Voraussetzung ist, dass der zu transformierende Lambda-Term keine freien Variablen enthält.

  kann folgendermaßen definiert werden

  1.  
  2.  
  3.   (nur, wenn   nicht frei in  )
  4.  
  5.   (falls   freie Variable von  )
  6.  

Die Transformation eines Lambda-Terms in einen CL-TermBearbeiten

Wir versuchen zum Beispiel, den Term   in einen CL-Term zu übersetzen:

 
  (Regel 5)
  (Regel 6)
  (Regel 4)
  (Regel 3 und Regel 1)
  (Regel 6)
  (Regel 3)
  (Regel 6)
  (Regel 3)
  (Regel 4)

Wenn wir nun diesen Kombinator auf zwei Terme   und   anwenden, sieht die Reduktion folgendermaßen aus:

 
 
 
 
 
 
 
 
 

Die kombinatorische Repräsentation   ist viel länger als der Lambda-Term  . Das ist typisch für die Transformation. Generell kann es passieren, dass eine  -Konstruktion einen Lambda-Term der Länge   in einen Kombinator der Länge   umwandelt.

Erläuterung der T[ ]-TransformationBearbeiten

Die Motivation der  -Transformation ist die Eliminierung von Abstraktionen. Drei der Regeln sind trivial: Regel 4 transformiert   in seine eindeutige Äquivalenz  , Regel 3 transformiert   zu  , was allerdings nur funktioniert, wenn die gebundene Variable   in   nicht verwendet wird (i.e.: in   nicht frei ist). Regel 2 transformiert die Applikation zweier Terme, was auch in den Termen der CL erlaubt ist.

Regel 1 ist etwas schwierig, denn sie konvertiert Variablen: Variablen können nur durch Regel 4 aufgelöst werden, daher bleiben sie fürs Erste erhalten. Da es keine freien Variablen im Gesamtterm gibt und jede Transformation von Abstraktionen die gebundenen Variablen berücksichtigt (Regeln 3,4,5,6), werden irgendwann alle Variablen aufgelöst.

Die Regeln 5 und 6 verschieben die Abstraktionen ins Innere des Funktionskörpers, bis sie von Regel 4 aufgelöst werden können. Regel 5 konvertiert dazu zuerst den Körper der äußeren Abstraktion, danach die Abstraktion selbst. Regel 6 verteilt die Abstraktion über einer Applikation auf deren Teilterme:

  ist eine Funktion, die ein Argument nimmt und im Lambda-Term   für   einsetzt. Genau dies tut der Kombinator  , nur für Funktionen   bzw.  :

 
 
 

Daher gilt, gemäß extensionaler Gleichheit:

 

Um nun einen Kombinator für   zu finden, reicht es aus einem Kombinator für   zu finden, also:

 

Vereinfachung der TransformationBearbeiten

η-ReduktionBearbeiten

Die Kombinatoren, die   liefert, werden kürzer wenn wir die η-Reduktion aus dem Lambda-Kalkül verwenden:

  (nur, wenn   nicht frei in  )

  ist die Funktion, die ein Argument   nimmt, und es in die Funktion   einsetzt; dies ist extensional gleich der Funktion   selbst. Es ist daher ausreichend, einfach   in seine Kombinatorische Form zu transformieren.

Mit dieser Vereinfachung wird das obige Beispiel zu:

 
 
 
  (durch η-Reduktion)

Dieser Kombinator ist (extensional) gleich dem längeren aus dem vorangegangenen Beispiel:

 
 
 
 
 
 

Ganz ähnlich würde die normale  -Transformation die Identitätsfunktion   verwandeln in  . Mit der neuen η-Reduktionsregel wird aus   einfach nur  .

Die Kombinatoren B, C von CurryBearbeiten

Die Kombinatoren   und   tauchen bereits in der Arbeit von Schönfinkel auf (allerdings hieß   dort  ), Curry führte in seiner Dissertation Grundlagen der kombinatorischen Logik weiterhin  ,  ,   (und  ) ein.   und   können viele Reduktionen vereinfachen, sie sehen folgendermaßen aus:

 
 

Für diese beiden Kombinatoren werden die Regeln folgendermaßen erweitert:

  1.  
  2.  
  3.   (nur, wenn   nicht frei in  )
  4.  
  5.   (falls   freie Variable von  )
  6.   (falls   freie Variable von   und  )
  7.   (falls   freie Variable von   aber nicht von  )
  8.   (falls   freie Variable von   aber nicht von  )

Zum Beispiel sieht die Transformation von   so aus:

 
 
  (Regel 7)
 
  (η-Reduktion)
  (Notation für:  )
  (Notation für:  )

Tatsächlich reduziert   zu  :

 
 
 

  und   stellen beschränkte Versionen von   dar. Während   einen Wert sowohl in den Applikanten als auch in das Argument einsetzt, setzt   diesen nur in den Applikanten und   nur in das Argument ein.

Umgekehrte TransformationBearbeiten

Die Transformation   von CL-Termen in Lambda-Terme ist denkbar einfach, da wir im Lambda-Kalkül alle Möglichkeiten haben, die auch in der CL zur Verfügung stehen:

 
 
 
 
 
 

Wichtig ist jedoch zu wissen, dass diese Transformation nicht das Inverse der  -Transformation ist, da   zwar extensional gleich   ist, aber der Term dabei nicht zwingend erhalten bleibt.

Unentscheidbarkeit des kombinatorischen KalkülsBearbeiten

Es ist unentscheidbar, ob ein genereller Kombinator eine Normalform hat, ob zwei Kombinatoren gleich sind usw. Dies ergibt sich schon aus der Ähnlichkeit zum Lambda-Kalkül, aber hier noch einmal ein direkter Beweis:

Der Term

 

hat keine Normalform, da er mit drei Schritten wieder zu sich selbst reduziert:

 
 
 
 

und es keinen anderen Weg geben kann, der den Kombinator kürzer macht.

Sei nun   ein Kombinator, der auf Normalform testet, so dass

 , wenn   eine Normalform hat,
 , andernfalls.

(  und   sind hier die korrespondierenden Kombinatoren zu   und   aus dem Lambda-Kalkül:

 
 )

Sei nun

 

Untersuchen wir den Term  . Hat   eine Normalform? Falls ja, müssen auch die folgenden Ableitungen eine Normalform haben:

 
 
 
 
  (Definition von  )
 
 
 

Nun wenden wir   auf   an. Entweder hat   eine Normalform oder nicht.

Wenn ja, dann wäre:

 
  (Definition von  )
 

aber   hat keine Normalform.   haben wir durch Ableitungen aus   erhalten, also hat auch   keine Normalform. Dies ist ein Widerspruch.

Falls   keine Normalform hat, reduziert sich der Term folgendermaßen:

 
  (Definition von  )
 
 

was bedeutet, dass   als Normalform einfach   hat, also wieder ein Widerspruch. Daher kann es keinen solchen Kombinator   geben.

AnwendungsgebieteBearbeiten

Übersetzung funktionaler ProgrammiersprachenBearbeiten

Funktionale Programmiersprachen basieren häufig auf der einfachen, aber universellen Semantik des Lambda-Kalküls.

David Turner benutzte CL für die Sprache SASL.

ReferenzenBearbeiten

  • „Über die Bausteine der mathematischen Logik“, Moses Schönfinkel, 1924, übersetzt als „On the Building Blocks of Mathematical Logic“ in From Frege to Gödel: a source book in mathematical logic, 1879–1931, ed. Jean van Heijenoort, Harvard University Press, 1977. ISBN 0-674-32449-8 – Die Originalpublikation über kombinatorische Logik.
  • Combinatory Logic. Curry, Haskell B. et al., North-Holland, 1972. ISBN 0-7204-2208-6 – Eine umfassende Übersicht der CL, inklusive der historischen Umrisse.
  • Functional Programming. Field, Anthony J. and Peter G. Harrison. Addison-Wesley, 1998. ISBN 0-201-19249-7
  • „Foundations of Functional Programming“ (GZIP; 105 kB). Lawrence C. Paulson. University of Cambridge, 1995.
  • „Lectures on the Curry-Howard Isomorphism“. Sørensen, Morten Heine B. and Pawel Urzyczyn. University of Copenhagen and University of Warsaw, 1998.
  • „Principal Type-Schemes and Condensed Detachment“, Hindley and Meredith, Journal of Symbolic Logic (JSL), Volume 55 (1990), Number 1, pages 90–105

WeblinksBearbeiten