Подразумевает ли каноничность слабую нормализацию?
-
29-09-2020 - |
Вопрос
Контекст:теория типов.
Мое понимание:
- ВН:каждый термин можно переписать в NF.
- Каноничность:каждый термин переписывается в каноническую форму.
Тогда это приводит к интуитивному выводу, что если соблюдена каноничность, то мы получаем NF = каноническая форма и, следовательно, выполняется WN.Однако я не вижу, чтобы люди часто говорили об этом, типа этот вопрос говорит о каноничности, но никогда не упоминает НФ или нормализацию.На нЛаб, каноническая форма называется нормальной формой, что подтверждает мое предположение «NF = каноническая форма», но не говорит о том, что WN, следовательно, выполняется.Поэтому я сомневаюсь в своей интуиции.
Итак, мне интересно, верно ли это (есть ли доказательство?) или нет (есть ли контрпример?).
Решение
Каноничность не подразумевает слабую нормализацию.Во-первых, позвольте мне сформулировать соответствующие определения более точно:
- ВН:каждый открытый терм сводится к нормальному терму
- Каноничность:каждый замкнутый терм сводится к каноническому терму
(Примечание:в современной метатеории теории типов чаще говорят о преобразовании вместо редукции, а также говорят об уникальном существовании нормальных форм вместо слабой/сильной нормализации.Этот ответ останется в силе, если мы заменим вышеприведенное слово «приводимый» на «конвертируемый»).
Нормальные и канонические термины — это не одно и то же.Например, 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, в контексте не может быть ничего хитрого, поэтому закрытый термин все равно может быть оценен до канонической формы.