A canonicidade implica uma normalização fraca?

Question

Contexto:teoria dos tipos.

Minha compreensão de:

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

Então isso leva a uma intuição onde se a canonicidade for válida, então obtemos NF = forma canônica e, portanto, WN é válido.No entanto, não vejo pessoas afirmarem isso com frequência, como essa questão fala sobre canonicidade, mas nunca menciona NF ou normalização.Sobre nLab, diz-se que a forma canônica é 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 da minha intuição.

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

Answer 1

A canonicidade não implica uma normalização fraca.Primeiro, deixe-me formular as definições envolvidas com mais precisão:

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

(Observação: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 por “conversível”).

Os termos normais e canônicos não são iguais.Por exemplo, o x variável em x : Bool contexto é normal, mas não canônico.Além disso, o prazo fechado λ(b : Bool). if true then b else b é canônico, mas não normal.

A teoria extensional dos tipos tem a propriedade de canonicidade, mas não WN, SN ou existência única de formas normais.Isso porque na ETT é possível adicionar uma igualdade de definição inconsistente ao contexto, ou adicionar uma teoria equacional de um sistema completo de Turing.Por exemplo, no contexto ETT n : Nat, p : n = suc n o n variável não tem forma normal única, pois n pode ser expandido 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 para uma forma canônica.