¿La canonicidad implica una normalización débil?

Question

Contexto:teoría de tipos.

Mi comprensión de:

• WN:cada término puede reescribirse a NF.
• Canonicidad:cada término se reescribe en forma canónica.

Luego conduce a una intuición en la que si se cumple la canonicidad, entonces obtenemos NF = forma canónica y, por lo tanto, se cumple WN.Sin embargo, no veo que la gente diga esto a menudo, como esta pregunta habla de canonicidad pero nunca menciona NF o normalización.En nLab, se dice que la forma canónica es la forma normal, lo que justifica mi suposición de "NF = forma canónica", pero no dice que WN, por lo tanto, se cumpla.Por eso dudo de mi intuición.

Entonces, me pregunto si está bien (¿hay alguna prueba?) o si está mal (¿hay un contraejemplo?).

Answer 1

La canonicidad no implica una normalización débil.Primero, permítanme expresar las definiciones involucradas con mayor precisión:

• WN:cada término abierto es reducible a un término normal
• Canonicidad:Todo término cerrado es reducible a un término canónico.

(Nota:En la metateoría moderna de la teoría de tipos, es más común hablar de conversión en lugar de reducción, y de la misma manera hablar de existencia única de formas normales en lugar de normalización débil/fuerte.Esta respuesta sigue siendo válida si reemplazamos "reducible" arriba con "convertible").

Los términos normales y canónicos no son lo mismo.Por ejemplo, el x variables en x : Bool El contexto es normal pero no canónico.Además, el plazo cerrado λ(b : Bool). if true then b else b Es canónico pero no normal.

La teoría de tipos extensionales tiene la propiedad de canonicidad pero no WN, SN o existencia única de formas normales.Esto se debe a que en ETT es posible agregar una igualdad definicional inconsistente al contexto, o agregar una teoría ecuacional de un sistema completo de Turing.Por ejemplo, en el contexto de la ETT n : Nat, p : n = suc n el n La variable no tiene una forma normal única, ya que n se puede ampliar arbitrariamente usando p.

Sin embargo, si tenemos un término ETT cerrado, no podemos tener nada dudoso en el contexto, por lo que un término cerrado aún puede evaluarse en una forma canónica.