Введение
1=Функция высшего порядка Y, для которой Y f = f (Y f)
В комбинаторной логике, используемой в информатике, комбинатор фиксированной точки – это функция высшего порядка (то есть функция, принимающая другую функцию в качестве аргумента), которая возвращает фиксированную точку (значение, которое отображается само на себя) своей аргументированной функции, если такая точка существует. Формально, если Y – комбинатор фиксированной точки, а f – функция, имеющая одну или несколько фиксированных точек, то Y f является одной из этих фиксированных точек, то есть Y f = f (Y f).
In combinatory logic for computer science, a fixed point combinator (or fixpoint combinator), is a higher order function (i. e. a function which takes a function as argument) that returns some fixed point (a value that is mapped to itself) of its argument function, if one exists. Formally, if is a fixed point combinator and the function has one or more fixed points, then is one of these fixed points, i. e.
Комбинаторы фиксированной точки могут быть определены в лямбда-исчислении и в функциональных языках программирования и предоставляют возможность рекурсивных определений.
Комбинатор Y в ламбда-калькуле
В классическом нетипизированном лямбда-исчислении каждая функция имеет фиксированную точку. Особой реализацией является парадоксальный комбинатор Хаскелла Карри Y, заданный
(Здесь мы используем стандартные обозначения и соглашения лямбда-исчисления: Y – это функция, которая принимает один аргумент f и возвращает всё выражение, следующее за первым периодом; выражение обозначает функцию, принимающую один аргумент x, рассматриваемый как функция, и возвращающую выражение , где обозначает применение x к самому себе. Сопоставление выражений обозначает применение функции, ассоциативно слева и имеет более высокий приоритет, чем период.)
Применение
Применяемый к функции с одной переменной, Y-комбинатор обычно не завершается. Более интересные результаты достигаются при применении Y-комбинатора к функциям двух и более переменных. Дополнительные переменные могут использоваться как счетчик или индекс. Полученная функция ведет себя подобно циклу while или for в императивном языке программирования. Используемый таким образом, Y-комбинатор реализует простую рекурсию. Лямбда-исчисление не позволяет функции фигурировать в собственном определении, как это возможно во многих языках программирования, но функцию можно передать в качестве аргумента функции высшего порядка, которая применяет её рекурсивно. Y-комбинатор также может быть использован при реализации парадокса Карри. Суть парадокса Карри заключается в том, что нетипизированное лямбда-исчисление является несостоятельной дедуктивной системой, и Y-комбинатор демонстрирует это, позволяя анонимному выражению представлять ноль или даже множество значений. Это противоречит математической логике.
Значения и области
Многие функции не имеют фиксированных точек, например, используя кодирование Черча, натуральные числа можно представить в лямбда-исчислении, и эта функция f может быть определена в лямбда-исчислении. Однако область определения этой функции теперь будет включать все лямбда-выражения, а не только те, которые представляют натуральные числа. Комбинатор Y, примененный к f, даст фиксированную точку для f, но эта фиксированная точка не будет представлять натуральное число. Если попытаться вычислить Y f в реальном языке программирования, возникнет бесконечный цикл.
Функция против реализации
Комбинатор фиксированной точки может быть определён в математике, а затем реализован на других языках. Общая математика определяет функцию, исходя из её экстенсиональных свойств. То есть, две функции считаются равными, если они выполняют одно и то же преобразование. Лямбда-исчисление и языки программирования рассматривают тождество функций как интенсиональное свойство. Тождество функции определяется её реализацией. Функция (терм) лямбда-исчисления является реализацией математической функции. В лямбда-исчислении существует несколько комбинаторов (реализаций), удовлетворяющих математическому определению комбинатора фиксированной точки.
Определение термина "комбинатор"
Комбинаторная логика — это теория функций высшего порядка. Комбинатор — это замкнутое лямбда-выражение, то есть выражение, не содержащее свободных переменных. Комбинаторы можно комбинировать для передачи значений в нужные места в выражении, не присваивая им имена переменных.
Общая информация
Поскольку комбинаторы фиксированной точки могут использоваться для реализации рекурсии, их можно использовать для описания конкретных типов рекурсивных вычислений, таких как итерация фиксированной точки, итеративные методы, рекурсивное соединение в реляционных базах данных, анализ потоков данных, множества FIRST и FOLLOW нетерминалов в контекстно-свободной грамматике, транзитивное замыкание и другие типы операций замыкания. Функция, для которой каждый вход является фиксированной точкой, называется тождественной функцией. Формально: в отличие от всеобщей квантификации, комбинатор фиксированной точки конструирует одно значение, которое является фиксированной точкой. Замечательное свойство комбинатора фиксированной точки заключается в том, что он конструирует фиксированную точку для произвольной заданной функции. Другие функции обладают особым свойством: после однократного применения дальнейшие применения не оказывают никакого эффекта. Более формально: такие функции называются идемпотентными (см. также Проекция (математика)). Примером такой функции является функция, возвращающая 0 для всех четных целых чисел и 1 для всех нечетных целых чисел. В лямбда-исчислении, с вычислительной точки зрения, применение комбинатора фиксированной точки к тождественной функции или идемпотентной функции обычно приводит к бесконечному вычислению. Например, мы получаем, где полученный член может быть сведен только к самому себе и представляет собой бесконечный цикл. Комбинаторы фиксированной точки не обязательно существуют в более строгих моделях вычислений. Например, они не существуют в просто типизированном лямбда-исчислении. Комбинатор Y позволяет определить рекурсию как набор правил переписывания, не требуя встроенной поддержки рекурсии в языке. В языках программирования, поддерживающих анонимные функции, комбинаторы фиксированной точки позволяют определять и использовать анонимные рекурсивные функции, то есть без необходимости привязывать такие функции к идентификаторам. В этом контексте использование комбинаторов фиксированной точки иногда называют анонимной рекурсией.
In contrast to universal quantification over all , a fixed point combinator constructs one value that is a fixed point of The remarkable property of a fixed point combinator is that it constructs a fixed point for an arbitrary given function
Other functions have the special property that, after being applied once, further applications don't have any effect. More formally:
Such functions are called idempotent (see also Projection (mathematics)). An example of such a function is the function that returns 0 for all even integers, and 1 for all odd integers. In lambda calculus, from a computational point of view, applying a fixed point combinator to an identity function or an idempotent function typically results in non terminating computation. For example, we obtain
where the resulting term can only reduce to itself and represents an infinite loop. Fixed point combinators do not necessarily exist in more restrictive models of computation. For instance, they do not exist in simply typed lambda calculus. The Y combinator allows recursion to be defined as a set of rewrite rules, without requiring native recursion support in the language. In programming languages that support anonymous functions, fixed point combinators allow the definition and use of anonymous recursive functions, i. e. without having to bind such functions to identifiers. In this setting, the use of fixed point combinators is sometimes called anonymous recursion.