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

Ответ 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.

Ответ 2

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

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

Ответ 3

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

Во-первых, Id хотел бы добавить некоторые скобки в определение, которое сделало все более ясным для меня. Позволяет переформулировать данную формулу следующим образом:

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

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

Ответ 4

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

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

    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)) и т.д.

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

Ответ 5

Я добавлю свое объяснение к вышеперечисленным хорошим, в основном ради моего собственного понимания. Здесь определение 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)) - странная функция, которую нам нужно понять. Давайте назовем это F.

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

PRED := λnfx. F^n const_x id

Давайте внимательнее посмотрим на F:

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

F отправляет g для оценки в g (f). Обозначим через ev_y оценку при значении 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), оценивая тождественную функцию.