Подразумевает ли каноничность слабую нормализацию?

Question

Контекст:теория типов.

Мое понимание:

• ВН:каждый термин можно переписать в NF.
• Каноничность:каждый термин переписывается в каноническую форму.

Тогда это приводит к интуитивному выводу, что если соблюдена каноничность, то мы получаем NF = каноническая форма и, следовательно, выполняется WN.Однако я не вижу, чтобы люди часто говорили об этом, типа этот вопрос говорит о каноничности, но никогда не упоминает НФ или нормализацию.На нЛаб, каноническая форма называется нормальной формой, что подтверждает мое предположение «NF = каноническая форма», но не говорит о том, что WN, следовательно, выполняется.Поэтому я сомневаюсь в своей интуиции.

Итак, мне интересно, верно ли это (есть ли доказательство?) или нет (есть ли контрпример?).

Answer 1

Каноничность не подразумевает слабую нормализацию.Во-первых, позвольте мне сформулировать соответствующие определения более точно:

• ВН:каждый открытый терм сводится к нормальному терму
• Каноничность:каждый замкнутый терм сводится к каноническому терму

(Примечание:в современной метатеории теории типов чаще говорят о преобразовании вместо редукции, а также говорят об уникальном существовании нормальных форм вместо слабой/сильной нормализации.Этот ответ останется в силе, если мы заменим вышеприведенное слово «приводимый» на «конвертируемый»).

Нормальные и канонические термины — это не одно и то же.Например, x переменная в x : Bool контекст нормальный, но не канонический.Кроме того, закрытый срок λ(b : Bool). if true then b else b канонично, но ненормально.

Теория экстенсиональных типов обладает свойством каноничности, но не свойством WN, SN или однозначного существования нормальных форм.Это потому, что в ETT можно добавить в контекст противоречивое равенство определений или добавить эквациональную теорию полной по Тьюрингу системы.Например, в контексте ETT n : Nat, p : n = suc n тот n переменная не имеет уникальной нормальной формы, поскольку n можно произвольно расширить, используя p.

Однако, если у нас есть закрытый термин ETT, в контексте не может быть ничего хитрого, поэтому закрытый термин все равно может быть оценен до канонической формы.