Der einfach getypte Lambda-Kalkül

Der einfach getypte Lambda-Kalkül (simply typed lambda-calculus) wurde von Alonso Church (1940) und Haskell Curry (1958) entwickelt. Er erweitert den ungetypten Lambda Kalkül um Typen, die über die Typrelation mit den Termen in Beziehung stehen. Da bereits der ungetypte Lambda-Kalkül turing-mächtig ist, ist nicht zu erwarten, dass die Einführung von Typen die Berechnung zusätzlicher Funktionen ermöglicht. Stattdessen ist die Einführung von Typen hauptsächlich durch folgende Aspekte motiviert: Für die Praxis am bedeutsamsten ist die automatisierte, statische Fehlererkennung, die durch Typisierung ermöglicht wird. So können Laufzeitfehler auf ein Minimum reduziert werden und bedeutungslose Terme, wie etwa die Summe aus einer Zahl und einem booleschen Wert, frühzeitig abgefangen werden. Deswegen kommen heutzutage bei größren Softwareprojekten fast ausschließlich Programmiersprachen mit einer entsprechenden Typisierung zum Einsatz. Zwar ist der Lambda-Kalkül keine in der Praxis eingesetzte Programmiersprache, jedoch basieren praxisrelevante funktionale Programmiersprachen wie ML oder Haskell und deren Typsysteme auf dem getypten Lambda-Kalkül. Historisch gesehen war die Einführung von Typen dem Anliegen Churchs geschuldet, den Lambda-Kalkül zur Kodierung und Berechnung logischer Aussagen zu verwenden. [...]