Рыцари Лямбда-исчисления бесконечности, написанные в виде кода lisp

Question

Рыцари логотипа Lambda Calculus имеют бесконечность, записанную в виде (Y F) = (F (Y F))

этот код лиспов одинаков и тоже представляет бесконечность?

(Y (λ (F) (YF)))

Answer 1

Эта сокращение вашего выражения Y (λ f. Y f) является Y Y, поскольку Y f сводится к f (Y f), мы получаем

Y Y --> Y (Y Y) --> Y Y (Y (Y Y)) --> Y (Y Y) (Y (Y Y)) --> ...

так что это расходящийся лямбда-термин.

Y f это не расходящийся термин сам по себе. Сводится к f (Y f), где f сейчас вступает во владение. Если f когда-либо использует свой аргумент и вынужден сделать это вызывающим, только тогда цепочка продолжится.

Answer 2

Y здесь комбинатор с фиксированной точкой. Для данной функции f она возвращает значение x, для которого x = f (x). Когда вместо записи x мы пишем Y (f), мы имеем Y (f) = f (Y (f)). В традиционных обозначениях лямбда-исчисления это (F (YF)) = (YF), что вы видите на изображении.

Некоторые числовые функции имеют одну или несколько неподвижных точек. Например, фиксированной точкой (положительной) функции квадратного корня, а также функцией квадрата являются 1 и 0. Некоторые числовые функции, например, f (x) → x + 1, не имеют фиксированной точки. В некоторых формализмах, включая нетипизированное лямбда-исчисление, каждая функция имеет фиксированную точку.

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

Answer 3

Это уравнение y-combinator на самом деле может быть получено через 4-5 сокращений, начиная с этого уравнения, которое также называется canonical combinator,

((lambda (self) (self self)) (lambda (self) (self self)))

Чтобы увидеть конкретный результат этой бесконечной рекурсии, нужно вставить окончательный критерий для рекурсии, например, в следующем виде примитивно-рекурсивного уравнения:

((lambda(s) (s s 100))
 (lambda(s n)
   (if (zero? n)
     0
     (+ n (s s (- n 1))))))

;Value: 5050

На самом деле картина представляет собой y-комбинатор или просто этот канонический комбинатор.

Эта картина была нарисована в MIT путем реализации встроенного языка программирования в схеме, в которой изображения были атомарными объектами, и простых способов объединения изображений, см. Здесь.

А по этой ссылке есть подробное описание языка функциональной геометрии ученого Peter Henderson который пытался создать язык программирования для генерации изображений Эшера, а также использовал его для создания логотипа MIT-SCHEME: