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

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

Формально, если ${\textrm {fix}}$ представляет собой комбинатор с фиксированной точкой, а функция $f$ имеет одну или несколько неподвижных точек, то ${\textrm {fix}}\ f$ является одной из этих неподвижных точек, т.е.

$f\ ({\textrm {fix}}\ f)={\textrm {fix}}\ f\ .$

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

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

В классическом нетипизированном лямбда-исчислении каждая функция имеет фиксированную точку. Конкретная реализация ${\textrm {fix}}$ - это Хаскеля Карри , заданный формулой парадоксальный комбинатор Y

$Y=\lambda f.\ (\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

(Здесь мы используем стандартные обозначения и соглашения лямбда-исчисления: Y — функция, которая принимает один аргумент f и возвращает все выражение после первой точки; выражение $\lambda x.f\ (x\ x)$ обозначает функцию, которая принимает один аргумент x , рассматриваемый как функция, и возвращает выражение $f\ (x\ x)$, где $(x\ x)$ обозначает x, примененный к самому себе. Сопоставление выражений обозначает применение функции, является левоассоциативным и имеет более высокий приоритет, чем точка.)

Проверка

Следующий расчет подтверждает, что $Yg$ действительно является фиксированной точкой функции $g$:

$Y\ g\$	$=(\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))\ g\ \ \$	по определению $Y$
	$=(\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x))\$	путем β-редукции : замена формального аргумента f функции Y фактическим аргументом g
	$=g\ ((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))\$	путем β-редукции: замена формального аргумента x первой функции фактическим аргументом $(\lambda x.g\ (x\ x))$
	$=g\ (Y\ g)$	по второму равенству выше

Лямбда-терм $g\ (Y\ g)$ вообще говоря, не может β-редуцироваться к члену $Y\ g$. Однако, как показано, оба термина β-сводятся к одному и тому же термину.

Использует

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

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

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

Пример реализации

Ниже представлен пример реализации Y-комбинатора на двух языках.

# Y Combinator in Python

Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))

Y(Y)

// Y Combinator in C++, using C++ 14 extensions

int main() {
    auto Y = [](auto f) {
        auto f1 = [f](auto x) -> decltype(f) {
            return f(x(x));
        };
        return f1(f1);
    };

    Y(Y);
}

Обратите внимание, что обе эти программы, хотя формально и корректны, на практике бесполезны; они оба выполняются бесконечно, пока не завершатся из-за переполнения стека . В более общем плане, поскольку и Python, и C++ используют строгие вычисления , комбинатор Y обычно бесполезен в этих языках; см. ниже комбинатор Z, который можно использовать в строгих языках программирования .

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

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

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

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

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

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

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

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

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

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

Многие функции не имеют фиксированных точек, например $f:\mathbb {N} \to \mathbb {N}$ с $f(n)=n+1$. Используя кодировку Чёрча , натуральные числа можно представить в лямбда-исчислении, и эту функцию f можно определить в лямбда-исчислении. Однако его домен теперь будет содержать все лямбда-выражения, а не только те, которые представляют натуральные числа. Комбинатор Y, примененный к f , даст фиксированную точку для f , но эта фиксированная точка не будет представлять собой натуральное число. При попытке вычислить Y f на реальном языке программирования произойдет бесконечный цикл.

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

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

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

Определение термина «комбинатор»

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

определения и комбинаторы с

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

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

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

$\operatorname {fact} \ n={\begin{cases}1&{\text{if}}~n=0\\n\times \operatorname {fact} (n-1)&{\text{otherwise.}}\end{cases}}$

где n — неотрицательное целое число. Если мы хотим реализовать это в лямбда-исчислении, где целые числа представляются с использованием кодировки Чёрча , мы столкнемся с проблемой, заключающейся в том, что лямбда-исчисление не позволяет использовать имя функции («факт») в определении функции. Это можно обойти, используя комбинатор с фиксированной точкой. ${\textsf {fix}}$ следующее.

Определите функцию F двух аргументов f и n :

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

(Здесь $(\operatorname {IsZero} \ n)$ — это функция, которая принимает два аргумента и возвращает свой первый аргумент, если n = 0, и второй аргумент в противном случае; $\operatorname {pred} \ n$ оценивается как n -1.)

Теперь определите $\operatorname {fact} ={\textsf {fix}}\ F$. Затем $\operatorname {fact}$ является фиксированной точкой F , что дает

${\begin{aligned}\operatorname {fact} n&=F\ \operatorname {fact} \ n\\&=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\operatorname {pred} \ n)))\ \end{aligned}}$

по желанию.

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

Комбинатор Y, открытый Хаскеллом Б. Карри , определяется как

$Y=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$

Другие комбинаторы

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

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

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

Дополнительные комбинаторы ( система B, C, K, W ) позволяют дать гораздо более короткое определение. С $U=SII$ комбинатор для самостоятельного применения, поскольку $S(Kx)yz=x(yz)=Bxyz$ и $Sx(Ky)z=xzy=Cxyz$, вышеизложенное становится

$Y=S(KU)(SB(KU))=BU(CBU)$

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

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

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

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

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

$X=\lambda f.(\lambda x.xx)(\lambda x.f(xx))$

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

$\Theta =(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))$

Его преимущество перед $Y$ это что $\Theta \ f$ бета-редуцирует до $f\ (\Theta f)$, тогда как $Y\ f$ и $f\ (Yf)$ только бета-приведение к общему термину.

$\Theta$ также имеет простую форму вызова по значению:

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

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

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

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

$Zgv=g(Zg)v\ .$

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

$Z=\lambda f.(\lambda x.f(\lambda v.xxv))\ (\lambda x.f(\lambda v.xxv))\ .$

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

Если F — комбинатор с фиксированной точкой в ​​нетипизированном лямбда-исчислении, то мы имеем

$F=\lambda x.Fx=\lambda x.x(Fx)=\lambda x.x(x(Fx))=\cdots$

Термы, которые имеют то же дерево Бема, что и комбинатор с фиксированной точкой, т. е. имеют такое же бесконечное расширение. $\lambda x.x(x(x\cdots ))$, называются нестандартными комбинаторами с фиксированной точкой . Любой комбинатор с фиксированной точкой также является нестандартным, но не все нестандартные комбинаторы с фиксированной точкой являются комбинаторами с фиксированной точкой, поскольку некоторые из них не удовлетворяют уравнению с фиксированной точкой, которое определяет «стандартные». Эти комбинаторы называются строго нестандартными комбинаторами с фиксированной точкой ; примером является следующий комбинатор:

$N=BM(B(BM)B)$

где

$B=\lambda xyz.x(yz)$

$M=\lambda 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

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

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

$f\ (f...(f\ ({\mathsf {fix}}\ f))...)\ x$.

Эту проблему можно решить, определив fix с помощью дополнительного параметра.

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" *)

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

(define Y!
  (lambda (f)
    ((lambda (i)                       
       (set! i (f (lambda (x) (i x)))) ;; (set! i expr) assigns i the value of expr
       i)                              ;; replacing it in the present lexical scope
     #f)))

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

$(Y_{!}\ \lambda x.e)e'=(\lambda x.e)\ (Y_{!}\ \lambda x.e)e'$

В более идиоматичном современном использовании Lisp это обычно обрабатывается с помощью метки с лексической областью действия (метки с лексической областью действия). let выражение), поскольку лексическая область видимости не была введена в Лисп до 1970-х годов:

(define Y*
  (lambda (f)
    ((lambda (i)
       (let ((i (f (lambda (x) (i x))))) ;; (let ((i expr)) i) locally defines i as expr
	     i))                             ;; non-recursively: thus i in expr is not expr
     #f)))

Или без внутренней метки:

(define Y
  (lambda (f)
    ((lambda (i) (i i))
     (lambda (i)
       (f (lambda (x)
	        (apply (i i) x)))))))

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

Этот пример представляет собой слегка интерпретирующую реализацию комбинатора с фиксированной точкой. Класс используется для хранения функции исправления , называемой 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);

Набираю

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

∀а.(а → а) → а

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

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

В просто типизированном лямбда-исчислении комбинатору Y с фиксированной точкой нельзя присвоить тип потому что в какой-то момент это будет касаться подтермина о самостоятельном применении $x~x$ по правилу применения:

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

где $x$ имеет бесконечный тип $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)))

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

Поскольку комбинаторы с фиксированной точкой могут использоваться для реализации рекурсии, их можно использовать для описания конкретных типов рекурсивных вычислений, например, итерации с фиксированной запятой , итеративных методов , рекурсивного соединения в реляционных базах данных , анализа потока данных , FIRST и СЛЕДУЙТЕ наборам нетерминалов в контекстно-свободной грамматике , транзитивном замыкании и других типах операций замыкания .

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

$\forall x(f\ x=x)$

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

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

$\forall x(f\ (f\ x)=f\ x)$

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

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

$(Y\ \lambda x.x)=(\lambda x.(xx)\ \lambda x.(xx))$

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

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

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

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

См. также

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

Ссылки

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

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

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