Faute de frappe dans le calcul des papiers de construction?

10

Dans le papier classique du calcul des constructions , il y a une règle qui dit

entrez la description de l'image ici (page 7 du pdf, page 101 du document original)

Cette règle signifierait que tout contexte est réductible à un membre de ce contexte. Il semble que cela ne devrait pas être correct, car cela impliquerait

1 ≅ Nat
3 ≅ Nat
1 ≅ 3

si Nat est un contexte.

Je pense que la meilleure interprétation est que le delta inférieur était censé être un M. Surtout compte tenu des règles données à la page suivante.

Est-ce simplement une faute de frappe ou une règle logique subtile que je ne comprends pas?

lo.logic calculus-of-constructions sequent-calculus user833970
la source

Réponses:

11

Vous avez raison, il y a une erreur dans cet article et la règle doit en effet se lire:

Γ⊢M:ΔΓ⊢M≅M

l'utilisation de jugements de ce style pour l'égalité (parfois appelée "égalité typée") trouve déjà son origine chez Martin-Löf, je pense (voir ici par exemple). Elle est souvent remplacée par une définition opérationnelle non typée dans les traitements modernes, où il n'y a pas de jugement de la forme , et la conversion est définie en termes bruts.Γ⊢N≅M

Un peu contre-intuitivement, prouver que le système avec conversion typée est équivalent à celui sans types est très difficile, et a été réglé en 2010 par Siles et Herbelin .

cody
la source
«Traitements modernes» signifie ici «traitements de compétence informatique qui s'intéressent principalement au calcul».
Andrej Bauer
C'est suffisant. J'ai presque évoqué les écoles de théorie des types «suédoises» et «françaises», mais je ne suis pas sûr que cette distinction existe réellement.
cody
Cette distinction n'existe pas, comme en témoigne le fait que Thierry Coquand vit en Suède. Ils sont tous informatiques.
Andrej Bauer
@cody: Je pensais que tous les traitements informatiques modernes utilisaient des jugements dactylographiés, car c'est le moyen le plus pratique d'obtenir l'eta pour pi / sigma. (Certainement Coq et Agda soutiennent cela.)
Neel Krishnaswami
@NeelKrishnaswami La conversion typée est nécessaire pour qu'aa ait un sens dans la plupart des situations, mais j'avais l'impression que cela pourrait rendre la métaphonie considérablement plus délicate. Peut-être que je me trompe complètement et cela rend tout simple. Il y a aussi la question de l'optimisation du contrôle de conversion afin de faire le moins de travail, y compris des obligations de vérification de type supplémentaires. Ce serait sûrement une excellente question de suivi.
cody