- Alonzo Church ist zwar weit weniger bekannt als Alan Turing, war aber der Logiker, der mit dem λ-Kalkül und der Theorie der Berechenbarkeit die logischen Grundlagen des Computings legte
- Die Church-Turing-These von 1936 lieferte den Rahmen dafür, dass effektiv berechenbare Funktionen von einer Turing machine oder einem dazu äquivalenten System berechnet werden können
- Als Antwort auf Hilberts Entscheidungsproblem zeigte er, dass es keinen entscheidenden Algorithmus gibt, der alle mathematischen Aussagen beurteilen kann, und machte damit die Grenzen der Berechnung deutlich
- In Princeton betreute er unter anderem Stephen Kleene, J. Barkley Rosser und Alan Turing; Turing schloss unter Churchs Betreuung seinen Ph.D. ab
- Seine abstrakte Arbeit lebt in der Genealogie des Computings fort, die zu modernen Compilern, Interpretern, funktionaler Programmierung, Smartphone-Apps und KI reicht
Größerer theoretischer Einfluss als öffentliche Bekanntheit
- Alan Turing wird in der populären Geschichte von Computing und künstlicher Intelligenz wegen des Turing Test häufiger erwähnt, doch Church war eine Person, die Turings Denken und Arbeit stark beeinflusste
- Churchs Arbeit bildete eine wichtige Grundlage dafür, zu verstehen, was Berechnung ist, und die Konzepte zu formen, mit denen KI bewertet wird
- Ohne Churchs Beiträge hätten sich auch die heutigen Vorstellungen von künstlicher Intelligenz und ihrer Bewertung deutlich anders entwickeln können
Leben und wissenschaftliche Prägung
- Church war ein stiller, wortkarger Logiker, geboren am 14. Juni 1903 in Washington, D.C.
- Es gibt Berichte, dass er in seiner Kindheit durch einen Unfall mit einem Luftgewehr auf einem Auge erblindete oder teilweise sein Sehvermögen verlor
- Nach dem Abschluss einer preparatory school in Connecticut im Jahr 1920 begann er noch im selben Jahr sein Studium in Princeton und beendete 1927 seine Promotion
- Nach Aufenthalten als National Research Fellow in Harvard, Göttingen und Amsterdam kehrte er nach Princeton zurück und erarbeitete dort einen großen Teil seiner wissenschaftlichen Leistungen
- Er war bekannt für seine ordentliche Tafelschrift und seine akribische Art und überzog wichtige Manuskripte sogar mit Duco cement, um sie zu konservieren
λ-Kalkül und Berechenbarkeit
- Churchs tiefgreifendster Beitrag war das λ-Kalkül, das schon vor der Prägung des Begriffs Informatik zu deren Grundlage wurde
- 1936 formulierte Church die Church-Turing-These, ein zentrales Konzept der theoretischen Informatik
- Effektiv berechenbare Funktionen können von einer Turing machine oder einem dazu äquivalenten System berechnet werden
- Sie bietet einen Rahmen, um zu verstehen, was Maschinen theoretisch leisten können
- Zugleich macht sie die Grenzen sichtbar, an die algorithmische Verfahren stoßen
- Die These ist ein grundlegendes Konzept, lässt aber weiterhin Diskussionen und Grenzen rund um die Auslegung von „effective computability“, physische Berechnung und das Wesen menschlicher Intelligenz offen
- Wenn Turing mit der Turing machine ein Modell vorschlug, das mechanische Verfahren in logische Form überführt, dann lieferte Church die reine Abstraktion, die solche Maschinen theoretisch untermauerte
Moderne Programmierung und funktionales Denken
- Der Einfluss des λ-Kalküls zeigt sich noch heute in den Prinzipien der Softwareentwicklung und ist mit Komposition, Higher-Order Functions und der Betonung von Immutability verbunden
- Dieses formale System machte es möglich, abstrakte mathematische Probleme in Code zu fassen und mechanisch zu lösen, und wurde zur Grundlage moderner Compiler- und Interpreter-Architekturen
- Für heutige Programmierer kann das λ-Kalkül wie eine Menge verschachtelter Funktionen erscheinen, wie man sie in einigen Paradigmen von Lisp, Haskell, Python oder JavaScript sieht
- Die Abstraktion des λ-Kalküls bildet die Grundlage der funktionalen Programmierung, in der Funktionen als First-Class Citizens behandelt werden
Entscheidungsproblem und die Grenzen der Berechnung
- Church leistete auch in anderen Bereichen von Logik und Philosophie wichtige Beiträge; ein repräsentatives Beispiel ist seine Arbeit zum Entscheidungsproblem
- Das Entscheidungsproblem war die von David Hilbert 1928 formulierte Frage, ob es einen entscheidenden Algorithmus gibt, der den Wahrheitswert jeder mathematischen Aussage bestimmen kann
- Church gab darauf eine negative Antwort: Ein solcher Algorithmus existiert nicht; dieses Ergebnis ist als Church's Theorem bekannt
- Diese Entdeckung beeinflusste die Entscheidungstheorie tiefgreifend und betonte die Grenzen dessen, was allein durch Berechnung erreichbar ist
Das intellektuelle Zentrum von Princeton und seine Schüler
- Church war ein Mentor, der bedeutende Logiker und Informatiker seiner Zeit betreute
- Zu seiner wissenschaftlichen Linie gehören Stephen Kleene, J. Barkley Rosser und Alan Turing
- Turing schloss in Princeton unter Churchs Betreuung seinen Ph.D. ab
- David Kaplan soll neuen Graduate-Studierenden empfohlen haben, Churchs Lehrveranstaltungen zu besuchen, und gesagt haben, es werde selbst dann eine Erfahrung sein, von der man später den Enkeln erzählen werde, wenn sie nicht zum eigenen Fachgebiet gehöre
- Princeton war in den 1930er Jahren mit John von Neumann, Kurt Gödel und Church ein intellektuelles Zentrum der Entwicklung moderner Logik
Ein wenig sichtbares Vermächtnis
- Church erreichte nie denselben Grad an öffentlicher Bekanntheit wie Turing, von Neumann oder Gödel
- Sein Vermächtnis war nicht von der Art, die die öffentliche Vorstellungskraft leicht fesselt, wie Heldengeschichten aus der Kriegszeit der Kryptanalyse oder die Tragik eines frühen Todes
- Die Milliarden Programme, die auf Smartphones laufen, können ihre Logik bis zu den abstrakten Funktionen des λ-Kalküls zurückverfolgen
- Von einfachen Apps bis hin zu künstlicher Intelligenz trägt die unsichtbare DNA der Berechnung eine wesentliche Linie von Churchs Arbeit in sich
- Churchs Genialität lag nicht im Spektakel, sondern in der strengen Struktur und stillen Eleganz, die die Welt veränderten
1 Kommentare
Hacker-News-Kommentare
Mir gefiel die Herkunft des Namens lambda, wie sie in Paradigms of Artificial Intelligence Programming (PDF/EPUB: https://github.com/norvig/paip-lisp) beschrieben wird
Demnach verschob Alonzo Church das Zirkumflex, das in der Notation von Russell und Whiteheads Principia Mathematica über gebundenen Variablen stand, etwa
x̂(x + x), nach vorne, um daraus eine eindimensionale Zeichenkette zu machen:^x(x + x). Da ein leeres Zirkumflex merkwürdig aussah, ersetzte er es durch ein großes LambdaΛx(x + x), das später zur Vermeidung von Verwechslungen zu einem kleinenλx(x + x)wurdeJohn McCarthy war in Princeton Schüler von Church und verwendete 1958 bei der Entwicklung von Lisp
(lambda (x) (+ x x)), weil es auf den damaligen Lochkartenstanzen keine griechischen Zeichen gab; das hat sich bis heute gehaltenDeshalb taucht Church, wie das Thema dieses Artikels andeutet, in Rückblicken auf Lisp häufig auf und kann nur für Menschen eine „vergessene“ Figur sein, die sich kaum für Computergeschichte interessieren
Laut Dana Scott sagte Church selbst, die Wahl sei eher eine willkürliche Entscheidung im Stil von „eeny, meeny, miny, moe“ gewesen, und auch die Erklärung nach Barendregt sei in einem neueren Vortrag an der University of Birmingham zurückgewiesen worden
Im französischsprachigen Raum bedeutet „personne lambda“ gewöhnlich eine durchschnittliche Person oder einen Unbekannten, was gut zu anonymen Funktionen passt; außerdem bedeutet das Adjektiv lambda auch „allgemein/gewöhnlich“, sodass ein Buchstabe aus der Mitte des griechischen Alphabets etwas Durchschnittliches zu bezeichnen scheint
https://math.stackexchange.com/questions/64468/why-is-lambda...
Es behandelt viele Programmier-Themen und eröffnet auch Paradigmen, die für Menschen mit wenig Berührung zu funktionaler Programmierung ungewohnt sein können
Einen weiteren Hinweis darauf, dass Churchs Wahl eher eine willkürliche Auswahl unter griechischen Buchstaben als mit einer bestimmten Bedeutung verbunden war, gibt es hier: https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_...
Mich würde auch interessieren, ob das vor oder nach McCarthys Beginn mit Lisp war
„Churchs Lambda-Kalkül und Turing-Maschinen sind rechnerisch gleich mächtig, aber Turing-Maschinen unterscheiden sich dadurch, dass sie veränderlichen Zustand verwenden. Dass es bis heute eine Kluft zwischen funktionalen und imperativen Sprachen gibt, liegt an der Trennung von Church und state“
Dieses Zitat kenne ich schon lange, aber ich kann die ursprüngliche Quelle nicht finden
Bearbeitung: Möglicherweise stammt es von Guy Steele: „Es gibt Leute, die den funktionalen, lambda-kalkülartigen Teil einer Sprache und den Teil, der Nebenwirkungen verursacht, nicht vermischen wollen. Sie scheinen an die Trennung von Church und state zu glauben.“
Das Originalarchiv ist hier: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
Europäer sprechen seinen Namen im Allgemeinen korrekt als „Nick-louse Veert“ aus, während Amerikaner ihn zu „Nickel's Worth“ verunstalten
Mit anderen Worten: Europäer nennen ihn beim Namen, Amerikaner beim Wert
https://en.m.wikiquote.org/wiki/Niklaus_Wirth
Wer einen wirklich erstaunlichen Text über Church lesen möchte, dem empfehle ich Rotas Erinnerungen
Es ist der erste Abschnitt von https://www34.homepage.villanova.edu/robert.jantzen/princeto...
Verwandte Links: Alonzo Church, 92, Theorist of the Limits of Mathematics (1995) - https://news.ycombinator.com/item?id=12240815 - August 2016, sowie Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - Februar 2015
Das ganze Buch ist lesenswert
Die nach ihm benannte Programmiersprache Alonzo ist fast vergessen
https://dl.acm.org/doi/pdf/10.1145/68127.68139
Besonders die Logikphilosophie und die Theorie von Sinn/Bedeutung und Referenz, die an die Arbeiten von Frege und Russell anknüpfen, sind weitgehend in Vergessenheit geraten.
Church hat zu diesem Thema viele Aufsätze veröffentlicht, aber an Orten wie Wikipedia wird das kaum behandelt.
Der Eintrag in der Stanford Encyclopedia of Philosophy ist immerhin etwas besser: https://plato.stanford.edu/entries/church/
Allerdings habe ich gehört, dass auch dort einige seiner wichtigsten Arbeiten fehlen; vermutlich war er für Mathematiker zu philosophisch und für Philosophen zu technisch.
Das ist nicht der Kernpunkt, aber ich fände es besser, bei Blogbeiträgen etwas zurückhaltender mit KI-generierten Illustrationen umzugehen.
Es gibt echte Fotos von Church, die sogar gemeinfrei sind, und diese Illustration sieht ihm nicht einmal besonders ähnlich; da der Artikel an Popularität gewinnt, taucht sie inzwischen schon in der Bildersuche auf.
Wenn eine Illustration nicht einmal die mehr als 5 Minuten wert ist, die ihre Erzeugung gekostet hat, wäre es dann nicht besser, sie einfach wegzulassen?
Wenn man dennoch unbedingt ein von „KI“ erzeugtes Bild verwenden will, sollte es zumindest entsprechend beschriftet werden.
Ich wollte ungern einfach ein Online-Foto übernehmen, und dieses Bild war das siebte Ergebnis, das ich erzeugt habe, damit es nicht zu sehr wie ein „falsches“ Lookalike wirkt; ich fand, dass es ihm einigermaßen ähnlich sah.
Das Bild von JvN ist ziemlich gut gelungen, aber künftig ist es wohl richtiger, statt eines falschen personenähnlichen Porträts eher ein symbolisches Bild zu verwenden.
Die Formulierung „Architekt der Computerintelligenz“ scheint mir übertrieben.
Dass Church ein herausragender Logiker war, steht außer Frage, aber wenn mit Computerintelligenz hier AI/ML gemeint ist, dann hat er dazu faktisch nichts beigetragen.
Unabhängig davon bin ich mir nicht sicher, ob der Lambda-Kalkül überhaupt wirklich Mathematik ist; er wirkt eher wie eine clevere Notation.
Die Vorzüge einer Notation sind subjektiv, und interessant ist auch, dass Church selbst offenbar wenig Interesse daran hatte, dass seine Ideen das Design bestimmter Programmiersprachen inspirierten.
STT wird oft auch mit Logik höherer Ordnung gleichgesetzt, weil sich mit den beiden primitiven Typen grundlegender „Objekte“ und Wahrheitswerte T/F sowie dem Funktionstyp
(a --> b)beliebige logische Objekte ausdrücken lassen.STT ist eindeutig eine Erfindung Churchs, hat moderne Typentheorien stark beeinflusst und auch Programmiersprachen mit komplexen Typsystemen wie Haskell geprägt.
Ich kann das nicht vollständig begründen, aber intuitiv scheint es so, dass Turing und das, wofür er steht, im Bereich KI am Ende hoch geschätzt werden, während es bei Church eher umgekehrt ist.
Der eine begann bei Reinheit, minimalen Voraussetzungen und abstrakter, „reiner“ Berechnung, der andere schien sich eher dafür zu interessieren, wie wir tatsächlich denken können, und kümmerte sich mehr um die Erweiterung von Ausdruck und Abstraktion als um die Implementierung.
Church hatte keine praktische Erfahrung mit Computern und war eher darauf ausgerichtet, die mathematische Theorie selbst zu erweitern.
Ihre Zusammenarbeit und die Kommunikation über den Atlantik hinweg verbanden Praxis und Theorie und festigten zentrale Konzepte wie die Dualität von imperativ und funktional, das Church-Turing-Theorem sowie den Zusammenhang zwischen Halteproblem und Churchs Theorem.
Es als Rivalität zu sehen, ist falsch, und die Rede von den „zwei Vätern“ der Informatik ist aus mehreren Gründen passend.
Besonders wenn man an Turings Tod denkt, gilt das umso mehr.
Außerdem darf man nicht weglassen, dass Turing nicht etwa kein Interesse an der Implementierung hatte, sondern zur praktischen Umsetzung zurückkehren wollte und daran gehindert wurde.
Es bleibt eine große Tragödie und eine offene Frage, was anders gewesen wäre, wenn die Geheimhaltungseinstufung der britischen Regierung anders ausgefallen wäre; zugleich hätten wir dann in unserer Zeitlinie womöglich die Zusammenarbeit mit Church verloren, die die Theorie so wirkungsvoll gefestigt hat.
Es war ein Glück, Alonzo Church und Haskell Curry im August 1982 beim ACM Symposium on LISP and Functional Programming an der CMU treffen zu können.
Curry war eindeutig gesundheitlich angeschlagen und starb etwa zwei Wochen nach der Konferenz, aber Church wirkte gesund und lebte danach noch ungefähr 13 Jahre.
Beim Empfang war Gerry Sussman sehr aufgeregt, als er durch den Raum ging und die beiden vorstellte, und auch für uns war es zutiefst bewegend, ihnen zu begegnen.
Einer von Churchs großen Beiträgen waren seine Schüler.
Aus einem einzigen Ort kamen erstaunlich viele bemerkenswerte Denker hervor.