Свойство нормализации (абстрактное переписывание) - Normalization property (abstract rewriting)

В математическая логика и теоретическая информатика, а переписать систему имеет (сильный) свойство нормализации или это прекращение если каждый срок сильно нормализующий; то есть, если каждая последовательность перезаписи в конечном итоге заканчивается несводимый термин, также называемый нормальная форма. Система перезаписи может также иметь свойство слабой нормализации, что означает, что для каждого члена существует по крайней мере одна конкретная последовательность перезаписей, которая в конечном итоге дает нормальную форму, то есть неприводимый член.

Лямбда-исчисление

Нетипизированное лямбда-исчисление

В чистый нетипизированный лямбда-исчисление не удовлетворяет свойству сильной нормализации, и даже свойству слабой нормализации. Рассмотрим термин ${ displaystyle lambda x.xxx}$ . Он имеет следующее правило перезаписи: Для любого срока ${ displaystyle t}$ ,

{ displaystyle ( mathbf { lambda} x.xxx) т rightarrow ttt}

Но подумайте, что происходит, когда мы подаем заявку ${ displaystyle lambda x.xxx}$ себе:

{ displaystyle { begin {align} ( mathbf { lambda} x.xxx) ( lambda x.xxx) & rightarrow ( mathbf { lambda} x.xxx) ( lambda x.xxx) ( лямбда x.xxx) & rightarrow ( mathbf { lambda} x.xxx) ( lambda x.xxx) ( lambda x.xxx) ( lambda x.xxx) & rightarrow ( mathbf { lambda} x.xxx) ( lambda x.xxx) ( lambda x.xxx) ( lambda x.xxx) ( lambda x.xxx) & rightarrow ldots , end {выровнено }}}

Следовательно, термин ${ Displaystyle ( лямбда х.ххх) ( лямбда х.ххх)}$ не является ни сильно, ни слабо нормализующим.

Типизированное лямбда-исчисление

Различные системы типизированное лямбда-исчисление в том числепросто типизированное лямбда-исчисление, Жан-Ив Жирар с Система F, и Тьерри Кокванд с расчет конструкций сильно нормализуют.

Система лямбда-исчисления с свойство нормализации можно рассматривать как язык программирования, обладающий тем свойством, что каждая программа прекращается. Хотя это очень полезное свойство, у него есть недостаток: язык программирования со свойством нормализации не может быть Тьюринг завершен.^[1] Это означает, что есть вычислимые функции, которые не могут быть определены в простом типизированном лямбда-исчислении (и аналогично есть вычислимые функции, которые не могут быть вычислены в расчет конструкций или же Система F ). Например, невозможно определить переводчик-самоучитель в любом из приведенных выше расчетов ^[2].^[3]^[4]

Смотрите также

Примечания

^ Университет Рочестера, [1]
^ (в том смысле, что это заставляет язык быть нетипизированным или не быть целостным языком); Предположим, что "eval" - это функция, которая интерпретирует язык TLC (типизированное лямбда-исчисление), и она принимает "код" в качестве аргумента, семантически невозможно правильно ввести "eval" (то есть определить его тип), потому что вы можете ' t введите все возможные фрагменты кода TLC (поскольку их несчетное количество (Диагональный аргумент ), или, если вы заставили его принимать тип типа "строка", проанализируйте его с точки зрения реализации, но не с точки зрения семантической корректности (предположим, что другая функция "evil" выполняет следующие действия (evil = 1 + eval ([здесь идет код зла]), и это ускользает от свойства нормализации («зло» никогда не нормализуется, и это потому, что оно нарушает некоторые предположения строгого доказательства нормализации (поскольку оно подразумевает зависимые типы данных)))).
^ Конор Макбрайд (май 2003 г.), "по прекращении" (отправлено в список рассылки Haskell-Cafe).
^ Андрей Бауэр (июнь 2014 г.), Ответ на: Общий язык, который может интерпретировать только полный язык Тьюринга (размещено в Теоретической информатике StackExchange сайт)