Aufriß des Lambda-Kalküls (in Lisp-Notation)

Der Lambda-Kalkül als formallogische Abstraktion dessen, was Algorithmen sind, was sie leisten, wozu sie fähig sind und wozu nicht, bedient sich einer suggestiven Notation, die anders als die ebenso abstrakte Modellbildung durch die Turing-Maschine(n) alle algorithmischen Abläufe mathematisch-symbolisch (re‑)konstruiert, statt codierte Programme auf einer virtuellen Maschine (quasi‑)prozedural zu implementieren. Im Lambda-Kalkül wird der mathematische Kern von Algorithmen in die formale Symbolik selbst ‘eingelagert’ oder ‘eingebaut’, bei der Turing-Maschine wird der mathematische Sinn von Algorithmen in einen separaten Code ‘übertragen’ oder ‘übersetzt’. Es erinnert in gewisser Weise an die subtile, letztlich illusorische Differenz, wie sie zwischen einem Interpreter und einem Compiler entsteht, obwohl in beiden Fällen mit einer durchformalisierten Sprache gearbeitet wird, um ein ausführbares Programm zu schreiben. Die Modellierung abstrakter Strukturen durch den Lambda-Kalkül einerseits und durch die Turing-Maschine(n) andererseits erweckt den Eindruck, als sei, um es scholastisch auszudrücken, zwischen intentio recta und intentio obliqua zu unterscheiden. Wie gesagt, es handelt sich um eine Illusion, die allerdings alles andere als abwegig ist.

Wird von der üblichen Punkt-Notation des Lambda-Kalküls abgewichen, um sich den symbolischen Kalkül in Lisp-Notation anzusehen, hat das seinen eigenen Reiz, weil sich das funktionale/prozedurale Konzept in aller Unmittelbarkeit abzeichnet, wenn man mit Lisp oder Scheme vertraut ist. Daß sich die Lisp-Notation anbietet, um den Lambda-Kalkül, wie er von Alonzo Church konzipiert wurde, im Aufriß darzustellen, liegt daran, daß die Symbolik von Lisp (oder Scheme) eben daher stammt (mutatis mutandis). Es ergibt sich folgendes Bild:

Terme, Applikation und λ‑Abstraktion

  • Terme sind Variable wie a, b, c, … x, y, z, …, die als elementare Terme gelten, sowie
  • komplexe Terme der Gestalt (P Q) oder (λ (vQ), wobei P und Q (irgendwelche) Terme sind, und v (irgend‑) eine Variable ist.
  • Ein Term der Gestalt (P Q) heißt Applikation (des Operators P auf den Operanden Q).
  • Und ein Term der Gestalt (λ (vQ) heißt λ‑Abstraktion (oder einfach Abstraktion); wobei λ ein reserviertes Symbol des danach benannten Lambda-Kalküls ist.

Formeln

Als Formel gelten

  • Reduktion P → Q
  • Äquivalenz P = Q

wobei P und Q Terme sind.

Klammern (syntactic sugar)

  • Bei einer geschachtelten Applikation kann eine linksassoziative Klammerung unterdrückt und ein Term der Gestalt ((P QR) als (P Q R) geschrieben werden.
  • Eine geschachtelte Abstraktion der Gestalt (λ (u) (λ (vQ)) kann abgekürzt durch den Ausdruck (λ (u vQ) wiedergegeben werden, und entsprechend zu verstehen sind Ausdrücke wie (λ (u v wQ), (λ (u v w xQ) etc.

Freie vs. gebundene Variable

Eine Variable v, die im Term Q vorkommt, wird (darin) frei genannt, falls sie nicht im Geltungsbereich einer λ‑Abstraktion (λ (v) …) liegt, die einen (Sub‑) Term von Q bildet; andernfalls wird jene Variable als gebunden bezeichnet.

Umbenennung

Die Notation {y/x}Q steht für das Resultat einer (durchgängigen) Umbenennung der Variablen x in y innerhalb des Terms Q, egal ob sie darin frei oder gebunden vorkommt. Tritt die umzubenennende Variable im Term überhaupt nicht auf, bleibt er unverändert.

Substitution

Die Notation [P/x]Q repräsentiert das Resultat, das sich ergibt, wenn innerhalb des Terms Q die Variable x durch den Term P substituiert wird, und zwar überall wo sie darin frei vorkommt. Dabei dürfen allerdings keine freien Variablen des Terms P gebunden werden; zuvor sind deshalb im Term Q jene darin gebunden vorkommenden Variablen gleichen Namens auf geeignete Weise umzubenennen.

Axiome

  1. Q → Q
  2. Transitivität der Reduktion: mit P → Q und Q → R gilt P → R
  3. Mit P → Q gilt (R P) → (R Q)
  4. Mit P → Q gilt (P R) → (Q R)
  5. Mit P → Q gilt (λ (vP) → (λ (vQ)
  6. Reduktion bewahrt Semantik: mit P → Q gilt P = Q
  7. Kommutativität der Äquivalenz: mit P = Q gilt Q = P
  8. Transitivität der Äquivalenz: mit P = Q und Q = R gilt P = R
  9. Beta-Reduktion: ((λ (uQv) → [v/u]Q
  10. Eta-Reduktion: (λ (v) (Q v)) → Q, falls v in Q nicht frei vorkommt

Kalkulation als Reduktion

Unter einer Kalkulation ist eine Sequenz von Termen zu verstehen, die jeweils durch Reduktion auseinander hervorgehen, also etwa P → Q → R → S → T; wobei sich, abgesehen vom Term am Anfang, jeder weitere Term jener Sequenz reduktiv aus dem unmittelbar vorher­gehenden ergibt. Der vorangehende Term bei einer Reduktion wird Redex genannt, und der nachfolgende wird dann als Redukt bezeichnet.

Term vs. Form

Ein Term heißt Form, falls keine freien Variablen darin vorkommen.

Normalform

Ein Term ist in Normalform, falls er keine (Sub‑) Terme der Gestalt ((λ (vPQ) oder (λ (v) (Q v)) enthält. Und daß ein Term eine Normalform hat, heißt: Es gibt eine Kalkulation, die, ausgehend von jenem Term, mit einem Term in Normalform endet.

Church/Rosser-Theorem

Wenn P = Q für zwei Terme P und Q gilt, dann existiert ein Term R, so daß P → R und Q → R gilt.

Korollar:

Wenn ein Term eine Normalform hat, so ist diese eindeutig.

Wert

Die Normalform eines Terms ist als sein Wert zu betrachten. Daher ist, falls der Term überhaupt eine Normalform hat, sein Wert durch Kalkula­tion zu finden. Und jene Kalkulation bricht ab oder terminiert, sobald eine Normalform erreicht ist. Dagegen gibt es bei einem Term ohne Normal­form keine terminierende Kalkulation.

Term ohne Normalform

Wegen

((λ (v) (v v)) (λ (v) (v v)))

→ ((λ (v) (v v)) (λ (v) (v v)))

hat der Term ((λ (v) (v v)) (λ (v) (v v))) keine Normalform.

Fundamentale Definitionen

Identität

id := (λ (uu)

Wahrheitswerte

true := (λ (u vu)

false := (λ (u vv)

Logik-Operatoren

not := (λ (u) (u false true))

and := (λ (u v) (u (v true falsefalse))

or := (λ (u v) (u true (v true false)))

Listen-Operatoren

car := (λ (v) (v true))

cdr := (λ (v) (v false))

cons := (λ (u v w) (w u v))

Natürliche Zahlen

0 := id

n‘ := (cons n true)

Zählen mit Successor,  Predecessor,  Zero-Prädikator

succ := (λ (v) (cons v true))

pred := car

zerop := (λ (v) ((cdr vfalse true))

Dotted-Pair

(P . Q) := (λ (w) (w P Q))

Fixpunkt‑Theorem

Zu jedem Term F existiert ein Term X, Fixpunkt von F genannt, so daß (F X) = X gilt.

Fixpunkt‑Konstruktion

X = ((λ (v) (F (v v))) (λ (v) (F (v v))))

Fixpunkt‑Operator

fxpt := (λ (f v) (f (v v))) (λ (v) (f (v v)))

Exemplarische Kalkulationen

(true id) = false

(true id)

→ ((λ (u vuid)

→ (λ (vid)

→ (λ (v) (λ (ww))

→ (λ (v ww)

→ false

(true P Q) = P

(true P Q)

→ ((λ (u vuP Q)

→ P

(false P Q) = Q

(false P Q)

→ ((λ (u vvP Q)

→ Q

(not true) = false

(not true)

→ ((λ (w) (w false true)) true)

→ (true false true)

→ false

(not false) = true

 (not false)

→ ((λ (w) (w false true)) false)

→ (false false true)

→ true                                                                                                                                                                                (

(not (not true)) = true

(not (not true))

→ (not false)

→ true

(not (not false)) = false

(not (not false))

→ (not true)

→ false

(not not) = (λ (u v w) v)

(not not)

→ (λ (w) (w false true)) (λ (u) (u false true))

→ ((λ (u) (u false true)) false true)

→ ((false false truetrue)

→ (true true)

→ ((λ (x ux) (λ (v wv))

→ (λ (u) (λ (v wv))

→ (λ (u v wv)

(not not true) = true

(not not true)

→ ((λ (u v wvtrue)

→ (λ (v wv)

→ true

[!]    (not not false) = true

(not not false)

→ ((λ (u v wvfalse)

→ (λ (v wv)

→ true

Extensionalität

Seien f und g Funktionen (im mathematisch üblichen Sinne). Wenn f(x) = g(x) für alle x gilt, dann ist f = g.

Beweis (mittels Eta-Reduktion):

Angenommen (P x) = (Q x) gilt für einen Term x, der nicht als freie Variable in den Termen P und Q vorkommt, dann gibt es einen Term T, so daß:

(P x) → T und (Q x) → T

Also:

(λ (x) (P x)) → (λ (x) T)

(λ (x) (Q x)) → (λ (x) T)

(λ (x) (P x)) = (λ (x) T)

(λ (x) (Q x)) = (λ (x) T)

(λ (x) (P x)) = (λ (x) (Q x))

(λ (x) (P x)) → P

(λ (x) (Q x)) → Q

(λ (x) (P x)) = P

(λ (x) (Q x)) = Q

P = Q

Blockseminar zur Logik

Mein Blockseminar zur Logik im Institut für Philosophie der Universität Frankfurt findet von Montag bis Freitag ganztägig ab 09:00 Uhr, beginnend am 13.02.12, am Campus Westend statt. Die abschließende Klausur ist für den darauffolgenden Montag 20.02.12 angesetzt. Zur Teilnahme am Seminar ist keine Voranmeldung nötig. Der Raum wird kurzfristig im Aushang des Instituts bekanntgegeben.

Literatur: Richard C. Jeffrey (& George Boolos),  Formal Logic. Its Scope and Limits, 3rd Edition, New York, Cambridge 1990/2004, oder 4th Edition (by John P. Burgess) 2006.

Proseminar zur Formalen Logik

Mein Proseminar zur Formalen Logik findet in der Woche vom 21.02.11 – 25.02.11 täglich von 09:00 – 18:00 Uhr in Raum IG 0.457 am Campus Westend der Universität Frankfurt statt. Es ist keine Voranmeldung erforderlich. Die Klausur wird voraussichtlich am 28.02.11 um 17:00 Uhr geschrieben. Empfohlene Literatur: Richard C. Jeffrey (& George Boolos),  Formal Logic. Its Scope and Limits, 3rd Edition, New York, Cambridge 1990/2004, oder 4th Edition (by John P. Burgess) 2006.

Proseminar: »Logik«

Mein Proseminar zur »Logik« im Sommersemester 2010 findet als Blockveranstaltung vom 15.03.10 – 19.03.10 von 09:00 – 18:00 Uhr in Raum IG 0.454 am Campus Westend der Universität Frankfurt statt.

Wittgensteins N-Operator im »Tractatus«

In Wittgensteins »Tractatus logico-philosophicus« wird ein logischer Operator eingeführt, um die allgemeine Satzstruktur (in formallogischer Hinsicht) zu klären: der N-Operator. Es handelt sich um einen Operator, dessen Operanden (Aussage-) Sätze sind, Propositionen genannt, die einen von zwei Wahrheitswerten annehmen. Der Operator stellt eine Wahrheitsfunktion dar, das heißt eine Funktion (im mathematischen Sinne), welche in Abhängigkeit von den jeweiligen Wahrheitswerten ihrer Argumente ebenfalls Wahrheitswerte als Funktionswerte liefert. Aber anders als übliche Funktionen mit fester Stellenzahl ist der N-Operator für eine beliebige Stellenzahl erklärt. Er wirkt nämlich als monadischer, als dyadischer, als triadischer etc. Operator, je nachdem welche Anzahl von Operanden auftritt, fungiert also für n Operanden als n-adischer oder n-stelliger Operator. Aus technischer Sicht der digitalen Schaltalgebra liegt der Typus des NOR-Gatters (NOR gate) mit variabler Anzahl von Anschlüssen für den Input vor, wobei mit NOR gemeint ist, daß die (kombinierte) Operation »not-or« ausgeführt wird. Der Output eines ähnlichen Schaltkreises, des NAND-Gatters (NAND gate), wird erzeugt, indem der anstehende Input gemäß der Operation »not-and« umgewandelt und anschließend ausgegeben wird, wobei beide Gatter die Negation »not« erst nach der logischen Verknüpfung der Eingangssignale gemäß der Disjunktion »or« beziehungsweise der Konjunktion »and« vornehmen. Wollte man digitale logische Schaltungen auf einen einzigen Typus von vorgefertigen Schaltkreisen reduzieren, wäre jeder der beiden logischen Bausteine geeignet, sämtliche anderen Typen zu ersetzen. In der formalen Logik läßt sich für den Fall von zwei Operanden die Wirkung des NOR-Gatters durch den Peirce-Pfeil symbolisieren, während dem NAND-Gatter das Symbol des Sheffer-Strichs entspricht. Beide werden definiert als:

Peirce-Pfeil + Sheffer-Strich

Die genannten Operatoren sind dual zueinander. Sie waren Peirce (um 1880) beide bekannt, und er wußte auch was von Sheffer (1913) bewiesen wurde, daß nämlich die logischen Operationen in der Boolschen Algebra auf einen von beiden zurückführbar sind. Im »Tractatus« (1921) knüpft Wittgenstein an Sheffer an, Peirce hatte seine eigenen Ergebnisse nicht veröffentlicht, doch benannt ist der betreffende Operator inzwischen nach Peirce, nicht nach Sheffer.

In Form des N-Operators wird der Peirce-Pfeil verallgemeinert, indem keine bestimmte Anzahl von Operanden in dessen Definition angegeben wird: Es werde als Resultat der Operation der Wahrheitswert »falsch« geliefert, wenn und nur wenn mindestens einer der Operanden den Wert »wahr« annimmt, andernfalls sei das Resultat »wahr«. Dies charakterisiert den N-Operator in seiner Wirkung, ohne seine Anwendung an irgendeine feste Stellenzahl zu koppeln. Insofern egeben sich folgende logische Äquivalenzen:

N-Operator #1

Anhand des N-Operators lassen sich sämtliche logischen Junktoren einführen oder nachbilden, ob einstellig oder mehrstellig, wie Negator, Konjunktor, Disjunktor oder Adjunktor, Konditional, Bikonditional oder Äquivalenz etc. Unter einer Junktorenbasis ist eine Auswahl von Junktoren zu verstehen, mittels derer sämtliche anderen Junktoren definierbar sind. Solche Mengen von Junktoren werden als funktional vollständig bezeichnet. Beispielsweise bilden die beiden Junktoren der Negation und des Konditionals (materiale Implikation) eine Junktorenbasis, ebenso die Negation gemeinsam mit der Konjunktion oder der Disjunktion. Eine Junktorenbasis bildet auch der Peirce-Pfeil allein, ebenso der Sheffer-Strich allein. Wie sich der N-Operator dazu eignet, andere Junktoren zu definieren oder zu emulieren, zeigt sich an folgenden Entsprechungen:

N-Operator #2

Auf ähnliche Weise sind sämtliche weiteren n-adischen Operatoren der Junktorenlogik definierbar. Dasselbe ist mittels des Peirce-Pfeils oder des dazu dualen Sheffer-Strichs erreichbar, allerdings weisen beide eine feste Stellenzahl auf, was bei Wittgensteins N-Operator eben vermieden wird. Weniger elegant, doch nicht weniger allgemein wäre es, statt Wittgensteins N-Operator einen jener beiden zueinander dualen Operatoren zu wählen. Übrigens gehört zu Wittgensteins N-Operator ebenfalls ein dualer, der als solcher den Sheffer-Strich anstelle des Peirce-Pfeils verallgemeinert. In der Schaltalgebra entspricht, wie gesagt, dem Peirce-Pfeil ein NOR-Gatter und dem Sheffer-Strich ein NAND-Gatter, jeweils mit zwei Eingängen. Werden die beiden Eingänge leitend miteinander verbunden, das heißt kurzgeschlossen, so wirkt sowohl das NOR als auch das NAND-Gatter wie ein Inverter, welcher die Negation des digitalen Eingangssignals liefert, denn es gelten die Äquivalenzen:

Negation

In den angegebenen Formeln zeichnet sich ab, inwiefern im Rekurs auf den N-Operator von Wttgenstein die beabsichtigte strukturelle Vereinheitlichung verschachtelter Junktoren erzielbar ist, um die formale Diversität logischer Operatoren auf einen einzigen Operationstyp zu reduzieren. Wenn die Bedeutung eines Satzes nicht von oberflächlichen Umformungen beinflußt wird, sondern allein von dessen Wahrheitsbedingungen abhängt, wobei letztere in logischen Operatoren codiert sind, dient es der formalen Einheitlichkeit und Durchsichtigkeit, wenn auch nicht der Bequemlichkeit, eine einzige logische Operation als fundamental auszuzeichnen und andere Operationen dadurch auszudrücken. Ohne eine gewisse Konvergenz der komplexen Formen gleichbedeutender Propositionen ergäbe sich kein Anhaltspunkt, an dem so etwas wie eine allgemeine Satzform festzumachen wäre.

(Copyright by Peter Gold)

Kausalität laut Aristoteles’ Physik

Bedenkt man, daß aitia neben ‘Ursache’, ‘Grund’ oder ‘Anlaß’ auch ‘Schuld’ bedeutet (aitios = schuldig, schuld, verantwortlich; der Schuldige, Urheber, Täter), so zielt die Frage nach Kausalität darauf ab, zu erfahren, was an etwas ‘schuld’ ist.

Um die von Aristoteles unterschiedenen ‘Ursachen’, nach denen gefragt werden kann, zu typisieren, ohne sie zu verdinglichen, ist es am besten, die Frage so neutral wie möglich zu formulieren:

Was (alles) ist schuld daran, daß etwas (ein Ding) das ist, was es ist, und daß es so ist, wie es ist?

Wird nach diesem Schema gefragt, wobei das Wort ‘Ursache’ nicht unabsichtlich vermieden wird, werden die Antworten unter vier verschiedenen Aspekten erfolgen, je nachdem, worauf Bezug genommen wird:

  1. causa materialis: das Material, aus dem etwas besteht (woraus ist das Ding gemacht?)
  2. causa formalis: die Form, die etwas aufweist (wie ist das Ding geformt?)
  3. causa efficiens: die Weise, wie etwas entstanden ist (wie ist das Ding zu diesem Ding geworden?)
  4. causa finalis: der Zweck, den etwas erfüllt (wozu ist das Ding gedacht?)

Statt nach einem ‘Ding’ oder einem ‘Gegenstand’ kann auch nach einer ‘Sache’ gefragt werden, oder neutraler nach einer Entität, nach irgendetwas. Eine ‘Ursache’ ist nun nicht ihrerseits eine ‘Sache’ oder ein ‘Ding’ im selben Sinne, sondern sie ist auch nur – irgendetwas.

(Copyright by Peter Gold)

Seminar: »Formale Logik«

Mein Seminar zur Einführung in die »Formale Logik« im Sommersemester 2009 findet vom 16.03.09 bis 20.03.09 um 09:00-18:00 Uhr am Campus Westend im Hörsaal IG 457 der Universität Frankfurt statt. Behandelt wird die Junktoren- und Quantoren-Logik. Es ist keine Voranmeldung zur Teilnahme an der Lehrveranstaltung erforderlich. Den Abschluß des Blockseminars bildet eine Klausur, die voraussichtlich nachmittags am 23.03.09 geschrieben wird.