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

Question

в лямбда-исчислении (λ x. Λ y. Λ s. Λ z. X s (y s z)) используется для сложения двух церковных чисел. Как мы можем это объяснить, есть ли хороший ресурс для лямбда-исчисления для функционального программирования? Ваша помощь очень ценится

Answer 1

На самом деле λ f1. λ f2. λ s. λ z. (f1 s (f2 s z)) вычисляет сложение, поскольку оно фактически подставляет (f2 s z) число, представленное как f2, в «ноль» внутри (f1 s z).

Пример: возьмем два для f2, s s z в развернутом виде. f1 один: s z. Замените эту последнюю z на f2, и вы получите s s s z, расширенную форму для трех.

Это было бы легче с доской и маханием рукой, извините.

Answer 2

В лямбда-исчислении вы кодируете тип данных с точки зрения операций, которые он вызывает. Например, логическое значение - это функция выбора, которая принимает на вход два значения a и b и возвращает либо a, либо b:

                      true = \a,b.a   false = \a,b.b

Какая польза от натурального числа? Его основная вычислительная цель состоит в том, чтобы обеспечить привязку к итерации. Итак, мы кодируем натуральное число как оператор которая принимает на вход функцию f, значение x и выполняет итерацию приложения f над x для n раз:

                        n = \f,x.f(f(....(f x)...))

с n вхождениями f.

Теперь, если вы хотите итерировать n + m раз функцию f, начиная с x Вы должны начать итерацию n раз, то есть (n f x), а затем итерацию для m дополнительное время, начиная с предыдущего результата, то есть

                                m f (n f x)

Точно так же, если вы хотите повторять n * m раз, вам нужно повторять m раз операция итерации n раз f (как в двух вложенных циклах), то есть

                                 m (n f) x  

Предыдущая кодировка типов данных более формально объясняется в терминах конструкторов и соответствующих элиминаторов (так называемый Кодировка Бома-Берардуччи).