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.

Ensuite, cela conduit à une intuition où si la canonicité tient, alors nous obtenons NF = forme canonique et donc WN tient. Cependant, je ne vois pas les gens dire cela souvent, comme cette question parle de canonicité mais ne mentionne jamais NF ou normalisation. Sur nLab , on dit que la forme canonique est une forme normale, ce qui justifie ma supposition "NF = forme canonique" mais cela ne dit pas que WN est donc valable. Par conséquent, je doute 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 normalisation faible. Tout d'abord, permettez-moi de formuler plus précisément les définitions impliquées:

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

(Remarque: dans la métathéorie moderne de la théorie des types, il est plus courant de parler de conversion au lieu de réduction, et de même de parler d'existence unique de formes normales au lieu de normalisation faible / forte. Cette réponse reste valable si nous remplaçons "réductible" ci-dessus avec «cabriolet»).

Les termes normaux et canoniques ne sont pas les mêmes. Par exemple, la xvariable en x : Boolcontexte est normale mais pas canonique. De plus, le terme fermé λ(b : Bool). if true then b else best 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 de Turing-complet. Par exemple, dans le contexte ETT, n : Nat, p : n = suc nla nvariable n'a pas de forme normale unique, puisqu'elle npeut être développée 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.