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: Wenn die Kanonizität gilt, dann erhalten wir NF = kanonische Form und daher gilt WN.Ich sehe jedoch nicht, dass die Leute so etwas oft sagen diese Frage spricht von Kanonizität, erwähnt jedoch nie NF oder Normalisierung.An nLab, kanonische Form wird als Normalform bezeichnet, was meine Vermutung „NF = kanonische Form“ rechtfertigt, aber es heißt nicht, dass WN daher gilt.Daher zweifle ich an meiner 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:Jeder offene Term ist auf einen normalen Term reduzierbar
• Kanonizität:Jeder geschlossene Begriff ist auf einen kanonischen Begriff reduzierbar

(Notiz:In der modernen Metatheorie der Typentheorie spricht man häufiger von Konvertierung statt von Reduktion und ebenso von der eindeutigen Existenz normaler Formen statt von schwacher/starker Normalisierung.Diese Antwort bleibt gültig, wenn wir oben „reduzierbar“ durch „umwandelbar“ ersetzen.

Normale und kanonische Begriffe sind nicht dasselbe.Zum Beispiel die x Variable in x : Bool Der Kontext ist normal, aber nicht kanonisch.Auch der geschlossene Begriff λ(b : Bool). if true then b else b ist kanonisch, aber nicht normal.

Die Theorie des Erweiterungstyps verfügt über die Kanonizitätseigenschaft, jedoch nicht über WN, SN oder die eindeutige Existenz von Normalformen.Das liegt daran, dass es in ETT möglich ist, dem Kontext eine inkonsistente Definitionsgleichung oder eine Gleichungstheorie eines Turing-vollständigen Systems hinzuzufügen.Zum Beispiel im ETT-Kontext n : Nat, p : n = suc n Die n Variable hat seitdem keine eindeutige Normalform n kann mit beliebig erweitert werden p.

Wenn wir jedoch einen geschlossenen ETT-Begriff haben, dürfen wir im Kontext nichts Zwielichtiges haben, sodass ein geschlossener Begriff immer noch in eine kanonische Form ausgewertet werden kann.