La canonicité implique-t-elle une faible normalisation ?

Question

Contexte:théorie des types.

Ma compréhension de :

• WN :chaque terme peut être réécrit en NF.
• Canonicité :chaque terme se réécrit sous forme canonique.

Cela conduit ensuite à une intuition où si la canonicité est vraie, alors nous obtenons NF = forme canonique et donc WN est valable.Cependant, je ne vois pas souvent les gens le dire, comme cette question parle de canonicité mais ne mentionne jamais la NF ou la normalisation.Sur nLab, la forme canonique est dite être la forme normale, ce qui justifie ma supposition "NF = forme canonique" mais cela ne dit pas que WN est donc valable.Je doute donc de mon intuition.

Alors, je me demande si c'est vrai (y a-t-il une preuve ?), ou si c'est faux (y a-t-il un contre-exemple ?).

Answer 1

La canonicité n'implique pas une faible normalisation.Tout d’abord, permettez-moi de formuler plus précisément les définitions impliquées :

• WN :tout terme ouvert est réductible à un terme normal
• Canonicité :tout terme fermé est réductible à un terme canonique

(Note:dans la métathéorie moderne de la théorie des types, il est plus courant de parler de conversion plutôt que de réduction, et de même de parler de l'existence unique de formes normales au lieu de normalisation faible/forte.Cette réponse reste valable si l'on remplace "réductible" ci-dessus par "convertible").

Les termes normaux et canoniques ne sont pas les mêmes.Par exemple, le x variable dans x : Bool le contexte est normal mais pas canonique.Aussi, le terme fermé λ(b : Bool). if true then b else b est canonique mais pas normal.

La théorie des types extensionnels a la propriété de canonicité mais pas WN, SN ou l'existence unique de formes normales.En effet, dans ETT, il est possible d'ajouter une égalité définitionnelle incohérente au contexte, ou d'ajouter une théorie équationnelle d'un système complet de Turing.Par exemple, dans le contexte ETT n : Nat, p : n = suc n le n la variable n'a pas de forme normale unique, puisque n peut être étendu arbitrairement en utilisant p.

Cependant, si nous avons un terme ETT fermé, nous ne pouvons rien avoir de douteux dans le contexte, donc un terme fermé peut toujours être évalué sous une forme canonique.