Der Titel dieses Artikels ist mehrdeutig Zum bisweilen ebenfalls kombinatorische Logik genannten Netz aus logischen Schaltgliedern siehe Schaltnetz Kombinatorische Logik Abgekurzt CL fur engl Combinatory Logic ist eine Notation die von Moses Schonfinkel und Haskell Brooks Curry eingefuhrt wurde um die Verwendung von Variablen in der Mathematischen Logik zu vermeiden Sie wird besonders in der Informatik als theoretisches Modell fur Berechnung als auch als Grundlage zum Design funktionaler Programmiersprachen eingesetzt Inhaltsverzeichnis 1 Kombinatorische Logik in der Mathematik 2 Kombinatorische Logik in der Informatik 3 Eine kurze Zusammenfassung des Lambda Kalkuls 4 Der kombinatorische Kalkul 4 1 Kombinatorische Terme 4 2 Beispiele von Kombinatoren 4 3 Fixpunktkombinator 4 4 Vollstandigkeit der Grundlage S K 4 4 1 Die Transformation eines Lambda Terms in einen CL Term 4 4 2 Erlauterung der T Transformation 4 5 Vereinfachung der Transformation 4 5 1 h Reduktion 4 5 2 Die Kombinatoren B C von Curry 4 6 Umgekehrte Transformation 5 Unentscheidbarkeit des kombinatorischen Kalkuls 6 Anwendungsgebiete 6 1 Ubersetzung funktionaler Programmiersprachen 7 Quellen 8 WeblinksKombinatorische Logik in der Mathematik BearbeitenDie Kombinatorische Logik war als einfachere Logik gedacht die die Bedeutung von quantifizierten Variablen in der Notation von Logik klaren und sie tatsachlich unnotig machen sollte Siehe Curry 1958 1972 Kombinatorische Logik in der Informatik BearbeitenIn der Informatik dient die kombinatorische Logik als einfaches Modell einer Berechnung Dieses wird in der Berechenbarkeitstheorie und der Beweistheorie benotigt In der Tat erfasst die kombinatorische Logik viele Aspekte naturlicher Berechnung Man kann die kombinatorische Logik als Variation des Lambda Kalkuls auffassen wobei die Ausdrucke des Lambda Kalkuls durch einige wenige Kombinatoren ersetzt werden Kombinatoren sind primitive Funktionen die keine freien Variablen enthalten Da es sehr einfach ist Lambda Ausdrucke in Terme der CL umzuwandeln und sich die Reduktion von Kombinatoren wesentlich einfacher gestaltet als die Lambda Reduktion wird die CL gerne als Implementationsgrundlage fur nicht strikte Sprachen verwendet Man kann die CL auch auf viele andere Art und Weisen betrachten so zeigen viele fruhere Abhandlungen die Aquivalenz verschiedener Kombinatoren zu Axiomen der Logik Hindley and Meredith 1990 Eine kurze Zusammenfassung des Lambda Kalkuls BearbeitenEine ausfuhrliche Beschreibung des Lambda Kalkuls findet sich unter dessen Artikel Lambda Terme bestehen aus Variablen v displaystyle v nbsp Abstraktionen l v T displaystyle lambda v T nbsp Applikationen T 1 T 2 displaystyle T1 T2 nbsp wobei v displaystyle v nbsp hier fur einen beliebigen Variablennamen und T displaystyle T nbsp T 1 displaystyle mathit T 1 nbsp und T 2 displaystyle T2 nbsp wiederum fur Lambda Terme stehen Lambda Terme werden durch Beta Reduktion vereinfacht wobei die Applikation l v E a displaystyle lambda v E a nbsp ersetzt wird durch die Ersetzung E v a displaystyle E v a nbsp Die Kombinatorische Logik ist ein Berechnungsmodell das aquivalent zum Lambda Kalkul ist aber ohne die Abstraktion auskommt Der kombinatorische Kalkul BearbeitenDa Abstraktion im Lambda Kalkul verwendet wird um Funktionen zu modellieren muss es im kombinatorischen Kalkul etwas Vergleichbares geben Hier gibt es statt der Abstraktion einige wenige primitive Funktionen Kombinatoren aus denen nun weitere Funktionen zusammengesetzt werden konnen Kombinatorische Terme Bearbeiten Kombinatorische Terme bestehen aus Kombinatoren P displaystyle P nbsp Applikationen T 1 T 2 displaystyle T1 T2 nbsp T 1 displaystyle T1 nbsp und T 2 displaystyle T2 nbsp sind wiederum kombinatorische Terme Die Applikation ist wie im Lambda Kalkul linksassoziativ das heisst T 1 T 2 T 3 T 4 displaystyle T1 T2 T3 T4 nbsp ist gleichbedeutend mit T 1 T 2 T 3 T 4 displaystyle T1 T2 T3 T4 nbsp Beispiele von Kombinatoren Bearbeiten x displaystyle x nbsp y displaystyle y nbsp usw bezeichnen im Folgenden beliebige Terme Der einfachste Kombinator ist I displaystyle mathbf I nbsp der Identitatskombinator Fur ihn gilt I x x displaystyle mathbf I x x nbsp Ein weiterer einfacher Kombinator ist K displaystyle mathbf K nbsp der Konstantenkombinator K x displaystyle mathbf K x nbsp modelliert eine Funktion die fur ein weiteres Argument immer x displaystyle x nbsp zuruckgibt also K x y x displaystyle mathbf K x y x nbsp Ein dritter Kombinator ist S displaystyle mathbf S nbsp er stellt eine generalisierte Version der Applikation dar S x y z x z y z displaystyle mathbf S x y z x z y z nbsp S displaystyle mathbf S nbsp wendet x displaystyle x nbsp auf y displaystyle y nbsp an setzt jedoch zuvor z displaystyle z nbsp in beide ein Eigentlich ist I displaystyle mathbf I nbsp unnotig wenn man S displaystyle mathbf S nbsp und K displaystyle mathbf K nbsp hat denn S K K x displaystyle mathbf S mathbf K mathbf K x nbsp S K K x displaystyle mathbf S mathbf K mathbf K x nbsp K x K x displaystyle mathbf K x mathbf K x nbsp x displaystyle x nbsp dd Fixpunktkombinator Bearbeiten Noch interessanter ist der Fixpunktkombinator Y displaystyle mathbf Y nbsp der verwendet wird um Rekursion zu implementieren Y x x Y x displaystyle mathbf Y mathbf x mathbf x mathbf Y mathbf x nbsp Auch Y displaystyle mathbf Y nbsp ist unnotig Es kann falls keine Typisierung erforderlich ist als Y S I I S K S I S I I displaystyle mathbf Y mathbf S mathbf I mathbf I mathbf S mathbf K mathbf S mathbf I mathbf S mathbf I mathbf I nbsp dargestellt werden Vollstandigkeit der Grundlage S K Bearbeiten Erstaunlich ist dass man aus S displaystyle mathbf S nbsp und K displaystyle mathbf K nbsp allein Kombinatoren zusammensetzen kann die extensional gleich jedem beliebigen Lambda Term sind und daher gemass der These von Church extensional gleich jeder beliebigen berechenbaren Funktion Als Beweis dient eine Transformation T displaystyle T nbsp die Lambda Terme in aquivalente CL Terme verwandelt Einzige Voraussetzung ist dass der zu transformierende Lambda Term keine freien Variablen enthalt T displaystyle T nbsp kann folgendermassen definiert werden T V V displaystyle T V Rightarrow V nbsp T E 1 E 2 T E 1 T E 2 displaystyle T E1 E2 Rightarrow T E1 T E2 nbsp T l x E K T E displaystyle T lambda x E Rightarrow mathbf K T E nbsp nur wenn x displaystyle x nbsp nicht frei in E displaystyle E nbsp T l x x I displaystyle T lambda x x Rightarrow mathbf I nbsp T l x l y E T l x T l y E displaystyle T lambda x lambda y E Rightarrow T lambda x T lambda y E nbsp falls x displaystyle x nbsp freie Variable von E displaystyle E nbsp T l x E 1 E 2 S T l x E 1 T l x E 2 displaystyle T lambda x E1 E2 Rightarrow mathbf S T lambda x E1 T lambda x E2 nbsp Die Transformation eines Lambda Terms in einen CL Term Bearbeiten Als Beispiel wird der Term l x l y y x displaystyle lambda x lambda y y x nbsp in einen CL Term ubersetzt T l x l y y x displaystyle T lambda x lambda y y x nbsp T l x T l y y x displaystyle T lambda x T lambda y y x nbsp Regel 5 T l x S T l y y T l y x displaystyle T lambda x mathbf S T lambda y y T lambda y x nbsp Regel 6 T l x S I T l y x displaystyle T lambda x mathbf S mathbf I T lambda y x nbsp Regel 4 T l x S I K x displaystyle T lambda x mathbf S mathbf I mathbf K x nbsp Regel 3 und Regel 1 S T l x S I T l x K x displaystyle mathbf S T lambda x mathbf S mathbf I T lambda x mathbf K x nbsp Regel 6 S K S I T l x K x displaystyle mathbf S mathbf K mathbf S mathbf I T lambda x mathbf K x nbsp Regel 3 S K S I S T l x K T l x x displaystyle mathbf S mathbf K mathbf S mathbf I mathbf S T lambda x mathbf K T lambda x x nbsp Regel 6 S K S I S K K T l x x displaystyle mathbf S mathbf K mathbf S mathbf I mathbf S mathbf K mathbf K T lambda x x nbsp Regel 3 S K S I S K K I displaystyle mathbf S mathbf K mathbf S mathbf I mathbf S mathbf K mathbf K mathbf I nbsp Regel 4 dd Wenn nun dieser Kombinator auf zwei Terme x displaystyle x nbsp und y displaystyle y nbsp angewendet wird sieht die Reduktion folgendermassen aus S K S I S K K I x y displaystyle mathbf S mathbf K mathbf S mathbf I mathbf S mathbf K mathbf K mathbf I x y nbsp K S I x S K K I x y displaystyle mathbf K mathbf S mathbf I x mathbf S mathbf K mathbf K mathbf I x y nbsp S I S K K I x y displaystyle mathbf S mathbf I mathbf S mathbf K mathbf K mathbf I x y nbsp I y S K K I x y displaystyle mathbf I y mathbf S mathbf K mathbf K mathbf I x y nbsp y S K K I x y displaystyle y mathbf S mathbf K mathbf K mathbf I x y nbsp y K K x I x y displaystyle y mathbf K mathbf K x mathbf I x y nbsp y K I x y displaystyle y mathbf K mathbf I x y nbsp y I x displaystyle y mathbf I x nbsp y x displaystyle y x nbsp dd Die kombinatorische Reprasentation S K S I S K K I displaystyle mathbf S mathbf K mathbf S mathbf I mathbf S mathbf K mathbf K mathbf I nbsp ist viel langer als der Lambda Term l x l y y x displaystyle lambda x lambda y y x nbsp Das ist typisch fur die Transformation Generell kann es passieren dass eine T displaystyle T nbsp Konstruktion einen Lambda Term der Lange n displaystyle n nbsp in einen Kombinator der Lange 8 3 n displaystyle Theta 3 n nbsp umwandelt Erlauterung der T Transformation Bearbeiten Die Motivation der T displaystyle T nbsp Transformation ist die Eliminierung von Abstraktionen Drei der Regeln sind trivial Regel 4 transformiert l x x displaystyle lambda x x nbsp in seine eindeutige Aquivalenz I displaystyle mathbf I nbsp Regel 3 transformiert l x E displaystyle lambda x E nbsp zu K T E displaystyle mathbf K T E nbsp was allerdings nur funktioniert wenn die gebundene Variable x displaystyle x nbsp in E displaystyle E nbsp nicht verwendet wird i e in E displaystyle E nbsp 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 konnen nur durch Regel 4 aufgelost werden daher bleiben sie furs Erste erhalten Da es keine freien Variablen im Gesamtterm gibt und jede Transformation von Abstraktionen die gebundenen Variablen berucksichtigt Regeln 3 4 5 6 werden irgendwann alle Variablen aufgelost Die Regeln 5 und 6 verschieben die Abstraktionen ins Innere des Funktionskorpers bis sie von Regel 4 aufgelost werden konnen Regel 5 konvertiert dazu zuerst den Korper der ausseren Abstraktion danach die Abstraktion selbst Regel 6 verteilt die Abstraktion uber einer Applikation auf deren Teilterme l x E 1 E 2 displaystyle lambda x E1 E2 nbsp ist eine Funktion die ein Argument nimmt und im Lambda Term E 1 E 2 displaystyle E1 E2 nbsp fur x displaystyle x nbsp einsetzt Genau dies tut der Kombinator S displaystyle mathbf S nbsp nur fur Funktionen E 1 x displaystyle E1 x nbsp bzw E 2 x displaystyle E2 x nbsp l x E 1 E 2 a l x E 1 a l x E 2 a displaystyle lambda x E1 E2 a lambda x E1 a lambda x E2 a nbsp S l x E 1 l x E 2 a displaystyle mathbf S lambda x E1 lambda x E2 a nbsp S l x E 1 l x E 2 a displaystyle mathbf S lambda x E1 lambda x E2 a nbsp dd Daher gilt gemass extensionaler Gleichheit l x E 1 E 2 S l x E 1 l x E 2 displaystyle lambda x E1 E2 mathbf S lambda x E1 lambda x E2 nbsp Um nun einen Kombinator fur l x E 1 E 2 displaystyle lambda x E1 E2 nbsp zu finden reicht es aus einem Kombinator fur S l x E 1 l x E 2 displaystyle mathbf S lambda x E1 lambda x E2 nbsp zu finden also S T l x E 1 T l x E 2 displaystyle mathbf S T lambda x E1 T lambda x E2 nbsp Vereinfachung der Transformation Bearbeiten h Reduktion Bearbeiten Die Kombinatoren die T displaystyle T nbsp liefert werden kurzer wenn wir die h Reduktion aus dem Lambda Kalkul verwenden T l x E x T E displaystyle T lambda x E x T E nbsp nur wenn x displaystyle x nbsp nicht frei in E displaystyle E nbsp l x E x displaystyle lambda x E x nbsp ist die Funktion die ein Argument x displaystyle x nbsp nimmt und es in die Funktion E displaystyle E nbsp einsetzt dies ist extensional gleich der Funktion E displaystyle E nbsp selbst Es ist daher ausreichend einfach E displaystyle E nbsp in seine Kombinatorische Form zu transformieren Mit dieser Vereinfachung wird das obige Beispiel zu T l x l y y x displaystyle T lambda x lambda y y x nbsp displaystyle ldots nbsp S K S I T l x K x displaystyle mathbf S mathbf K mathbf S mathbf I T lambda x mathbf K x nbsp S K S I K displaystyle mathbf S mathbf K mathbf S mathbf I mathbf K nbsp durch h Reduktion dd Dieser Kombinator ist extensional gleich dem langeren aus dem vorangegangenen Beispiel S K S I K x y displaystyle mathbf S mathbf K mathbf S mathbf I mathbf K x y nbsp K S I x K x y displaystyle mathbf K mathbf S mathbf I x mathbf K x y nbsp S I K x y displaystyle mathbf S mathbf I mathbf K x y nbsp I y K x y displaystyle mathbf I y mathbf K x y nbsp y K x y displaystyle y mathbf K x y nbsp y x displaystyle y x nbsp dd Ganz ahnlich wurde die normale T displaystyle T nbsp Transformation die Identitatsfunktion l f l x f x displaystyle lambda f lambda x f x nbsp verwandeln in S S K S S K K I K I displaystyle mathbf S mathbf S mathbf K mathbf S mathbf S mathbf K mathbf K mathbf I mathbf K mathbf I nbsp Mit der neuen h Reduktionsregel wird aus l f l x f x displaystyle lambda f lambda x f x nbsp einfach nur I displaystyle mathbf I nbsp Die Kombinatoren B C von Curry Bearbeiten Die Kombinatoren S displaystyle mathbf S nbsp und K displaystyle mathbf K nbsp tauchen bereits in der Arbeit von Schonfinkel auf allerdings hiess K displaystyle mathbf K nbsp dort C displaystyle mathbf C nbsp Curry fuhrte in seiner Dissertation Grundlagen der kombinatorischen Logik weiterhin B displaystyle mathbf B nbsp C displaystyle mathbf C nbsp W displaystyle mathbf W nbsp und K displaystyle mathbf K nbsp ein B displaystyle mathbf B nbsp und C displaystyle mathbf C nbsp konnen viele Reduktionen vereinfachen sie sehen folgendermassen aus C a b c a c b displaystyle mathbf C a b c a c b nbsp B a b c a b c displaystyle mathbf B a b c a b c nbsp Fur diese beiden Kombinatoren werden die Regeln folgendermassen erweitert T V V displaystyle T V Rightarrow V nbsp T E 1 E 2 T E 1 T E 2 displaystyle T E1 E2 Rightarrow T E1 T E2 nbsp T l x E K T E displaystyle T lambda x E Rightarrow mathbf K T E nbsp nur wenn x displaystyle x nbsp nicht frei in E displaystyle E nbsp T l x x I displaystyle T lambda x x Rightarrow mathbf I nbsp T l x l y E T l x T l y E displaystyle T lambda x lambda y E Rightarrow T lambda x T lambda y E nbsp falls x displaystyle x nbsp freie Variable von E displaystyle E nbsp T l x E 1 E 2 S T l x E 1 T l x E 2 displaystyle T lambda x E1 E2 Rightarrow mathbf S T lambda x E1 T lambda x E2 nbsp falls x displaystyle x nbsp freie Variable von E 1 displaystyle E1 nbsp und E 2 displaystyle E2 nbsp T l x E 1 E 2 C T l x E 1 T E 2 displaystyle T lambda x E1 E2 Rightarrow mathbf C T lambda x E1 T E2 nbsp falls x displaystyle x nbsp freie Variable von E 1 displaystyle E1 nbsp aber nicht von E 2 displaystyle E2 nbsp T l x E 1 E 2 B T E 1 T l x E 2 displaystyle T lambda x E1 E2 Rightarrow mathbf B T E1 T lambda x E2 nbsp falls x displaystyle x nbsp freie Variable von E 2 displaystyle E2 nbsp aber nicht von E 1 displaystyle E1 nbsp Zum Beispiel sieht die Transformation von l x l y y x displaystyle lambda x lambda y y x nbsp so aus T l x l y y x displaystyle T lambda x lambda y y x nbsp T l x T l y y x displaystyle T lambda x T lambda y y x nbsp T l x C T l y y x displaystyle T lambda x mathbf C T lambda y y x nbsp Regel 7 T l x C I x displaystyle T lambda x mathbf C mathbf I x nbsp C I displaystyle mathbf C mathbf I nbsp h Reduktion C displaystyle mathbf C ast nbsp Notation fur X X I displaystyle mathbf X ast mathbf X mathbf I nbsp I displaystyle mathbf I nbsp Notation fur X C X displaystyle mathbf X mathbf C mathbf X nbsp dd Tatsachlich reduziert C I x y displaystyle mathbf C mathbf I x y nbsp zu y x displaystyle y x nbsp C I x y displaystyle mathbf C mathbf I x y nbsp I y x displaystyle mathbf I y x nbsp y x displaystyle y x nbsp dd B displaystyle mathbf B nbsp und C displaystyle mathbf C nbsp stellen beschrankte Versionen von S displaystyle mathbf S nbsp dar Wahrend S displaystyle mathbf S nbsp einen Wert sowohl in den Applikanten als auch in das Argument einsetzt setzt C displaystyle mathbf C nbsp diesen nur in den Applikanten und B displaystyle mathbf B nbsp nur in das Argument ein Umgekehrte Transformation Bearbeiten Die Transformation L displaystyle L nbsp von CL Termen in Lambda Terme ist denkbar einfach da wir im Lambda Kalkul alle Moglichkeiten haben die auch in der CL zur Verfugung stehen L I l x x displaystyle L mathbf I lambda x x nbsp L K l x l y x displaystyle L mathbf K lambda x lambda y x nbsp L C l x l y l z x z y displaystyle L mathbf C lambda x lambda y lambda z x z y nbsp L B l x l y l z x y z displaystyle L mathbf B lambda x lambda y lambda z x y z nbsp L S l x l y l z x z y z displaystyle L mathbf S lambda x lambda y lambda z x z y z nbsp L E 1 E 2 L E 1 L E 2 displaystyle L E1 E2 L E1 L E2 nbsp Wichtig ist jedoch zu wissen dass diese Transformation nicht das Inverse der T displaystyle T nbsp Transformation ist da T L x displaystyle T L x nbsp zwar extensional gleich x displaystyle x nbsp ist aber der Term dabei nicht zwingend erhalten bleibt Unentscheidbarkeit des kombinatorischen Kalkuls BearbeitenEs ist unentscheidbar ob ein genereller Kombinator eine Normalform hat ob zwei Kombinatoren gleich sind usw Dies ergibt sich schon aus der Ahnlichkeit zum Lambda Kalkul aber hier noch einmal ein direkter Beweis Der Term W S I I S I I displaystyle mathbf Omega mathbf S mathbf I mathbf I mathbf S mathbf I mathbf I nbsp hat keine Normalform da er mit drei Schritten wieder zu sich selbst reduziert S I I S I I displaystyle mathbf S mathbf I mathbf I mathbf S mathbf I mathbf I nbsp I S I I I S I I displaystyle mathbf I mathbf S mathbf I mathbf I mathbf I mathbf S mathbf I mathbf I nbsp S I I I S I I displaystyle mathbf S mathbf I mathbf I mathbf I mathbf S mathbf I mathbf I nbsp S I I S I I displaystyle mathbf S mathbf I mathbf I mathbf S mathbf I mathbf I nbsp dd und es keinen anderen Weg geben kann der den Kombinator kurzer macht Sei nun N displaystyle mathbf N nbsp ein Kombinator der auf Normalform testet so dass N x T displaystyle mathbf N x Rightarrow mathbf T nbsp wenn x displaystyle x nbsp eine Normalform hat F displaystyle mathbf F nbsp andernfalls T displaystyle mathbf T nbsp und F displaystyle mathbf F nbsp sind hier die korrespondierenden Kombinatoren zu t r u e displaystyle true nbsp und f a l s e displaystyle false nbsp aus dem Lambda Kalkul t r u e l x l y x K T displaystyle true lambda x lambda y x mathbf K mathbf T nbsp f a l s e l x l y y K I F displaystyle false lambda x lambda y y mathbf K mathbf I mathbf F nbsp Sei nun Z C C B N S I I W I displaystyle Z mathbf C mathbf C mathbf B mathbf N mathbf S mathbf I mathbf I mathbf Omega mathbf I nbsp Untersuchen wir den Term S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp Hat S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp eine Normalform Falls ja mussen auch die folgenden Ableitungen eine Normalform haben S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp I Z I Z displaystyle mathbf I Z mathbf I Z nbsp Z I Z displaystyle Z mathbf I Z nbsp Z Z displaystyle Z Z nbsp C C B N S I I W I Z displaystyle mathbf C mathbf C mathbf B mathbf N mathbf S mathbf I mathbf I mathbf Omega mathbf I Z nbsp Definition von Z displaystyle Z nbsp C B N S I I W Z I displaystyle mathbf C mathbf B mathbf N mathbf S mathbf I mathbf I mathbf Omega Z mathbf I nbsp B N S I I Z W I displaystyle mathbf B mathbf N mathbf S mathbf I mathbf I Z mathbf Omega mathbf I nbsp N S I I Z W I displaystyle mathbf N mathbf S mathbf I mathbf I Z mathbf Omega mathbf I nbsp dd Nun wenden wir N displaystyle mathbf N nbsp auf S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp an Entweder hat S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp eine Normalform oder nicht Wenn ja dann ware N S I I Z W I displaystyle mathbf N mathbf S mathbf I mathbf I Z mathbf Omega mathbf I nbsp K W I displaystyle mathbf K mathbf Omega mathbf I nbsp Definition von N displaystyle N nbsp W displaystyle mathbf Omega nbsp dd aber W displaystyle mathbf Omega nbsp hat keine Normalform W displaystyle mathbf Omega nbsp haben wir durch Ableitungen aus S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp erhalten also hat auch S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp keine Normalform Dies ist ein Widerspruch Falls S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp keine Normalform hat reduziert sich der Term folgendermassen N S I I Z W I displaystyle mathbf N mathbf S mathbf I mathbf I Z mathbf Omega mathbf I nbsp K I W I displaystyle mathbf K mathbf I mathbf Omega mathbf I nbsp Definition von N displaystyle mathbf N nbsp I I displaystyle mathbf I mathbf I nbsp I displaystyle mathbf I nbsp dd was bedeutet dass S I I Z displaystyle mathbf S mathbf I mathbf I Z nbsp als Normalform einfach I displaystyle mathbf I nbsp hat also wieder ein Widerspruch Daher kann es keinen solchen Kombinator N displaystyle mathbf N nbsp geben Anwendungsgebiete BearbeitenUbersetzung funktionaler Programmiersprachen Bearbeiten Funktionale Programmiersprachen basieren haufig auf der einfachen aber universellen Semantik des Lambda Kalkuls David Turner benutzte CL fur die Sprache SASL Quellen Bearbeiten Uber die Bausteine der mathematischen Logik Moses Schonfinkel 1924 ubersetzt als On the Building Blocks of Mathematical Logic in From Frege to Godel a source book in mathematical logic 1879 1931 ed Jean van Heijenoort Harvard University Press 1977 ISBN 0 674 32449 8 Die Originalpublikation uber kombinatorische Logik Combinatory Logic Curry Haskell B et al North Holland 1972 ISBN 0 7204 2208 6 Eine umfassende Ubersicht 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 Sorensen 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 105Weblinks BearbeitenKatalin Bimbo Combinatory Logic In Edward N Zalta Hrsg Stanford Encyclopedia of Philosophy Normdaten Sachbegriff GND 4164750 6 lobid OGND AKS LCCN sh85028814 Abgerufen von https de wikipedia org w index php title Kombinatorische Logik amp oldid 238802404
