Комбинатор неподвижной точки

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

Неподвижной точкой некоторой функции $f$ называется значение $x$ такое, что $f(x) = x$ . Например, значения $0$ и $1$ являются неподвижными точками функции $f(x) = x^2$ , поскольку $f(0) = 0$ и $f(1) = 1$ . Тогда как неподвижная точка функций первого порядка (то есть функций на «простых» значениях, таких как целые числа) является значением первого порядка, для функций высших порядков неподвижными точками являются другие функции, то есть $f(g) = g$ , где $g$ — неподвижная точка (сама по себе функция) функции $f$ . Принимая это во внимание, комбинатором неподвижной точки называется специальная функция $fix$ :

f (fix (f)) = fix (f)

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

Один из самых известных (и, вероятно, из самых простых) комбинаторов неподвижной точки в нетипизированном λ-исчислении называется комбинатором Y. Он был разработан Хаскеллом Карри и определяется следующим образом:

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

Необходимо отметить, что комбинатор Y предназначен для использования совместно с вычислительной стратегией «вызов по имени», поскольку выражение (Y g) зацикливается для произвольного g в стратегии «вызов по значению».

Комбинатор неподвижной точки в строгих и нестрогих языках[править | править код]

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

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

Например, в языке программирования Standard ML вариант комбинатора Y для вызова по значению имеет тип ∀a.∀b.((a → b) → (a → b)) → (a → b), в то время как вариант для вызова по имени имеет тип ∀a.(a → a) → a. Вариант для вызова по имени зацикливается при применении в строгих языках, поскольку любое применение Y f всегда разворачивается в f (Y f). Далее вычисляется аргумент внешней функции f, как того требуется стратегия вызова по значению, и получается значение f (f (Y f)). Этот процесс будет продолжаться до бесконечности, но значение этого применения получено никогда не будет.

Пример[править | править код]

Рассмотрим функцию для вычисления факториала (в нотации А. Чёрча). Обычное рекурсивное математическое определение выглядит так:

fact (n) = if n = 0 then 1 else n * fact (n - 1)

Можно рассмотреть один шаг вычисления этой рекурсии в нотации λ-исчисления:

F = λf.λx.(ISZERO x) 1 (MULT x (f (PRED x)))

где «f» — параметр для получения функции вычисления факториала. Функция F вычисляет один шаг рекурсии в вышеприведённой формуле. При применении к ней комбинатора неподвижной точки fix получится следующая последовательность выражений:

fix (F) (n) = F (fix (F)) (n)

fix (F) (n) = λx.(ISZERO x) 1 (MULT x (fix (F) (PRED x))) (n)

fix (F) (n) = (ISZERO n) 1 (MULT n (fix (F) (PRED n)))

Далее можно переименовать применение fix (F) в fact, а потому:

fact (n) = (ISZERO n) 1 (MULT n (fact (PRED n)))

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

Другие комбинаторы неподвижной точки[править | править код]

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

Z = λf.(λx.f(λy.xxy))(λx.f(λy.xxy))

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

Y = S(K(SII))(S(S(KS)K)(K(SII)))

Простейший (требующий наименьшее количество базовых комбинаторов для разложения в базисе) комбинатор неподвижной точки в базисе SK, найденный Д. Тромпом:

Y' = SSK(S(K(SS(S(SSK))))K)

Эта запись соответствует следующему λ-выражению:

Y' = (λx.λy.xyx)(λy.λx.y(xyx))

Другой комбинатор неподвижной точки найден А. Тьюрингом:

Θ = (λx.λy.(y(xxy)))(λx.λy.(y(xxy)))

Этот комбинатор также имет простую форму для вызова по значению:

Θ_v = (λx.λy.(y(λz.xxyz)))(λx.λy.(y(λz.xxyz)))

Комбинаторы неподвижной точки встречаются не так редко (их вообще существует бесконечное множество). Некоторые используются в качестве развлечений (терм L встречается в нём 26 раз):

Y_k = (LLLLLLLLLLLLLLLLLLLLLLLLLL)

где:

L = λabcdefghijklmnopqstuvwxyzr.(r(thisisafixedpointcombinator))

См. также[править | править код]

Внешние ссылки[править | править код]

На английском языке[править | править код]