Блог

Я пытаюсь добавить одно число в список в лямбда-исчислении, и я изо всех сил пытаюсь найти какие-либо отработанные примеры с использованием церковных цифр, не мог бы кто-нибудь, пожалуйста, указать мне направление некоторых примеров добавления списка в лямбда-исчислении

Для моделирования алгебраических типов данных в лямбда-исчислении я бы рекомендовал кодировку Скотта. У Кванга есть хороший пост в блоге по этому поводуhttps://kseo.github.io/posts/2016-12-13-scott-encoding.html.

Вот некоторые haskell, которые соответствуют вашему варианту использования.

 -- model as adt in haskell
data List a = Nil | Cons a (List a)

-- apply scott encoding
data ListS a r = ListS (forall r. r -> (a -> ListS -> r) -> r)

-- make constructors

nil :: ListS a
nil = ListS (n c -> n)

cons :: a -> ListS a -> ListS a
cons x xs = ListS (n c -> c x xs)
  

или в чистом лямбда-исчислении

 nil = n c -> n
cons = x xs n c -> c x xs