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

Question

Contexto: teoría de tipos.

Mi comprensión de:

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

Luego conduce a una intuición donde si la canonicidad se mantiene, entonces obtenemos NF = forma canónica y por lo tanto WN se mantiene. Sin embargo, no veo que la gente diga esto a menudo, como si esta pregunta hablara de canonicidad pero nunca mencionara 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 cumple. Por tanto, 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 se puede reducir a un término normal
• Canonicidad: todo término cerrado se puede reducir 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, e igualmente 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, la xvariable en x : Boolcontexto es normal pero no canónica. Además, el término cerrado λ(b : Bool). if true then b else bes canónico pero no normal.

La teoría de tipos extensionales tiene la propiedad de canonicidad, pero no WN, SN o la existencia única de formas normales. Eso es porque en ETT es posible agregar una igualdad de definición inconsistente al contexto, o agregar una teoría de ecuaciones de un sistema completo de Turing. Por ejemplo, en el contexto ETT, n : Nat, p : n = suc nla nvariable no tiene una forma normal única, ya que npuede expandirse 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 se puede evaluar a una forma canónica.