Что означает выражение haskell

Question

Я только начал изучать Haskell, и я пытаюсь использовать лямбда-исчисление в Haskell. Я нашел это выражение, которое преобразует число церкви в число, но я не могу понять, что означает 0 в этом выражении. Я не могу найти его нигде:

zero = (\f -> \x -> x) 
one = (\f -> \x -> f x) 
two = (\f -> \x -> f (f x)) 

getNum church = church (\x-> (x + 1)) 0 

Это самый последний ноль, который меня смущает. Это базовый случай или какой-то аргумент для этого лямбда-выражения?

Answer 1

Это второй аргумент функции «церковь». Церковные цифры - это способ подсчета в Lambda Calculus. Они работают так же, как и числа Пеано. В таких случаях вы считаете

Z = 0 
S Z = 1 
S S Z = 2 

Прочитайте «Z» как «Zero» и «S» как «Successor». Итак, 1 является преемником 0, а 2 является преемником 1. Фактически его унарный подсчет.

В Lambda Calculus у вас есть только приложение-функция, поэтому вы можете определить 2 как функцию, которая принимает аргумент «f» и применяет его дважды.

В вашем примере указаны номера церкви нуль, один и два. Каждая из них представляет собой функцию, которая принимает два аргумента. Первый аргумент - это функция для применения, а вторая - значение, к которому она применяется. Функция getnum использует функцию succ (т. Е. \x -> x+1), которая затем применяется N раз к базовому регистру «0».

Вы также можете определить

getPeano church = church ('S':) "Z" 

Это будет предварять правильное число «S» с к Z, чтобы перевести номер церкви в число Пеано.