Canonicidade implica normalização fraca?

Question

Contexto: teoria dos tipos.

Meu entendimento de:

• WN: todo termo pode ser reescrito para NF.
• Canonicidade: cada termo é reescrito na forma canônica.

Em seguida, isso leva a uma intuição onde se a canonicidade é válida, então temos NF = forma canônica e, portanto, WN é válida. No entanto, não vejo as pessoas afirmarem isso com frequência, como se essa pergunta fosse sobre canonicidade, mas nunca menciona NF ou normalização. No nLab , a forma canônica é considerada a forma normal, o que justifica minha suposição "NF = forma canônica", mas não diz que WN, portanto, é válido. Portanto, estou duvidando de minha intuição.

Então, eu me pergunto se está certo (há uma prova?), Ou se está errado (há um contra-exemplo?).

Answer 1

Canonicidade não implica normalização fraca. Primeiro, deixe-me formular as definições envolvidas de forma mais precisa:

• NS: cada termo aberto é redutível a um termo normal
• Canonicidade: todo termo fechado é redutível a um termo canônico

(Nota: na metateoria moderna da teoria dos tipos, é mais comum falar sobre conversão em vez de redução, e da mesma forma falar sobre a existência única de formas normais em vez de normalização fraca / forte. Esta resposta permanece válida se substituirmos "redutível" acima com "conversível").

Os termos normais e canônicos não são iguais. Por exemplo, a xvariável no x : Boolcontexto é normal, mas não canônica. Além disso, o termo fechado λ(b : Bool). if true then b else bé canônico, mas não normal.

A teoria de tipo extensional tem a propriedade de canonicidade, mas não WN, SN ou existência única de formas normais. Isso porque no ETT é possível adicionar uma igualdade de definição inconsistente ao contexto, ou adicionar uma teoria equacional de um sistema Turing-completo. Por exemplo, no contexto ETT n : Nat, p : n = suc na nvariável não tem uma forma normal única, uma vez que npode ser expandida arbitrariamente usando p.

No entanto, se tivermos um termo ETT fechado, não podemos ter nada duvidoso no contexto, portanto, um termo fechado ainda pode ser avaliado em uma forma canônica.