Используется ли теорема Церковно-Россера для уменьшения стоимости звонка?

Question

Я изучаю лямбда-исчисление и недавно увидел теорему Церковно-Россера. Теорема гласит, что при применении правил сокращения к членам в лямбда-исчислении упорядочение, в котором выбираются сокращения, не имеет никакого значения для конечного результата (из wiki). Но я считаю это несовместимым с уменьшением стоимости звонка и нормальным порядком. Например, лямбда-член λz. (Λx.x) y может быть сведен к λz.z при соблюдении правил нормального порядка сокращения. Но он не может быть дополнительно уменьшен при использовании сокращения по каждому значению, поскольку сокращение по каждому значению запрещает сокращение внутри λ-абстракции. Таким образом, термин терм λz. (Λx.x) y не может быть оценен с одним и тем же результатом с использованием разных правил, что, по-видимому, противоречит теореме Церков-Россера. В чем проблема? Пожалуйста, помогите мне. Спасибо большое!

Answer 1

Я думаю, что вы не указали на теорему Церкви-Россера, и именно это вызывает путаницу.

Насколько я понял (и я пишу это с "The Implementation of Functional Programming Languages" под рукой), теорема говорит следующее:

Если два лямбда-выражения E и F являются взаимо любой последовательности сокращений, то существует выражение G, такое, что и Е и F может быть сведено к G.

Из этого следует, что только одно выражение не может иметь две различные нормальные формы (хотя может быть не нормальная форма вообще). Однако, учитывая два сокращения, можно привести к нормальной форме, в то время как другая может расходиться - и некоторые могут даже остановиться раньше, например, по вызову.

Теперь, в вашем случае, E = \z.z находится в нормальной форме, и F = \z.((\x.x) z)^* может быть сведена к ней; единственное, что можно сказать здесь, это то, что F не может быть сведена ни к чему другому, кроме E, в то время как ничего не сказано о том, сколько его нужно уменьшить.

Существует также другая часть теоремы, в которой говорится, что если существует нормальная форма, ее найдет нормальный порядок. Опять же, никакого противоречия с вашим наблюдением, поскольку позывные и позывные по имени могут оказаться иначе, чем обычный порядок.

_{^* Я предполагаю, что вы имели в виду это InstEd из \z.((\x.x) y), так как последний не имеет смысла.}