Этапы сокращения функции-предшественника лямбда-исчисления

1110 Ответ Макканна объясняет это довольно хорошо. Давайте возьмем конкретный пример для Pred 3 = 2:

Рассмотрим выражение: n (λgh.h (g f)) (λu.x). Пусть K = (λgh.h (g f))

Для n = 0 мы кодируем 0 = λfx.x, поэтому при применении бета-редукции для (λfx.x)(λgh.h(gf)) означает, что (λgh.h(gf)) заменяется 0 раз. После дальнейшего бета-восстановления мы получаем:

λfx.(λu.x)(λu.u)

уменьшается до

λfx.x

где λfx.x = 0, как и ожидалось.

Для n = 1 мы применяем K 1 раз:

(λgh.h (g f)) (λu.x) => λh. h((λu.x) f) => λh. h x

Для n = 2 мы применяем K 2 раза:

(λgh.h (g f)) (λh. h x) => λh. h ((λh. h x) f) => λh. h (f x)

Для n = 3 мы применяем K три раза:

(λgh.h (g f)) (λh. h (f x)) => λh.h ((λh. h (f x)) f) => λh.h (f (f x))

Наконец, мы берем этот результат и применяем к нему функцию id, получаем

λh.h (f (f x)) (λu.u) => (λu.u)(f (f x)) => f (f x)

Это определение числа 2.

Реализация на основе списка может быть проще для понимания, но она требует много промежуточных шагов. Так что это не так приятно, как первоначальная реализация ИМО в Церкви.

Я добавлю свое объяснение к вышеупомянутым хорошим, главным образом для пользы моего собственного понимания. Вот определение PRED снова:

PRED := λnfx. (n (λg (λh.h (g f))) )  λu.x λu.u

материал на правой стороне первой точки, как предполагается, (n-1), состав сгиба f относился к x: f^ (n-1) (x).

Позволяют нам видеть почему дело обстоит так инкрементно пониманием выражение.

О» u.x является постоянной функцией, оцененной в x. Позвольте нам просто обозначить его const_x.

О» u.u является тождественным отображением. Давайте назовем это идентификатором.

О» g (О» h.h (g f)) является странной функцией, которую мы должны понять. Давайте назовем это F.

хорошо, таким образом, PRED говорит нам оценивать состав n-сгиба F на постоянной функции и затем оценивать результат на тождественном отображении.

PRED := λnfx. F^n const_x id

Позволяют нам более тщательно изучить F:

F:= λg (λh.h (g f))

F отправляет g в оценку в g (f). Давайте обозначим оценку в значении y ev_y. Таким образом, ev_y: = О» h.h y

Так

F = λg. ev_{g(f)}

Теперь мы выясняем, каков F^n const_x.

F const_x = ev_{const_x(f)} = ev_x

и

F^2 const_x = F ev_x = ev_{ev_x(f)} = ev_{f(x)}

Точно так же

F^3 const_x = F ev_{f(x)} = ev_{f^2(x)}

и так далее:

F^n const_x = ev_{f^(n-1)(x)}

Теперь,

PRED = λnfx. F^n const_x id

     = λnfx. ev_{f^(n-1)(x)} id

     = λnfx. id(f^(n-1)(x))

     = λnfx. f^(n-1)(x)

, который является тем, что мы хотели.

Супер глупо. Идея состоит в том, чтобы повернуть выполнение чего-то n времена в выполнение f n-1 времена. Решение состоит в том, чтобы применить F n времена к const_x, чтобы получить ev_ {f^ (n-1) (x)} и затем извлечь f^ (n-1) (x) путем оценки в тождественном отображении.