Объяснение теоремы Церков-Россера в основных терминах

Question

Я хотел бы знать, как теорема Церковно-Россера используется в рамках программирования, в частности функционального программирования. Я искал информацию, но могу найти источники, ссылаясь на лямбда-исчисление (ограниченное знание) и бета-скидки.

Если бы кто-нибудь мог объяснить, где исчисление лямбда входит в это и какие сокращения, я думаю, что это прояснит ситуацию.

Мои первоначальные мысли о теореме Церкви-Россера состоят в том, что это связано с порядком эвакуляции и выполнения функций, но я не совсем уверен, является ли это точной информацией.

Спасибо.

Примечание: Я в настоящее время изучает Standard ML

Answer 1

Ваши первые мысли прекрасны.

• Исчисление лямбда - это формальная основа, на которой построено функциональное программирование.
• Исчисление лямбда - это система перезаписи терминов, а reduction означает следующее правило перезаписи.

• Исчисление лямбда не определяет конкретный порядок оценки, поэтому с учетом лямбда-выражения, где возможны множественные сокращения, теорема Церковно-Россера говорит, что вы можете выбрать один из них. Это дает разработчикам функционального программирования довольно много свободы для разработки семантики оценки. Например, в f (g x), считая обе чистые функции, уменьшаете ли вы f или g сначала эквивалентны.

  Описание Википедии из Church-Rosser theorem является:

  [I], е существует две различных сокращений или последовательность сокращений, которые могут быть применены к такому же сроку, то существует термин, который доступен из обоего результатов , применяя (возможно, пустые) последовательности дополнительных сокращений.

  Пример F (GX), где е является x² и г является 2x:

  (λx.x*x) ((λy.y+y) 2) ~β~> ((λy.y+y) 2)*((λy.y+y) 2) 
           ~β~> (2+2)*((λy.y+y) 2) 
           ~β~> (2+2)*(2+2) 
  
  (λx.x*x) ((λy.y+y) 2) ~β~> (λx.x*x) (2+2) 
           ~β~> (2+2)*(2+2) 
  

  В этом примере два различных сокращений являются бета-сокращения на любом из лямбдов, и один термин среди других, который доступен из обоих сокращений, - (2+2)*(2+2).