В чистом λ-исчислении у вас нет доступа к какому-либо типу данных, но вы все равно можете представлять их с помощью так называемых церковных кодировок.
Например, натуральные числа в унарном представлении могутлибо 0 (z), либо преемник (s) другого натурального числа n, т. е. представляющего n+1. Таким образом, у вас есть z, s z, s (s z), s (s (s z)) и т. Д. Чтобы представить их в λ-исчислении, вы используете функции, принимающие z и s в качестве аргументов: λz.λs.z, λz.λs.s z, λz.λs.s (s z), λz.λs.s (s (s z)) и т. Д.
Что довольно круто в этом представлении, так это то, что оно также дает вам рекурсор для натуральных чисел, т. Е. Способ индуктивного построения чисел на вашем натуральном числе. *
Скажем, вы хотите проверить, является ли n 0, просто напишите n true (λm. false) (где true и false будут представлять логические значения, но на самом деле они могут быть чем угодно). Затем у вас есть
0 true (λm. false) = true
1 true (λm. false) = (λm. false) true = false
2 true (λm. false) = (λm. false) ((λm. false) true) = false
...
, что означает, что вы можете отличить 0 от остальных церковных цифр. В основном, когда вы вводите церковную цифру b и f, вы даете изображение 0 как b и функцию f для перехода от изображения n к изображению n+1.
Чтобы написать функцию succ для добавления единицы к натуральному числу, необходимо добавить одну s перед ее представлением:
succ n = λz.λs.s (n z s)
n z s является синонимомудаление двух ведущих λ s.
Теперь списки могут быть представлены одинаково. Список может быть пустым списком ([] или nil) или каким-либо элементом (head), прикрепленным к другому списку (tail): head :: tail или cons head tail. Мы делаем то же самое трюк : nil это λn.λc.n и cons x nil это λn.λc.c x n, cons y (cons x nil) это λn.λc.c y (c x n) и т. Д.
Аналогично вы можете кормить базурегистр и функция для выполнения списка fold .
cons x (cons y nil) b f = f x (f y b)
(cons x1 (cons x2 (... (cons xn nil) ...))) b f = f x1 (f x2 (... (f xn b) ...)))
. Чтобы получить длину, вы должны заметить, что длина nil равна 0 и что длинаcons x l равно succ (length l), без учета x. Итак, length l = l 0 (λ_.λn. succ n).
Вы должны продолжать создавать такие примитивы, чтобы в конечном итоге решить вашу проблему.
Далее вы хотите написать firstn функцию, которая принимает целое число n и список l и возвращает n первые элементы. В основном у вас есть
firstn 0 l = nil
firstn (n+1) nil = nil
firstn (n+1) (cons a l) = cons a (firstn n l)
, поэтому вы сначала делаете анализ по натуральному числу, а затем по списку. Я напишу это как функцию, принимающую натуральное число и возвращающую функцию, берущую список и возвращающую список.
firstn = λn. n (λl. nil) (λr.λl. l nil (λa.λl. cons a (r l)))
Там r представляет рекурсивный вызов firstn n, когда я определяю firstn (n+1).
Это может показаться немного сложным, и, честно говоря, знание того, как написать это на правильном функциональном языке с помощью сопоставления с образцом, помогает. Я лично протестировал их в coq.
Возможно, еще проще понять, если бы сначала написал функцию анализа случаев в списках, но для этого нам нужно построить пары.
Парачто-то, состоящее из двух элементов, поэтому из любой пары вы хотите иметь возможность наблюдать эти два элемента.
pair a b = λp. p a b
Другими словами
pair = λa.λb.λp. p a b
Затем вы можете взять первое и второепроекции пары легко.
fst = λp. p (λx.λy.x)
snd = λp. p (λx.λy.y)
Вы можете видеть
fst (pair a b) = (pair a b) (λx.λy.x)
= (λp. p a b) (λx.λy.x)
= (λx.λy.x) a b
= a
Анализ случаев в списках похож на сопоставление с образцом, в ocaml вы бы написали
match l with
| nil -> b
| cons h t -> f h t
то есть, если l равно nil, я хочу вернуть b, а если это cons h t, я хочу вернуть f h t.
Здесь нет рекурсивных вызовов, однако применение l автоматически сделает рекурсию. В частности, вы получаете доступ не к t, а к значению рекурсивного вызова на t. Чтобы обойти это, мы вернем как исходный список, так и значение, которое мы хотим вернуть, используя пары.
caseL = λl.λb.λf. snd (l (pair nil b) (λx.λr. pair (cons x (fst r) (f x (fst r)))
, такие что
caseL nil b f = b
caseL (cons x l) b f = f x l
, как мы хотели.
Теперь мы можем снова написать firstn. Помните, что firstn n вычисляет функцию по спискам, удаляя все, кроме n первых элементов.
firstn = λn. n (λl. nil) (λr.λl. caseL l nil (λh.λt. cons h (r t)))
Она подчиняется следующей структуре
n b (λr. f r)
, соответствующей наведению на n,For 0 мы возвращаем базовый случай b и для n+1 мы получаем значение рекурсивного вызова r для получения нашего ответа f r. В нашем случае базовый случай - это функция firstn 0, которая означает, что функция берет список и выбрасывает его. При определении firstn (n+1) рекурсивный вызов соответствует firstn n, и в этом случае мы хотим выполнить анализ случая в списке, как указано выше, используя firstn n (то есть r) в хвосте, если список непустой.