У меня есть такая функция
iter :: Int -> (a -> a) -> a -> a iter n f a = f (f ... (f a) .. )
как я могу определить такую функцию в нетипизированном лямбда-исчислении?
любая подсказка / помощь будут оценены.
Числа не существуют per se в чистом лямбда-исчислении.Вы должны создать представление для чисел (и показать, что они действительно ведут себя как числа).Основная идея состоит в том, что вы можете определить числа так, чтобы они были точно необходимой вам итерацией: n было бы лямбда-термином, который при задании функции f вычисляет n thитерация f.
n
f
Эта идея известна как Кодировка церкви .
iter == (rec g (fn f (fn n (fn x ((= n 0) x (g f (- n 1) (f x)))))))