Как именно лямбда-исчисление охватывает интуитивное понятие вычислимости?

Я пытался обернуть голову вокруг того, что, почему и как вычислить, но я не могу понять, «почему это работает»?$\lambda$

«Интуитивно» я получаю модель вычислимости машин Тьюринга (ТМ). Но эта абстракция просто оставляет меня в замешательстве.$\lambda$

Давайте предположим, что ТМ не существуют - тогда как можно «интуитивно» убедиться в способности калькулятора уловить это понятие вычислимости. Как наличие множества функций для всего и их сочетаемость подразумевают вычислимость? Что мне здесь не хватает? Я читал статью Алонзо Черча об этом, но я все еще в замешательстве и ищу более «тупое» понимание того же самого.$\lambda$

$\lambda$

$\lambda$$\lambda$

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

Например, кодировка списка - это функция свертывания, которая сворачивает его. Обратите внимание, что это не кодировка Черча, а та, которую я получил от типов Перси и языков программирования. Парные кодировки Черча не дают нам рекурсии, мы должны добавить это обратно в себя с помощью своего рода комбинатора рекурсии.

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

cons x xs = lam f. lam a. f x (xs f a)
nil       = lam f. lam a. a

теперь мы можем определить суммирование с помощью функции добавления (см. церковные кодировки сверху)

sum xs = xs add 0

мы можем сделать больше и определить функцию карты

consApply f x xs = cons (f x) xs
map f xs = xs (consApply f) nil

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