(Убедитесь, что вы понимаете функции высшего порядка ) . В Алонзо-Черч * нетипизированное лямбда-исчисление функция является единственным примитивным типом данных.Здесь нет чисел, логических значений, списков или чего-либо еще, только функции.Функции могут иметь только 1 аргумент, но функции могут принимать и / или возвращать функции - не значения этих функций, а сами функции.Поэтому, чтобы представлять числа, логические значения, списки и другие типы данных, вы должны придумать способ, чтобы анонимные функции могли их поддерживать. Церковные цифры - это способ представления натуральных чисел .Три наиболее примитивных конструкции в нетипизированном лямбда-исчислении:
λx.x, тождественная функция , принимает некоторую функцию и немедленно возвращает ее. λx.x x, self-application. λf.λx.f x, application application, принимает функцию и аргумент и применяет функцию к аргументу.
Как вы кодируете 0, 1,2 как ничего кроме функций?Нам как-то нужно встроить понятие количество в систему.У нас есть только функции, каждая функция может быть применена только к 1 аргументу.Где мы можем увидеть что-то похожее на количество?Эй, мы можем применить функцию к параметру несколько раз!Очевидно, что в трех повторяющихся вызовах функции есть ощущение количества: f (f (f x)).Итак, давайте закодируем его в лямбда-исчислении:
- 0 =
λf.λx.x - 1 =
λf.λx.f x - 2 =
λf.λx.f (f x) - 3 =
λf.λx.f (f (f x))
И так далее.Но как вы идете от 0 до 1 или от 1 до 2?Как бы вы написали функцию, которая, учитывая число, вернула бы число, увеличенное на 1?Мы видим шаблон в церковных цифрах, что термин всегда начинается с λf.λx., и после того, как у вас есть конечное повторное применение f , поэтому нам нужно каким-то образом попасть в тело λf.λx. и обернуть его вдругой f.Как изменить тело абстракции без сокращения?Ну, вы можете применить функцию, обернуть тело в функцию, а затем обернуть новое тело в старую лямбда-абстракцию.Но вы не хотите, чтобы аргументы менялись, поэтому вы применяете абстракции к значениям с тем же именем: ((λf.λx.f x) f) x → f x, но ((λf.λx.f x) a) b) → a b, а это не то, что нам нужно.
Вот почему add1 - этоλn.λf.λx.f ((n f) x): вы применяете n к f, а затем x, чтобы уменьшить выражение для тела, затем применяете f к этому телу, затем снова абстрагируете его с помощью λf.λx.. Упражнение: также убедитесь, что это правда, быстро выучите β-уменьшение и уменьшите (λn.λf.λx.f ((n f) x)) (λf.λx.f (f x)) до шага 2 на 1.
Теперь вы понимаете интуицию, лежащую в основе обертывания телав другой вызов функции, как мы реализуем сложение 2 чисел?Нам нужна функция, которая, учитывая λf.λx.f (f x) (2) и λf.λx.f (f (f x)) (3), вернет λf.λx.f (f (f (f (f x)))) (5).Посмотрите на 2. Что если бы вы могли заменить его x телом 3, то есть f (f (f x))?Очевидно, чтобы получить тело из 3, просто примените его к f, а затем x.Теперь примените 2 к f, но затем примените его к телу 3, а не к x.Затем снова оберните его в λf.λx.: λa.λb.λf.λx.a f (b f x).
Заключение: Чтобы сложить вместе 2 числа a и b, оба из которых представлены как церковные цифры, выхотите заменить x в a телом b, чтобы f (f x) + f (f (f x)) = f (f (f (f (f x)))).Чтобы это произошло, примените a к f, затем к b f x.