Создание списка упорядоченных пар в лямбда-исчислении с использованием рекурсии

Question

Мой ввод - два списка: l = [x1, x2, x3,...,xn] и k = [y1, y2, y3,...,yn]

Мне нужен вывод a y = [(x1,y1),(x2,y2),(x3,y3)...(xn,yn)].

Как я могу применить рекурсию к своему коду? Я мог бы сделать это для первого пункта с f = \l k. (cons (pair (head l) (head k)) empty) но я не совсем понимаю, как использовать рекурсию для создания других элементов.

Функция "head" возвращает первый элемент списка, а функция "tail" возвращает список без первого элемента.

Answer 1

Естественно, это зависит именно от того, как вы реализовали кортежи, списки и т. Д. В Lambda Calculus. Но при условии стандартного функционала cons списки, и что оба списка имеют одинаковую длину, и что вы уже определили следующих помощников, некоторые из которых вы уже процитировали:

cons    -- construct a list from a node and another list
empty   -- the empty list
head    -- retrieve the first node value of a list
tail    -- retrieve all but the first node of a list
pair    -- pair values into a tuple
isEmpty -- return `true` if a list is `empty`, `false` otherwise
true    -- return the first argument
false   -- return the second argument

Затем мы можем рекурсивно сжать списки следующим образом:

ZIP = λlk. isEmpty l -- "if the list is empty…"
           empty     -- "return an empty result. Else…"
           (cons     -- "return a new list, containing…"
               (pair (head l) (head k))  -- "the zipped heads, and…"
               (ZIP  (tail l) (tail k))) -- "everything else zipped."

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

ZIP = Y (λzlk. isEmpty l empty (cons (pair (head l) (head k)) (z (tail l) (tail k)))

Определение Y является:

Y = λf.(λx.f(x x))(λx.f(x x))

Распутывание того, как именно это работает, - впечатляющая часть умственной гимнастики, которая не совсем подходит для этого вопроса, но использовать ее довольно просто. В общем, если у вас есть желаемое (но недопустимое, в необработанном LC) рекурсивное определение, подобное этому:

R = λ ??? . ??? R ???

Вместо этого вы можете написать это как абсолютно легальное, нерекурсивное определение:

R = Y (λr ??? . ??? r ???)

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