Представление целых чисел как функций (церковные цифры?)

Question

Учитывая следующее определение функции и допуская аналогичные определения для всех положительных целых чисел, дайте определение типа и код для функции с именем плюс, которая примет в качестве аргументов две такие функции, представляющие целые числа, и вернет функцию, которая представляет сумму двух входных целых чисел. Например (plus one two) следует оценить функцию, которая принимает два аргумента f x и возвращается (f(f(f x))),

one f x = f x
two f x = f (f x)
three f x = f (f (f x)))

и т.п.

Я новичок в функциональном программировании, и я не могу разобраться с этим. Во-первых, я не знаю, как я могу определить функции для всех натуральных чисел, не записывая их (что, очевидно, невозможно). Как, если у меня есть plus(sixty, forty)Как моя функция может распознать, что шестьдесят е применяется 60 раз к x?

Я собираюсь написать это в Миранде, но я больше знаком с Хаскеллом, так что помощь обоим приветствуется.

Answer 1

Применить эквациональное мышление ¹ и абстракцию. У тебя есть

one   f x = f  x                            -- :: (a -> b) -> a -> b
two   f x = f (f  x)     -- = f (one f x)   -- :: (a -> a) -> a -> a
three f x = f (f (f x))  -- = f (two f x)   -- :: (a -> a) -> a -> a

таким образом, функция- преемник next естественно определяется, так что three = next two, Да, это так же просто, как писать next two вместо three в приведенном выше уравнении:

next :: ((b -> c) -> a -> b) -> (b -> c) -> a -> c
-- three f x = next two f x = f (two f x)   -- `two` is a formal parameter
next                num f x = f (num f x)   -- generic name `num`

zero :: t -> a -> a
zero f x = x

это отражает образец преемственности. f будет использоваться в качестве функции- преемника, и x как нулевое значение. Остальное следует. Например,

plus :: (t -> b -> c) -> (t -> a -> b) -> t -> a -> c
plus two one f x = two f (one f x)   -- formal parameters two, one
              -- = f (f (one f x))   -- an example substitution
              -- = f (f (f x)        --   uses the global definitions
              -- = three f x         --   for one, two, three

т.е. one f x будет использоваться в качестве нулевого значения two (вместо "обычного" x), таким образом представляя three, Число" n представляет последовательность п +1 операции.

Выше, опять же, на самом деле определяет общее plus операция, потому что two а также one это просто два формальных параметра функции:

Prelude> plus three two succ 0    -- built-in `succ :: Enum a => a -> a`
5
Prelude> :t plus three two
plus three two :: (a -> a) -> a -> a
Prelude> plus three two (1:) [0]
[1,1,1,1,1,0]

Ключевым моментом здесь является то, что функция - это объект, который будет вызывать значение при вызове. Сам по себе это непрозрачный объект. Аргументы "наблюдателя", которые мы применяем к нему, дают "значение" для того, что значит быть нулем, или чтобы найти преемника, и таким образом определить, какой результат получается, когда мы делаем наблюдение за значением числа.

¹ т. Е. Свободно заменять в любом выражении LHS на RHS определения или RHS на LHS, как вы считаете нужным (вплоть до переименования переменных, конечно, чтобы не захватывать / не скрывать существующие свободные переменные).

Answer 2

Чтобы преобразовать число в число, вы можете использовать что-то вроде:

type Numeral = forall a . (a -> a) -> (a -> a)

toChurch :: Int -> Numeral
toChurch 0 _ x = x
toChurch n f x = f $ toChurch (pred n) f x

fromChurch :: Numeral -> Int
fromChurch numeral = numeral succ 0

Answer 3

Вам не нужно распознавать, сколько раз функция вызывает f, Например, реализовать succ, который добавляет 1 к церковной цифре, вы можете сделать что-то вроде этого:

succ n f x = f (n f x)

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

succ n f x = n f (f x)

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