Шаги редукции функции-предшественника лямбда-исчисления

Итак, идея числительных Чёрча заключается в кодировании «данных» с помощью функций, верно? Это работает путем представления значения некоторой общей операцией, которую вы выполняете с ним. Поэтому мы можем пойти и в другом направлении, что иногда может прояснить ситуацию.

Церковные цифры - это унарные представления натуральных чисел. Итак, давайте использовать Z для обозначения нуля и Sn для обозначения преемника n. Теперь мы можем считать так: Z, SZ, SSZ, _7 _... Эквивалентное число Черча принимает два аргумента - первый соответствует S, а второй - _9 _, а затем использует их для построения вышеуказанного шаблона. Итак, учитывая аргументы f и x, мы можем считать так: x, f x, f (f x), _15 _...

Давайте посмотрим, что делает PRED.

Во-первых, он создает лямбду с тремя аргументами --_ 16_ - это число Чёрча, чей предшественник, конечно, нам нужен, что означает, что f и x являются аргументами для результирующего числа, что, таким образом, означает, что тело этой лямбды будет f применяется к x на один раз меньше, чем n.

Затем он применяет n к трем аргументам. Это сложная часть.

Второй аргумент, который соответствует Z из предыдущего, - это _24 _-- постоянная функция, которая игнорирует один аргумент и возвращает x.

Первый аргумент, который соответствует S из более раннего, - λgh.h (g f). Мы можем переписать это как λg. (λh.h (g f)), чтобы отразить тот факт, что n раз применяется только самая внешняя лямбда. Эта функция принимает накопленный результат до g и возвращает новую функцию с одним аргументом, которая применяет этот аргумент к g, примененному к f. Что, конечно, совершенно сбивает с толку.

Итак ... что здесь происходит? Рассмотрим прямую замену на S и Z. В ненулевом числе Sn n соответствует аргументу, связанному с g. Итак, помня, что f и x связаны во внешней области, мы можем считать так: λu.x, λh. h ((λu.x) f), λh'. h' ((λh. h ((λu.x) f)) f) ... Выполнив очевидные сокращения, мы получим это: λu.x, λh. h x, λh'. h' (f x) ... Здесь шаблон таков. функция передается «внутрь» на один уровень, в этот момент S применит ее, а Z проигнорирует. Таким образом, мы получаем по одному приложению f для каждого S кроме самого внешнего.

Третий аргумент - это просто функция идентификации, которая должным образом применяется самым внешним S, возвращая окончательный результат --_ 51_ применено на один раз меньше, чем соответствует количество S слоев n.

Ответ Макканна это хорошо объясняет. Возьмем конкретный пример для 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 3 раза:

(λ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 := λn λf λx.(n (λgλh.h (g f)) (λu.x)) (λu.u)

Давайте также определим три числа Чёрча, которые помогут в этом примере:

Zero := λfλx.x
One := λfλx. f (Zero f x)
Two := λfλx. f (One f x)
Three := λfλx. f (Two f x)

Чтобы понять, как это работает, давайте сначала сосредоточимся на этой части формулы:

n (λgλh.h (g f)) (λu.x)

Отсюда мы можем сделать следующие выводы: n - это число Чёрча, функция, которую нужно применить, - λgλh.h (g f), а начальные данные - λu.x

Имея это в виду, давайте попробуем пример:

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

Давайте сначала сосредоточимся на сокращении числительного (часть, которую мы объясняли ранее):

Three (λgλh.h (g f)) (λu.x)

Что сводится к:

(λgλh.h (g f)) (Two (λgλh.h (g f)) (λu.x))
(λgλh.h (g f)) ((λgλh.h (g f)) (One (λgλh.h (g f)) (λu.x)))
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (Zero (λgλh.h (g f)) (λu.x))))
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) ((λfλx.x) (λgλh.h (g f)) (λu.x)))) -- Here we lose one application of f
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (λu.x)))
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h ((λu.x) f)))
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h x))
(λgλh.h (g f)) (λh.h ((λh.h x) f))
(λgλh.h (g f)) (λh.h (f x))
(λh.h ((λh.h (f x) f)))

Заканчивается:

λh.h f (f x)

Итак, имеем:

PRED Three := λf λx.(λh.h (f (f x))) (λu.u)

Снова уменьшение:

PRED Three := λf λx.((λu.u) (f (f x)))
PRED Three := λf λx.f (f x)

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

Используя add1 как f и 0 как x, мы получаем:

PRED Three add1 0 := add1 (add1 0) = 2

Надеюсь это поможет.

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

Чтобы немного упростить дело, рассмотрим следующий вариант

    PRED := λn.n (λgh.h (g S)) (λu.0) (λu.u)

тогда вы можете заменить S на f и 0 на x.

Тело функции повторяет n раз преобразование M по аргументу N. Аргумент N является функцией типа (nat -> nat) -> nat, которая ожидает продолжения для nat и возвращает nat. Первоначально N = λu.0, то есть игнорирует продолжение и просто возвращает 0. Назовем N текущим вычислением.

Функция M: (nat -> nat) -> nat) -> (nat -> nat) -> nat изменяет вычисление g: (nat -> nat) -> nat следующим образом. Он принимает на входе продолжение h и применяет его к результату продолжения текущего вычисления g с помощью S.

Поскольку начальное вычисление игнорировало продолжение, после одного применения M мы получаем вычисление (λh.h 0), затем (λh.h (S 0)) и так далее.

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

Я добавлю свое объяснение к вышеупомянутым хорошим, в основном ради собственного понимания. Вот снова определение 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 - тождественная функция. Назовем это id.

λg (λh.h (g 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

So

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) путем вычисления в функции идентичности.