Комбинатор с фиксированной точкой - Fixed-point combinator

В математике и информатике в целом фиксированная точка функции - это значение, которое функция отображает сама себе.

В комбинаторной логике для информатики комбинатор с фиксированной точкой (или комбинатор с фиксированной точкой ) - это функция высшего порядка, которая возвращает некоторую фиксированную точку своей функции аргумента, если таковая существует. ${\ displaystyle {\textf {fix}}}$

Формально, если функция f имеет одну или несколько неподвижных точек, то

${\ Displaystyle {\textf {fix}} \ f = f \ ({\textf {fix}} \ f) \,}$

и, следовательно, при повторном применении

${\ Displaystyle {\textf {fix}} \ f = f \ (f \ (\ ldots f \ ({\textf {fix}} \ f) \ ldots)) \.}$

Y комбинатор

В классическом нетипизированном лямбда-исчислении каждая функция имеет фиксированную точку.

Частной реализацией исправления является парадоксальный комбинатор Карри Y , представленный

${\ Displaystyle {\textf {Y}} = \ lambda f. \ (\ lambda xf \ (x \ x)) \ (\ lambda xf \ (x \ x)) \.}$

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

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

Применительно к функции с одной переменной комбинатор Y обычно не завершается. Более интересные результаты получаются при применении комбинатора Y к функциям двух или более переменных. Вторая переменная может использоваться как счетчик или индекс. Результирующая функция ведет себя как цикл while или for в императивном языке.

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

Комбинатор с фиксированной точкой

Y комбинатор является реализацией с фиксированной точкой комбинатора в лямбда - исчислении. Комбинаторы с фиксированной точкой также могут быть легко определены в других функциональных и императивных языках. Реализация в лямбда-исчислении сложнее из-за ограничений в лямбда-исчислении. Комбинатор с фиксированной точкой может использоваться в различных областях:

• Общая математика
• Нетипизированное лямбда-исчисление
• Типизированное лямбда-исчисление
• Функциональное программирование
• Императивное программирование

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

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

В нетипизированном лямбда-исчислении функция, к которой применяется комбинатор с фиксированной точкой, может быть выражена с использованием кодирования, например кодирования Черча . В этом случае определенные лямбда-термины (которые определяют функции) рассматриваются как значения. «Запуск» (бета-уменьшение) комбинатора с фиксированной точкой при кодировании дает лямбда-член для результата, который затем может быть интерпретирован как значение с фиксированной точкой.

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

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

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

Ценности и домены

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

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

Например, рассмотрим

${\ displaystyle x ^ {2} = - 1 \ Rightarrow x = {\ frac {-1} {x}} \ Rightarrow f \ x = {\ frac {-1} {x}} \ land {\textf {Y }} \ f = x}$

Отдел по подписанным номерам может быть реализован в кодировке Церкви, так е могут быть представлены в сроке лямбды. Это уравнение не имеет решения в действительных числах. Но в области комплексных чисел i и -i являются решениями. Это показывает, что могут быть решения уравнения в другой области. Однако лямбда-член для решения вышеуказанного уравнения более странный, чем это. Лямбда-член представляет состояние, в котором x может быть либо i, либо -i , как одно значение. Информация, различающая эти два значения, была потеряна при смене домена. ${\ displaystyle Y \ f}$

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

Функция против реализации

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

Функция (или термин) лямбда-исчисления - это реализация математической функции. В лямбда-исчислении существует ряд комбинаторов (реализаций), которые удовлетворяют математическому определению комбинатора с фиксированной точкой.

Что такое комбинатор?

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

Использование в программировании

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

Факториальная функция

Факториальная функция представляет собой хороший пример того, как можно применить комбинатор с фиксированной точкой. Результат демонстрирует простую рекурсию, которая была бы реализована в одном цикле на императивном языке. Определение используемых чисел объясняется в кодировке Чёрча .

Функция, принимающая себя в качестве параметра, есть

${\ displaystyle F \ f \ n = (\ operatorname {IsZero} \ n) \ 1 \ (\ operatorname {multiply} \ n \ (f \ (\ operatorname {pred} \ n))) \.}$

Это дает YF n как

${\ displaystyle {\ begin {align} {\ textf {fix}} \ F \ n & = F \ ({\textf {fix}} \ F) \ n \\ & = (\ operatorname {IsZero} \ n) \ 1 \ (\ operatorname {multiply} \ n \ (({\textf {fix}} \ F) \ (\ operatorname {pred} \ n))) \. \ End {align}}}$

Настройка дает ${\ displaystyle {\ textf {fix}} \ F = \ operatorname {fact}}$

${\ Displaystyle \ OperatorName {fact} \ N = (\ Operatorname {IsZero} \ n) \ 1 \ (\ Operatorname {multiply} \ n \ (\ Operatorname {fact} \ (\ Operatorname {pred} \ n))) \.}$

Это определение ставит F в роли тела цикла, который нужно повторять, и эквивалентно математическому определению факториала:

${\ displaystyle \ operatorname {fact} \ n = {\ begin {cases} 1 & {\ text {if}} ~ n = 0 \\ n \ times \ operatorname {fact} \ (n-1) & {\ text { в противном случае.}} \ end {case}}}$

Комбинаторы с фиксированной точкой в ​​лямбда-исчислении

Y комбинатор, обнаруженный Haskell B. Curry , определяется как

${\ Displaystyle Y = \ lambda f. (\ lambda xf \ (x \ x)) \ (\ lambda xf \ (x \ x)) \.}$

Бета-сокращение этого дает:

${\ displaystyle Y \ g}$	${\ Displaystyle = (\ лямбда е. (\ лямбда хf \ (х \ х)) \ (\ лямбда хf \ (х \ х))) \ g}$	(по определению Y )
	${\ Displaystyle = (\ лямбда хg \ (х \ х)) \ (\ лямбда хg \ (х \ х))}$	(путем β-редукции λf: применено Y к g)
	${\ Displaystyle = г \ ((\ lambda xg \ (x \ x)) \ (\ lambda xg \ (x \ x)))}$	(путем β-редукции λx: применена левая функция к правой функции)
	${\ Displaystyle = г \ (Y \ г)}$	(по второму равенству)

Многократное применение этого равенства дает:

${\ Displaystyle Y \ g = g \ (Y \ g) = g \ (g \ (Y \ g)) = g \ (\ ldots g \ (Y \ g) \ ldots)}$

(Вышеприведенное равенство следует рассматривать как последовательность многошаговых β-редукций слева направо. Лямбда-член , как правило, не может быть β-редукцией к члену . Вместо этого можно интерпретировать знаки равенства как β-эквивалентности многоступенчатого β-редукции, позволяющего двигаться в обоих направлениях.) ${\ displaystyle g \ (Y \ g)}$${\ displaystyle Y \ g}$

Эквивалентное определение комбинатора с фиксированной точкой

Этот комбинатор с фиксированной точкой может быть определен как y , как в

${\ Displaystyle х = е \ х \ земля у \ е = х}$

Выражение для y может быть получено с использованием правил из определения выражения let . Во-первых, используя правило

${\ Displaystyle (\ существует xE \ земля F) \ iff \ operatorname {let} x: E \ operatorname {in} F}$

дает

${\ displaystyle \ operatorname {let} x = f \ x \ operatorname {in} y \ f = x \.}$

Кроме того, используя

${\ displaystyle x \ not \ in \ operatorname {FV} (E) \ land x \ in \ operatorname {FV} (F) \ to \ operatorname {let} x: G \ operatorname {in} E \ F = E \ (\ operatorname {let} x: G \ operatorname {in} F)}$

дает

${\ displaystyle y \ f = \ operatorname {let} x = f \ x \ operatorname {in} x \.}$

А затем, используя правило сокращения эта ,

${\ Displaystyle е \ х = у \ если и только если е = \ лямбда ху \,}$

дает

${\ displaystyle y = \ lambda f. \ operatorname {let} x = f \ x \ operatorname {in} x \.}$

Вывод комбинатора Y

Комбинатор Y Карри легко получить из определения y .

Начиная с,

${\ displaystyle \ lambda f. \ operatorname {let} x = f \ x \ operatorname {in} x \,}$

Лямбда-абстракция не поддерживает ссылку на имя переменной в применяемом выражении, поэтому x необходимо передать в качестве параметра переменной x . Мы можем думать об этом как о замене x на xx , но формально это неверно. Вместо определения у по дает ${\ displaystyle \ forall z, y \ z = x}$

${\ displaystyle \ lambda f. \ operatorname {let} y \ z = f \ (y \ z) \ operatorname {in} y \ z \.}$

Выражение let можно рассматривать как определение функции y , где z - параметр. Создание экземпляра z как y в вызове дает

${\ displaystyle \ lambda f. \ operatorname {let} y \ z = f \ (y \ z) \ operatorname {in} y \ y \.}$

И поскольку параметр z всегда передает функцию y ,

${\ displaystyle \ lambda f. \ operatorname {let} y \ z = f \ (z \ z) \ operatorname {in} y \ y \.}$

Используя правило сокращения эта ,

${\ Displaystyle е \ х = у \ эквив е = \ лямбда ху \,}$

дает

${\ displaystyle \ lambda f. \ operatorname {let} y = \ lambda zf \ (z \ z) \ operatorname {in} y \ y \.}$

Выражение пусть может быть выражено в виде лямбда - абстракции ; с использованием

${\ displaystyle n \ not \ in FV (E) \ to (\ operatorname {let} n = E \ operatorname {in} L \ Equiv (\ lambda nL) \ E)}$

дает

${\ displaystyle \ lambda f. (\ lambda yy \ y) \ (\ lambda zf \ (z \ z)) \.}$

Возможно, это простейшая реализация комбинатора с фиксированной точкой в ​​лямбда-исчислении. Однако одно бета-сокращение дает более симметричную форму Y-комбинатора Карри:

${\ Displaystyle \ лямбда е. (\ лямбда zf \ (z \ z)) \ (\ лямбда zf \ (z \ z)) \.}$

См. Также Перевод между let и лямбда-выражениями .

Другие комбинаторы с фиксированной точкой

В нетипизированном лямбда-исчислении комбинаторы с фиксированной точкой не особенно редки. На самом деле их бесконечно много. В 2005 году Майер Голдберг показал, что набор комбинаторов с фиксированной точкой нетипизированного лямбда-исчисления рекурсивно перечислим .

Y комбинатор может быть выражено в SKI-исчислении как

${\ Displaystyle Y = S (К (SII)) (S (S (KS) K) (K (SII))) \.}$

Простейший комбинатор с фиксированной точкой в ​​SK-исчислении, найденный Джоном Тромпом , - это

${\ Displaystyle Y '= SSK (S (K (SS (S (SSK)))) K) \.}$

хотя учтите, что он не в нормальном виде, который длиннее. Этот комбинатор соответствует лямбда-выражению

${\ Displaystyle Y '= (\ lambda xy.xyx) (\ lambda yx.y (xyx)) \.}$

Следующий комбинатор с фиксированной точкой проще, чем комбинатор Y, и β-сводится к комбинатору Y; его иногда называют самим комбинатором Y:

${\ Displaystyle Х = \ лямбда е. (\ лямбда х.хх) (\ лямбда хf (хх)) \.}$

Другой распространенный комбинатор с фиксированной точкой - это комбинатор с фиксированной точкой Тьюринга (названный в честь его первооткрывателя Алана Тьюринга ):

${\ Displaystyle \ Theta = (\ lambda xy.y (xxy)) \ (\ lambda xy.y (xxy)) \.}$

Его преимущество в том, что бета-сокращается до , тогда как и только бета-сокращается до общего термина. ${\ Displaystyle {\textf {Y}}}$${\ displaystyle \ Theta \ f}$${\ Displaystyle f \ (\ Theta f)}$${\ Displaystyle {\textf {Y}} \ f}$${\ Displaystyle е \ ({\textf {Y}} е)}$

${\ Displaystyle \ Theta}$ также есть простая форма вызова по значению:

${\ Displaystyle \ Theta _ {v} = (\ lambda xy.y (\ lambda z.xxyz)) \ (\ lambda xy.y (\ lambda z.xxyz)) \.}$

Аналогом взаимной рекурсии является поливариадический комбинатор неподвижных точек , который можно обозначить Y *.

Строгий комбинатор с фиксированной точкой

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

${\ Displaystyle Zgv = г (Zg) v \.}$

а в лямбда-исчислении это эта-расширение комбинатора Y :

${\ displaystyle Z = \ lambda f. (\ lambda xf (\ lambda v.xxv)) \ (\ lambda xf (\ lambda v.xxv)) \.}$

Нестандартные комбинаторы с фиксированной точкой

В нетипизированном лямбда-исчислении есть термы, которые имеют то же дерево Бёма , что и комбинатор с фиксированной точкой, то есть они имеют такое же бесконечное расширение λx.x (x (x ...)). Они называются нестандартными комбинаторами с фиксированной точкой . Любой комбинатор с фиксированной точкой также является нестандартным, но не все нестандартные комбинаторы с фиксированной точкой являются комбинаторами с фиксированной точкой, потому что некоторые из них не удовлетворяют уравнению, которое определяет «стандартные». Эти странные комбинаторы называются строго нестандартными комбинаторами с неподвижной точкой ; Примером может служить следующий комбинатор:

${\ Displaystyle N = BM (B (BM) B)}$

куда

${\ Displaystyle B = \ лямбда xyz.x (yz)}$

${\ Displaystyle M = \ лямбда x.xx \.}$

Множество нестандартных комбинаторов с фиксированной точкой не рекурсивно перечислимо.

Реализация на других языках

(Комбинатор Y - это конкретная реализация комбинатора с фиксированной точкой в ​​лямбда-исчислении. Его структура определяется ограничениями лямбда-исчисления. Нет необходимости или полезно использовать эту структуру при реализации комбинатора с фиксированной точкой в ​​других языках. )

Ниже приведены простые примеры комбинаторов с фиксированной точкой, реализованных в некоторых парадигмах программирования .

Ленивая функциональная реализация

В языке, который поддерживает ленивое вычисление , например, в Haskell , можно определить комбинатор с фиксированной точкой, используя определяющее уравнение комбинатора с фиксированной точкой, которое носит условное название fix. Поскольку Haskell имеет ленивые типы данных, этот комбинатор также можно использовать для определения фиксированных точек конструкторов данных (а не только для реализации рекурсивных функций). Здесь дано определение, за которым следуют некоторые примеры использования. В Hackage исходный образец:

fix, fix' :: (a -> a) -> a
fix f = let x = f x in x         -- Lambda dropped. Sharing.
                                 -- Original definition in Data.Function.
-- alternative:
fix' f = f (fix' f)              -- Lambda lifted. Non-sharing.

fix (\x -> 9)                    -- this evaluates to 9

fix (\x -> 3:x)                  -- evaluates to the lazy infinite list [3,3,3,...]

fact = fix fac                   -- evaluates to the factorial function
  where fac f 0 = 1
        fac f x = x * f (x-1)

fact 5                           -- evaluates to 120

Строгая функциональная реализация

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

${\ Displaystyle е \ (е ... (е \ (\ operatorname {fix} \ f)) ...) \ x}$.

Это может быть решено путем определения исправления с дополнительным параметром.

let rec fix f x = f (fix f) x (* note the extra x; here fix f = \x-> f (fix f) x *)

let factabs fact = function   (* factabs has extra level of lambda abstraction *)
   0 -> 1
 | x -> x * fact (x-1)

let _ = (fix factabs) 5       (* evaluates to "120" *)

Реализация императивного языка

Этот пример представляет собой слегка интерпретируемую реализацию комбинатора с фиксированной точкой. Класс используется для содержания функции исправления , называемой fixer . Исправляемая функция содержится в классе, наследуемом от fixer. Функция fix обращается к функции, которая должна быть зафиксирована как виртуальная функция. Что касается строгого функционального определения, fix явно задается дополнительным параметром x , что означает, что ленивое вычисление не требуется.

template <typename R, typename D>
class fixer
{
public:
    R fix(D x)
    {
        return f(x);
    }
private:
    virtual R f(D) = 0;
};

class fact : public fixer<long, long>
{
    virtual long f(long x)
    {
        if (x == 0)
        {
            return 1;
        }
        return x * fix(x-1);
    }
};

long result = fact().fix(5);

В императивно-функциональном языке, таком как Lisp , Scheme или Racket , Ландин (1963) предлагает использовать присвоение переменной для создания комбинатора с фиксированной точкой:

(define Y!
  (lambda (f-maker)
    ((lambda (f)
       (set! f (f-maker (lambda (x) (f x)))) ;; assignment statement
       f)
     'NONE)))

Используя лямбда-исчисление с аксиомами для операторов присваивания, можно показать, что Y! удовлетворяет тому же закону фиксированной точки, что и комбинатор Y вызова по значению:

${\ displaystyle ({\textf {Y}} _ {!} \ \ lambda xe) e '= (\ lambda xe) \ ({\textf {Y}} _ {!} \ \ lambda xe) e'}$

Набор текста

В Системе F (полиморфное лямбда-исчисление) полиморфный комбинатор с фиксированной точкой имеет тип;

∀a. (A → a) → a

где a - переменная типа . То есть fix принимает функцию, которая отображает a → a и использует ее для возврата значения типа a.

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

В простом типизированном лямбда-исчислении комбинатору с фиксированной точкой Y нельзя присвоить тип, потому что в какой-то момент он будет иметь дело с подчленом самоприменения в соответствии с правилом приложения: ${\ Displaystyle х ~ х}$

${\ displaystyle {\ Gamma \ vdash x \!: \! t_ {1} \ to t_ {2} \ quad \ Gamma \ vdash x \!: \! t_ {1}} \ over {\ Gamma \ vdash x ~ х \!: \! t_ {2}}}$

где имеет бесконечный тип . Фактически невозможно типизировать комбинатор с фиксированной точкой; в этих системах любая поддержка рекурсии должна быть явно добавлена ​​к языку. ${\ displaystyle x}$${\ displaystyle t_ {1} = t_ {1} \ to t_ {2}}$

Тип для комбинатора Y

В языках программирования, поддерживающих рекурсивные типы данных , можно ввести комбинатор Y, соответствующим образом учитывая рекурсию на уровне типа. Потребность в самостоятельном применении переменной x может быть устранена с помощью типа (Rec a), который определен как изоморфный (Rec a -> a).

Например, в следующем коде Haskell у нас есть Inи, outявляющиеся именами двух направлений изоморфизма, с типами:

In :: (Rec a -> a) -> Rec a
out :: Rec a -> (Rec a -> a)

что позволяет нам писать:

newtype Rec a = In { out :: Rec a -> a }

y :: (a -> a) -> a
y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x)))

Или, что то же самое в OCaml:

type 'a recc = In of ('a recc -> 'a)
let out (In x) = x

let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))

Альтернативно:

let y f = (fun x -> f (fun z -> out x x z)) (In (fun x -> f (fun z -> out x x z)))

Общая информация

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

Функция, для которой каждый вход является фиксированной точкой, называется функцией идентичности . Формально:

${\ Displaystyle \ forall х (е \ х = х)}$

В отличие от универсального количественного определения для всех , комбинатор с фиксированной точкой создает одно значение, которое является фиксированной точкой . Замечательное свойство комбинатора неподвижной точки состоит в том, что он строит неподвижную точку для произвольной заданной функции . ${\ displaystyle x}$${\ displaystyle f}$${\ displaystyle f}$

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

${\ Displaystyle \ forall х (е \ (е \ х) = е \ х)}$

Такие функции называются идемпотентными (см. Также Проекция (математика) ). Примером такой функции является функция, которая возвращает 0 для всех четных целых чисел и 1 для всех нечетных целых чисел.

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

${\ Displaystyle (Y \ \ лямбда хх) = (\ лямбда х. (хх) \ \ лямбда х. (хх))}$

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

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

Комбинатор Y позволяет определять рекурсию как набор правил перезаписи , не требуя встроенной поддержки рекурсии в языке.

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

Смотрите также

• Анонимная функция
• Итерация с фиксированной точкой
• Лямбда-исчисление # Рекурсия и фиксированные точки
• Лямбда-лифтинг
• Пусть выражение

Примечания

использованная литература

• Вернер Клюге, Абстрактные вычислительные машины: перспектива лямбда-исчисления , Springer, 2005, ISBN  3-540-21146-2 , стр. 73–77
• Майер Голдберг, (2005) О рекурсивной перечислимости комбинаторов с фиксированной точкой , Отчет БРИКС RS-05-1, Орхусский университет
• Маттиас Феллейзен , Лекция по Why из Y .

внешние ссылки

• Теория рекурсии и радость , Манфред фон Тун (2002 или ранее)
• Лямбда-исчисление - записки Дона Блахеты, 12 октября 2000 г.
• Y комбинатор
• «Использование Y-комбинатора в Ruby»
• «Функциональное программирование на Аде»
• Код Розетты - Y комбинатор