Le combinateur Y contredit-il la correspondance Curry-Howard?

Le combinateur Y a le type . Par la correspondance de Curry-Howard, parce que le type est habité, il doit correspondre à un vrai théorème. Cependant est toujours vrai, il semble donc que le type du combinateur Y corresponde au théorème , qui n'est pas toujours vrai. Comment se peut-il?$(a \rightarrow a) \rightarrow a$$(a \rightarrow a) \rightarrow a$$a \rightarrow a$$a$

La correspondance originale de Curry-Howard est un isomorphisme entre la logique propositionnelle intuitionniste et le calcul lambda simplement typé.

Il existe, bien sûr, d'autres isomorphismes de type Curry-Howard; Phil Wadler a souligné que le nom à double canon "Curry-Howard" prédit d'autres noms à double canon comme "Hindley-Milner" et "Girard-Reynolds". Ce serait drôle si "Martin-Löf" était l'un d'eux, mais ce n'est pas le cas. Mais je m'égare.

Le combinateur Y ne contredit pas cela, pour une raison clé: il n'est pas exprimable dans le calcul lambda simplement tapé.

En fait, c'était tout le problème. Haskell Curry a découvert le combinateur de points fixes dans le calcul lambda non typé et l'a utilisé pour prouver que le calcul lambda non typé n'est pas un système de déduction solide.

Fait intéressant, le type de Y correspond à un paradoxe logique qui n'est pas aussi connu qu'il devrait l'être, appelé paradoxe de Curry. Considérez cette phrase:

Si cette phrase est vraie, alors le Père Noël existe.

Supposons que la phrase soit vraie. Alors, clairement, le Père Noël existerait. Mais c'est précisément ce que dit la phrase, donc la phrase est vraie. Par conséquent, le Père Noël existe. QED

Le Curry-Howard relie les systèmes de type aux systèmes de déduction logique. Entre autres, il cartographie:

• programmes aux épreuves
• évaluation de programme à transformations sur preuves
• types habités à de vraies propositions
• systèmes de type en systèmes de déduction logique

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

La correspondance Curry-Howard n'est que cela: une correspondance. En soi, cela ne dit pas que certains théorèmes sont vrais. Il dit que la typabilité / prouvabilité se porte d'un côté à l'autre.

La correspondance de Curry-Howard est utile comme outil de preuve avec de nombreux systèmes de types: calcul lambda simplement tapé, système F, calcul de constructions, etc. Tous ces systèmes de types ont la propriété que la logique correspondante est cohérente (si les mathématiques usuelles sont cohérentes) ). Ils ont également la propriété de ne pas autoriser la récursivité arbitraire. La correspondance Curry-Howard montre que ces deux propriétés sont liées.

Le Curry-Howard s'applique toujours aux calculs dactylographiés sans terminaison et aux systèmes de déduction incohérents. Ce n'est tout simplement pas particulièrement utile là-bas.