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

Question

Я застреваю с описанием Википедии функции предшественника в лямбда-исчислении.

Википедия говорит следующее:

ПРЕД:= λnfx.n (λgh.h (g f)) (λu.x) (λu.u)

Может кто-нибудь объяснить пошаговые процессы сокращения?

Благодарю.

Answer 1

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

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

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

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

Далее это относится n до трех аргументов. Это сложная часть.

Второй аргумент, который соответствует Z из ранее, это λu.x- константная функция, которая игнорирует один аргумент и возвращает 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, возвращая окончательный результат--f применяется один раз, чем количество S слои n соответствует.

Answer 2

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

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

Answer 3

Прочитав предыдущие ответы (хорошие), я хотел бы дать свое собственное видение вопроса в надежде, что это кому-то поможет (исправления приветствуются). Я буду использовать пример.

Прежде всего, я хотел бы добавить некоторые скобки к определению, которое сделало все более понятным для меня. Давайте доработаем данную формулу:

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

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

Answer 4

Разделить это определение

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

на 4 части:

      PRED := λn.λf.λx. | n | (λg.λh.h (g f)) | (λu.x) | (λu.u)
                    -   ---------------   ------   ------
                    A   B                 C        D

Пока что игнорируйтеD. По определению числительных Черча,A B CявляетсяB^n C: Нанесите складки наC.

Теперь относитесь к машине, которая превращает один вход в один выход. Его вводgимеет форму , при добавлении становится(λh.h *) f = f *. Это добавляет еще одно приложение к*. Результатf *затем предваряется стать .

Вы видите закономерность: Каждое применение поворотовλh.h *вλh.h (f *). Если бы мы имели в качестве начального термина, мы бы имелиλh.h (f^n x)как конечный срок (послеnприменения).

Однако начальный срокC = (λu.x), когда добавляется , становится(λu.x) f = x, затем предваряемыйλh.hстановиться . Итак, у нас былоλh.h xпосле, а не до первого примененияB. Вот почему мы имеем в качестве конечного термина: первое применениеfбыл проигнорирован.

Наконец, применитеλh.h (f^(n-1) x)кD = (λu.u), то есть тождество, чтобы получитьf^(n-1) x. То есть:

      PRED := λn.λf.λx.f^(n-1) x

Answer 5

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

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

Материал с правой стороны от первой точки должен представлять собой (n-1) кратную композицию f, примененную к x: f^(n-1)(x).

Давайте посмотрим, почему это так, постепенно просматривая выражение.

"Ux - постоянная функция со значением в x. Обозначим его просто const_x.

Î "uu - тождественная функция. Назовем это id.

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

Answer 6

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

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

    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)) и так далее.

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