Widerspricht der Y-Kombinator der Curry-Howard-Korrespondenz?

Der Y-Kombinator hat den Typ . Nach der Curry-Howard-Entsprechung muss der Typ einem wahren Theorem entsprechen, da er bewohnt ist. Jedoch ist immer wahr, so dass es so aussieht, als ob der Typ des Y-Kombinators dem Satz , was nicht immer wahr ist. Wie kann das sein?$(a \rightarrow a) \rightarrow a$$(a \rightarrow a) \rightarrow a$$a \rightarrow a$$a$

Die ursprüngliche Curry-Howard-Entsprechung ist ein Isomorphismus zwischen der intuitionistischen Aussagenlogik und dem einfach typisierten Lambda-Kalkül.

Es gibt natürlich auch andere Curry-Howard-ähnliche Isomorphismen; Phil Wadler wies darauf hin, dass der doppelte Name "Curry-Howard" andere doppelte Namen wie "Hindley-Milner" und "Girard-Reynolds" vorhersagt. Es wäre lustig, wenn "Martin-Löf" einer von ihnen wäre, aber das ist es nicht. Aber ich schweife ab.

Der Y-Kombinator widerspricht dem nicht, und zwar aus einem wichtigen Grund: Er ist in der einfach typisierten Lambda-Rechnung nicht ausdrückbar.

Tatsächlich war das der springende Punkt. Haskell Curry entdeckte den Fixpunkt-Kombinator im untypisierten Lambda-Kalkül und verwendete ihn, um zu beweisen, dass der untypisierte Lambda-Kalkül kein Schalldämpfungssystem ist.

Interessanterweise entspricht der Typ von Y einem logischen Paradoxon, das nicht so bekannt ist, wie es sein sollte, und das als Currys Paradoxon bezeichnet wird. Betrachten Sie diesen Satz:

Wenn dieser Satz wahr ist, existiert der Weihnachtsmann.

Angenommen, der Satz wäre wahr. Dann würde der Weihnachtsmann eindeutig existieren. Aber das ist genau das, was der Satz sagt, so dass der Satz ist wahr. Daher existiert der Weihnachtsmann. QED

Das Curry-Howard-Verfahren bezieht Typsysteme auf logische Abzugssysteme. Es bildet unter anderem ab:

• Programme zu Beweisen
• Programmauswertung zu Transformationen auf Proofs
• bewohnte Typen zu wahren Sätzen
• Typsysteme zu logischen Abzugssystemen

$a \to b$$a$$b$$Y (\lambda x. x) \to Y (\lambda x.M)$

Die Curry-Howard-Korrespondenz ist genau das: eine Korrespondenz. An sich sagt es nicht, dass bestimmte Theoreme wahr sind. Sie besagt, dass Typisierbarkeit / Beweisbarkeit von einer Seite zur anderen geht.

Die Curry-Howard-Korrespondenz eignet sich als Beweismittel für viele Typensysteme: einfach eingegebene Lambda-Rechnung, System F, Konstruktionsrechnung usw. Alle diese Typensysteme haben die Eigenschaft, dass die entsprechende Logik konsistent ist (sofern die üblichen mathematischen Regeln konsistent sind) ). Sie haben auch die Eigenschaft, keine willkürliche Rekursion zuzulassen. Die Curry-Howard-Entsprechung zeigt, dass diese beiden Eigenschaften zusammenhängen.

Der Curry-Howard gilt immer noch für nicht terminierende typisierte Kalküle und inkonsistente Abzugssysteme. Es ist dort einfach nicht besonders nützlich.