Bedeutet Kanonizität eine schwache Normalisierung?

Question

Kontext: Typentheorie.

Mein Verständnis von:

• WN: Jeder Begriff kann in NF umgeschrieben werden.
• Kanonizität: Jeder Begriff wird in kanonische Form umgeschrieben.

Dann führt es zu einer Intuition, wo, wenn Kanonizität gilt, wir NF = kanonische Form erhalten und daher WN gilt. Ich sehe jedoch nicht, dass Leute dies oft sagen, so wie diese Frage über Kanonizität spricht, aber niemals NF oder Normalisierung erwähnt. In nLab wird die kanonische Form als normale Form bezeichnet, was meine Vermutung "NF = kanonische Form" rechtfertigt, aber nicht besagt, dass WN daher gilt. Deshalb bezweifle ich meine Intuition.

Ich frage mich also, ob es richtig ist (gibt es einen Beweis?) Oder ob es falsch ist (gibt es ein Gegenbeispiel?).

Answer 1

Kanonizität bedeutet keine schwache Normalisierung. Lassen Sie mich zunächst die beteiligten Definitionen genauer formulieren:

• WN: Jede offene Laufzeit kann auf eine normale Laufzeit reduziert werden
• Kanonizität: Jeder geschlossene Begriff kann auf einen kanonischen Begriff reduziert werden

(Anmerkung: In der modernen Metatheorie der Typentheorie ist es üblicher, über Umwandlung statt Reduktion zu sprechen, und ebenso über die einzigartige Existenz von Normalformen anstelle von schwacher / starker Normalisierung. Diese Antwort bleibt gültig, wenn wir oben "reduzierbar" ersetzen mit "Cabrio").

Normale und kanonische Begriffe sind nicht dasselbe. Beispielsweise ist die xVariable im x : BoolKontext normal, aber nicht kanonisch. Auch der geschlossene Begriff λ(b : Bool). if true then b else bist kanonisch, aber nicht normal.

Die Theorie des Extensionstyps hat die Eigenschaft der Kanonizität, jedoch nicht WN, SN oder die einzigartige Existenz normaler Formen. Dies liegt daran, dass es in ETT möglich ist, dem Kontext eine inkonsistente definitive Gleichheit hinzuzufügen oder eine Gleichungstheorie eines Turing-vollständigen Systems hinzuzufügen. Beispielsweise hat n : Nat, p : n = suc ndie nVariable im ETT-Kontext keine eindeutige Normalform, da nsie mit beliebig erweitert werden kann p.

Wenn wir jedoch einen geschlossenen ETT-Begriff haben, können wir nichts zweifelhaftes im Kontext haben, so dass ein geschlossener Begriff immer noch in einer kanonischen Form bewertet werden kann.