Лямбда-исчисление, нормальный порядок, нормальная форма,

Question

В лямбда-исчислении, если термин имеет нормальную форму, стратегия сокращения нормального порядка всегда будет производить его.

Мне просто интересно, как строго доказать вышеприведенное утверждение?

Answer 1

Упомянутый вами результат является следствием так называемой теоремы стандартизации, утверждающей, что для любой редукционной последовательности M->N существует другой "стандартный" один и тот же термин M и N, где вы выполняете переопределения в крайнем левом внешнем порядке. Доказательство не так тривиально, и в литературе есть несколько разных подходов. Я добавляю краткую библиографию ниже.

Недавнее доказательство Касимы 5 (см. Также 1) имеет то преимущество, что не использует понятие остаточного и основано на чисто индуктивных методах. Это также хорошо для формализации 2, но если вы еще не уверены в предмете, это не особенно поучительно.

Общая идея стандартизации заключается в следующем. Предположим, что есть два переопределения R и S, где S находится в крайнем левом крайнем положении по отношению к R, и рассмотрим следующее сокращение:

                R      S
             M  ->  P  ->  N

Затем вы можете начать запускать S вместо этого, но таким образом вы можете дублировать (или стереть) переопределение R. Эти переопределения, которые, по сути, являются теми, что остаются от R после запуска S, называются остатками и обычно обозначаются как R/S (читай: остатки R после S). Итак, основная лемма заключается в том, что

             R S = S (R/S)

Чтобы использовать его для стандартизации, нам нужно обобщить R на произвольную последовательность ρ (которую мы можем считать стандартной, без переопределения в крайнем левом внешнем положении по отношению к S). Это все еще правда, что

         (*) ρS = S (ρ/S)

но что не так очевидно, так это стандартизация (ρ/S). С этой целью заметим, что ρ было выполнено до запуска S = C[\xM N], что по существу разделяет член на три несвязанные области: контекст C, M и N. Это вызывает перераспределение ρ на три последовательных последовательности:

           ρ1   inside M
           ρ2   inside N
           ρ3   inside C

(помните, что никакое переопределение не было в крайнем левом внешнем положении по отношению к S). Единственная часть, которая может быть продублирована (или стерта) - это ρ2, а остатки ρ2-0 ... ρ2-k легко упорядочиваются в соответствии с различными положениями k копий N, созданных стрельбой из S. Так

   S ρ1 ρ2-0 ... ρ2-k ρ_3

это стандартная версия (*).

Основная библиография.

1 А. Асперти, JJ. Леви. Стоимость использования в лямбда-исчислении. LICS 2013.

3 л.с. Барендрегт. Лямбда-исчисление, Северная Голландия (1984).

4 G.Gonthier, JJ. Леви, Пенсильвания. Mellies. Абстрактная теорема о стандартизации. LICS '92.

2 Ф.Гуйди. Стандартизация и слияние в чистом лямбда-исчислении, формализованном для доказательства теоремы Матиты. Журнал формализованных рассуждений 5(1): 1–25, 2012.

5 Р.Кашима. Доказательство теоремы стандартизации в лямбда-исчислении. Технический отчет C-145, Токийский технологический институт, 2000.

[6] JW. Клоп. Комбинаторные системы сокращения. Докторская диссертация, CWI, Амстердам, 1980.

[7] Г. Митчке. Теорема стандартизации для лямбда-исчисления. Z. Math.Logik. Grundlag. Математика, 25: 29–31, 1979

[8] М. Такахаши. Параллельные сокращения в лямбда-исчислении. Информация и вычисления 118, стр.120-127, 1995.

[9] Х. Си, Верхние оценки для стандартизации и приложения. Журнал Symboloc Logic 64, с.291-303, 1999.