Eine Verwirrung über Churchs einfache Typentheorie und den Curry-Howard-Isomorphismus

Da DanielV und spaceisdarkgreen angeben, gibt es zwei Möglichkeiten, wie Sie den einfach typisierten Lambda-Kalkül verwenden können. Eine Möglichkeit besteht darin, sie als Beweistheorie über Aussagen-als-Typen (dh Curry-Howard) zu verwenden, die andere besteht darin, die Gleichungstheorie mit Lambda-Termen als Termen zu betrachten.

In der ersteren Sichtweise stellen wir uns einen Typ vor, der einen Satz darstellt, und dieser Satz hat genau dann einen Beweis, wenn es einen Lambda-Term dieses Typs gibt. Dies ist die Propositions-as-Types/Curry-Howard-Perspektive. Wir können beweisen, dass es eine Eins-zu-Eins-Entsprechung zwischen den Typen, Termen und Termreduktionen des einfach typisierten Lambda-Kalküls und den Aussagen, Beweisen für natürliche Deduktion und Beweisumschreibungen der Darstellung natürlicher Deduktion der minimalen/intuitionistischen Aussagenlogik gibt .$\beta$-Reduktion entspricht lokaler Solidität, und$\eta$-Erweiterung auf lokale Vollständigkeit.

In der letzteren Ansicht, die zB von der HOL-Familie der Theorembeweiser verwendet und in The Seven Virtues of Simple Type Theory beschrieben wird , sind die einfach typisierten Lambda-Terme nur Terme in einer Gleichungslogik. In diesem Fall ist ein Beweis ein Beweis in dieser Logik, der klassisch oder intuitionistisch oder was auch immer sein kann. Typischerweise ist es ein klassischer und ein boolescher Typ$\mathbb B$wird mit Axiomen hinzugefügt, um sicherzustellen, dass es nur zwei Werte hat,$\mathsf{F}$Und$\mathsf{T}$. Wir können dann Sätze mit Begriffen des Typs identifizieren$\mathbb B$, und allgemeiner, Prädikate mit Begriffen des Typs$(\tau_1\to(\tau_2\to\cdots(\tau_n\to\mathbb B)\cdots))$. Aufgrund der Verwendung von Termen höherer Ordnung (Lambda-Terme) erzeugen nur eine Handvoll Regeln und Axiome für Gleichheit und Boolesche Werte eine ziemlich mächtige Logik höherer Ordnung. Siehe die Abschnitte 2.3.1 und 2.4.3 des HOL4-Logikhandbuchs für Details des deduktiven Systems im Fall von HOL4 (das tatsächlich den polymorphen Lambda-Kalkül verwendet, nicht den einfach typisierten Lambda-Kalkül, da dies viel bequemer ist). In HOL4 wären die Beweise also Abzüge in diesem deduktiven System.

Zusammenfassend lässt sich sagen, dass es in der ersteren Sichtweise um willkürliche Aussagen geht und die Lambda-Terme Beweisen dieser Aussagen entsprechen. In der letzteren Ansicht dreht sich die Logik um Lambda-Terme, dh Sie beweisen Fakten über Lambda-Terme, zB ob zwei gleich sind.