Lambda -Kalkül als Typtheorie

Question

Aus dem Abschnitt "Einführungsabschnitt des Homotopy Type Theory Theory Book":

Die Typentheorie wurde ursprünglich von Bertrand Russell erfunden ... es wurde später als eigenständiges formales System entwickelt (unter dem Namen "$ lambda $ -Calculus").

Kann mir jemand diesen Satz erklären? Ich habe Probleme, $ lambda $ -Calculus als Typsystem zu sehen.

(Auch im selben Absatz, $ lambda $ -Calculus als "Kirchentypsystem" bezeichnet))

Answer 1

Im nächsten Absatz dieses Buches (siehe Hott, p. 2) Sie geben eine informelle Charakterisierung dessen, was ein Sprachsystem (oder eine Logik) als Typsystem qualifiziert, nämlich das: In all den Begriffen werden getippt.

Nach "Kirchentypsystem" beziehen sie sich auf die Einfach tippte Lambda -Kalkül (1940 eingeführt).

Insbesondere in den 1930er Jahren hatte Church während der Vorbereitung seiner negativen Lösung für das Entscheidungsproblem ein System von eingeführt Untyped Lambda Calculus. Dies war natürlich nicht eine Typtheorie.

Das System von 1940 ist jedoch eine Typtheorie, da alle Begriffe getippt werden (siehe zum Beispiel (T & S) Abschnitt 1.2, wie genau dies getan wird). Von "lambda-calculus als Typsystem" beziehen sie sich auf diese zweite, einfach typisierte Version von Lambda Calculus.

(T & S) Troelstra, AS & Schwichtenberg, H. Grundlegende Beweistheorie, 1996.