В математике и информатике в целом фиксированная точка функции - это значение, которое функция отображает сама себе. В комбинаторной логике для информатики комбинатор с фиксированной точкой (или комбинатор с фиксированной точкой ) [1] : стр. 26 является функцией высшего порядка. который возвращает некоторую фиксированную точку своей функции аргумента, если таковая существует.
Формально, если функция f имеет одну или несколько неподвижных точек, то
и, следовательно, при повторном применении
Y комбинатор
В классическом нетипизированном лямбда-исчислении каждая функция имеет фиксированную точку. Частной реализацией исправления является парадоксальный комбинатор Карри Y , представленный
- [2] : 131 [примечание 1] [примечание 2]
В функциональном программировании комбинатор Y может использоваться для формального определения рекурсивных функций на языке программирования, который не поддерживает рекурсию.
Этот комбинатор можно использовать для реализации парадокса Карри . Суть парадокса Карри заключается в том, что нетипизированное лямбда-исчисление нецелесообразно как дедуктивная система, и комбинатор Y демонстрирует это, позволяя анонимному выражению представлять ноль или даже множество значений. Это противоречит математической логике.
Применительно к функции с одной переменной комбинатор Y обычно не завершается. Более интересные результаты получаются при применении комбинатора Y к функциям двух или более переменных. Вторая переменная может использоваться как счетчик или индекс. Результирующая функция ведет себя как цикл while или for в императивном языке.
При таком использовании комбинатор Y реализует простую рекурсию. В лямбда-исчислении невозможно сослаться на определение функции в теле функции. Рекурсия может быть достигнута только путем передачи функции в качестве параметра. Y комбинатор демонстрирует этот стиль программирования.
Комбинатор с фиксированной точкой
Y комбинатор является реализацией с фиксированной точкой комбинатора в лямбда - исчислении. Комбинаторы с фиксированной точкой также могут быть легко определены в других функциональных и императивных языках. Реализация в лямбда-исчислении сложнее из-за ограничений в лямбда-исчислении.
Комбинатор с фиксированной точкой может использоваться в различных областях,
- Общая математика
- Нетипизированное лямбда-исчисление
- Типизированное лямбда-исчисление
- Функциональное программирование
- Императивное программирование
Комбинаторы с фиксированной точкой могут применяться к ряду различных функций, но обычно не завершаются, если нет дополнительного параметра. Когда функция, которую необходимо исправить, обращается к своему параметру, вызывается другой вызов функции, поэтому расчет никогда не начинается. Вместо этого дополнительный параметр используется для запуска вычисления.
Тип фиксированной точки - это тип возвращаемого значения фиксируемой функции. Это может быть реальный, функциональный или любой другой тип.
В нетипизированном лямбда-исчислении функция, к которой применяется комбинатор с фиксированной точкой, может быть выражена с использованием кодирования, например кодирования Черча . В этом случае определенные лямбда-термины (которые определяют функции) рассматриваются как значения. «Запуск» (бета-сокращение) комбинатора с фиксированной точкой при кодировании дает лямбда-член для результата, который затем может быть интерпретирован как значение с фиксированной точкой.
В качестве альтернативы функцию можно рассматривать как лямбда-член, определенный исключительно в лямбда-исчислении.
Эти разные подходы влияют на то, как математик и программист могут рассматривать комбинатор с фиксированной точкой. Математик лямбда-исчисления может рассматривать комбинатор Y, примененный к функции, как выражение, удовлетворяющее уравнению с фиксированной точкой, и, следовательно, как решение.
Напротив, человек, желающий применить комбинатор с фиксированной точкой только к некоторой общей задаче программирования, может рассматривать его только как средство реализации рекурсии.
Ценности и домены
Каждое выражение имеет одно значение. Это верно для общей математики и должно быть верно для лямбда-исчисления. Это означает, что в лямбда-исчислении применение комбинатора с фиксированной точкой к функции дает выражение, значение которого является фиксированной точкой функции.
Однако это значение в области лямбда-исчисления , оно может не соответствовать какому-либо значению в области определения функции, поэтому в практическом смысле оно не обязательно является фиксированной точкой функции, и только в области лямбда-исчисления является это неподвижная точка уравнения.
Например, рассмотрим,
Деление чисел со знаком может быть реализовано в кодировке Чёрча, поэтому f может быть представлено лямбда-членом. Это уравнение не имеет решения в действительных числах. Но в области комплексных чисел i и -i являются решениями. Это показывает, что могут быть решения уравнения в другой области. Однако лямбда-член для решения вышеуказанного уравнения более странный, чем это. Лямбда-членпредставляет состояние, в котором x может быть либо i, либо -i , как одно значение. Информация, различающая эти два значения, была потеряна при смене домена.
Для математика лямбда-исчисления это является следствием определения лямбда-исчисления. Для программиста это означает, что бета-сокращение лямбда-члена будет повторяться бесконечно, никогда не достигнув нормальной формы.
Функция против реализации
Комбинатор с фиксированной точкой может быть определен в математике, а затем реализован на других языках. Общая математика определяет функцию на основе ее экстенсиональных свойств. [3] То есть две функции равны, если они выполняют одно и то же отображение. Лямбда-исчисление и языки программирования рассматривают идентичность функций как интенсиональное свойство. Идентичность функции зависит от ее реализации.
Функция (или термин) лямбда-исчисления - это реализация математической функции. В лямбда-исчислении существует ряд комбинаторов (реализаций), которые удовлетворяют математическому определению комбинатора с фиксированной точкой.
Что такое комбинатор?
Комбинаторная логика - это теория функций высшего порядка . Комбинатор является закрытым лямбда - выражение, а это означает , что он не имеет свободных переменных. Комбинаторы можно комбинировать, чтобы направлять значения на их правильные места в выражении, даже не называя их переменными.
Использование в программировании
Комбинаторы с фиксированной точкой могут использоваться для реализации рекурсивного определения функций. Однако в практическом программировании они используются редко. [4] Сильно нормализующие системы типов, такие как просто типизированное лямбда-исчисление, запрещают незавершение, и, следовательно, комбинаторам с фиксированной точкой часто не может быть назначен тип или требуются функции системы сложных типов. Кроме того, комбинаторы с фиксированной точкой часто неэффективны по сравнению с другими стратегиями реализации рекурсии, поскольку они требуют большего числа сокращений функций и построения и разделения кортежа для каждой группы взаимно рекурсивных определений. [1] : стр. 232
Факториальная функция
Факториальная функция представляет собой хороший пример того, как можно применить комбинатор с фиксированной точкой. Результат демонстрирует простую рекурсию, которая была бы реализована в одном цикле на императивном языке. Определение используемых чисел объясняется в кодировке Чёрча . Функция, принимающая себя в качестве параметра, выглядит так:
Это дает YF n как,
Параметр дает,
Это определение ставит F в роли тела цикла, который будет повторяться, и эквивалентно математическому определению факториала:
Комбинаторы с фиксированной точкой в лямбда-исчислении
Y комбинатор, обнаруженный Haskell B. Curry , определяется следующим образом:
Бета-сокращение этого дает,
(по определению Y ) | ||
(путем β-редукции λf: применено Y к g) | ||
(путем β-редукции λx: применена левая функция к правой функции) | ||
(по второму равенству) |
Повторно применяя это равенство, получаем
Обратите внимание, что приведенное выше равенство следует рассматривать как последовательность многоступенчатых β-редукций слева направо. Лямбда-член не может, как правило, β-сводиться к термину . Знаки равенства можно интерпретировать как β-эквивалентности вместо многошаговых β-редукций, позволяющих двигаться в обоих направлениях.
Эквивалентное определение комбинатора с фиксированной точкой
Этот комбинатор с фиксированной точкой может быть определен как y in,
Выражение для y может быть получено с использованием правил из определения выражения let . Во-первых, используя правило,
дает,
Также используя,
дает
Затем, используя правило сокращения эта ,
дает,
Вывод комбинатора Y
Комбинатор Y Карри легко получить из определения y . [5] Начиная с,
Лямбда-абстракция не поддерживает ссылку на имя переменной в применяемом выражении, поэтому x необходимо передать в качестве параметра переменной x . Мы можем думать об этом как о замене x на xx , но формально это неверно. Вместо определения y с помощью дает,
Выражение let можно рассматривать как определение функции y , где z - параметр. Создание экземпляра z как y в вызове дает,
И потому, что параметр z всегда передает функцию y .
Используя правило сокращения эта ,
дает,
Выражение пусть может быть выражено в виде лямбда - абстракции , используя,
дает,
Возможно, это простейшая реализация комбинатора с фиксированной точкой в лямбда-исчислении. Однако одно бета-сокращение дает более симметричную форму Y-комбинатора Карри.
См. Также перевод между let и лямбда-выражениями .
Другие комбинаторы с фиксированной точкой
В нетипизированном лямбда-исчислении комбинаторы с фиксированной точкой не особенно редки. На самом деле их бесконечно много. [6] В 2005 году Майер Голдберг показал, что множество комбинаторов с фиксированной точкой нетипизированного лямбда-исчисления рекурсивно перечислимо . [7]
Y комбинатор может быть выражено в SKI-исчислении как
Простейший комбинатор с фиксированной точкой в SK-исчислении, найденный Джоном Тромпом , - это
хотя учтите, что он не в нормальном виде, который длиннее. Этот комбинатор соответствует лямбда-выражению
Следующий комбинатор с фиксированной точкой проще, чем комбинатор Y, и β-сводится к комбинатору Y; его иногда называют самим комбинатором Y:
Другой распространенный комбинатор с фиксированной точкой - это комбинатор с фиксированной точкой Тьюринга (названный в честь его первооткрывателя Алана Тьюринга ): [8] [2] : 132
Его преимущество перед в том, что бета-сводится к , [примечание 3], тогда как а также только бета-сводить к общему члену. [заметка 2]
также есть простая форма вызова по значению:
Аналог для взаимной рекурсии является polyvariadic неподвижной точки комбинатора , [9] [10] [11] , которые могут быть обозначен Y *.
Строгий комбинатор с фиксированной точкой
В языке строгого программирования комбинатор Y будет расширяться до переполнения стека или никогда не останавливаться в случае оптимизации хвостового вызова. [12] Z комбинатор будет работать в строгих языках (называемых также стремятся языки, где применяются аппликативный порядок оценки). У комбинатора Z явно определен следующий аргумент, предотвращающий расширение Z g в правой части определения: [13]
а в лямбда-исчислении это эта-расширение комбинатора Y :
Нестандартные комбинаторы с фиксированной точкой
В нетипизированном лямбда-исчислении есть термы, которые имеют то же дерево Бёма , что и комбинатор с фиксированной точкой, то есть они имеют такое же бесконечное расширение λx.x (x (x ...)). Они называются нестандартными комбинаторами с фиксированной точкой . Любой комбинатор с фиксированной точкой также является нестандартным, но не все нестандартные комбинаторы с фиксированной точкой являются комбинаторами с фиксированной точкой, потому что некоторые из них не удовлетворяют уравнению, которое определяет «стандартные». Эти странные комбинаторы называются строго нестандартными комбинаторами с неподвижной точкой ; примером является следующий комбинатор;
где,
Множество нестандартных комбинаторов с фиксированной точкой не рекурсивно перечислимо. [7]
Реализация на других языках
Обратите внимание, что комбинатор Y - это конкретная реализация комбинатора с фиксированной точкой в лямбда-исчислении. Его структура определяется ограничениями лямбда-исчисления. Нет необходимости или полезно использовать эту структуру при реализации комбинатора с фиксированной точкой на других языках.
Ниже приведены простые примеры комбинаторов с фиксированной точкой, реализованных в некоторых парадигмах программирования .
Ленивая функциональная реализация
В языке, поддерживающем ленивое вычисление , например в Haskell , можно определить комбинатор с фиксированной точкой, используя определяющее уравнение комбинатора с фиксированной точкой, которое носит условное название fix
. Поскольку Haskell имеет ленивые типы данных, этот комбинатор также можно использовать для определения фиксированных точек конструкторов данных (а не только для реализации рекурсивных функций). Здесь дано определение, за которым следуют некоторые примеры использования. Исходный пример в Hackage: [14]
fix , fix ' :: ( a -> a ) -> a fix f = let x = f x in x - Лямбда отброшена. Совместное использование. - Исходное определение в Data.Function. - альтернатива: fix ' f = f ( fix' f ) - Лямбда снята. Не делиться.fix ( \ x -> 9 ) - это равно 9fix ( \ x -> 3 : x ) - вычисляет ленивый бесконечный список [3,3,3, ...]fact = fix fac - возвращает факториальную функцию, где fac f 0 = 1 fac f x = x * f ( x - 1 )факт 5 - оценивается в 120
Строгая функциональная реализация
На строгом функциональном языке аргумент функции f заранее раскрывается, давая бесконечную последовательность вызовов:
- .
Это может быть решено путем определения исправления с дополнительным параметром.
let rec fix f x = f ( fix f ) x (* обратите внимание на лишний x; здесь fix f = \ x-> f (fix f) x *)let factabs fact = function (* factabs имеет дополнительный уровень лямбда-абстракции *) 0 -> 1 | x -> x * факт ( x - 1 )let _ = ( fix factabs ) 5 (* оценивается как "120" *)
Реализация императивного языка
Этот пример представляет собой слегка интерпретируемую реализацию комбинатора с фиксированной точкой. Класс используется для содержания функции исправления , называемой fixer . Исправляемая функция содержится в классе, наследуемом от fixer. Функция fix обращается к функции, которая должна быть зафиксирована как виртуальная функция. Что касается строгого функционального определения, fix явно задается дополнительным параметром x , что означает, что ленивое вычисление не требуется.
шаблон < typename R , typename D > class fixer { public : R fix ( D x ) { return f ( x ); } частный : виртуальный R f ( D ) = 0 ; }; факт класса : public fixer < long , long > { virtual long f ( long x ) { if ( x == 0 ) { return 1 ; } return x * fix ( x -1 ); } };длинный результат = факт (). fix ( 5 );
В императивно-функциональном языке, таком как Lisp , Scheme или Racket , Ландин (1963) [ требуется полная цитата ] предлагает использовать присвоение переменной для создания комбинатора с фиксированной точкой:
( определить Y! ( lambda ( f-maker ) (( lambda ( f ) ( set! f ( f-maker ( lambda ( x ) ( f x )))) ;; оператор присваивания f ) 'NONE )))
Используя лямбда-исчисление с аксиомами для операторов присваивания, можно показать, что Y! удовлетворяет тому же закону фиксированной точки, что и комбинатор Y с вызовом по значению: [15] [16]
Печатать
В полиморфном лямбда-исчислении ( Система F ) полиморфный комбинатор с фиксированной точкой имеет тип [ необходима цитата ] ;
- ∀a. (A → a) → a
где a - переменная типа . То есть fix принимает функцию, которая отображает a → a и использует ее для возврата значения типа a.
В простом типизированном лямбда-исчислении, расширенном с помощью рекурсивных типов , могут быть написаны операторы с фиксированной точкой, но тип «полезного» оператора с фиксированной точкой (тот, чье приложение всегда возвращает) может быть ограничен.
В простом типизированном лямбда-исчислении комбинатору с фиксированной точкой Y нельзя присвоить тип [17], потому что в какой-то момент он будет иметь дело с подчленом самоприменения по правилу применения:
где имеет бесконечный тип . Фактически невозможно типизировать комбинатор с фиксированной точкой; в этих системах любая поддержка рекурсии должна быть явно добавлена к языку.
Тип для комбинатора Y
В языках программирования, поддерживающих рекурсивные типы , можно ввести комбинатор Y, соответствующим образом учитывая рекурсию на уровне типа. Необходимость самоприменения переменной x может быть устранена с помощью типа (Rec a), который определен как изоморфный (Rec a -> a).
Например, в следующем коде Haskell у нас есть In
и out
- имена двух направлений изоморфизма с типами: [18] [19]
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:
введите ' a recc = In of ( ' a recc -> ' a ) let out ( In x ) = xпусть 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 наборов нетерминалов в контекстно-свободной грамматике , транзитивном замыкании и других типах операций замыкания .
Функция, для которой каждый вход является фиксированной точкой, называется функцией идентичности . Формально:
В отличие от универсального количественного определения по всем комбинатор с фиксированной точкой создает одно значение, которое является фиксированной точкой. Замечательное свойство комбинатора неподвижной точки состоит в том, что он строит неподвижную точку для произвольной заданной функции.
Другие функции обладают особым свойством, согласно которому после однократного применения дальнейшие приложения не имеют никакого эффекта. Более формально:
Такие функции называются идемпотентными (см. Также проекцию ). Примером такой функции является функция, которая возвращает 0 для всех четных целых чисел и 1 для всех нечетных целых чисел.
В лямбда-исчислении с вычислительной точки зрения применение комбинатора с фиксированной точкой к функции идентичности или идемпотентной функции обычно приводит к непрерывному вычислению. Например, получаем
где полученный член может сводиться только к самому себе и представляет собой бесконечный цикл.
Комбинаторы с фиксированной точкой не обязательно существуют в более ограничительных моделях вычислений. Например, их не существует в просто типизированном лямбда-исчислении .
Y комбинатор позволяет рекурсию можно определить как набор правил перезаписи , [20] , не требуя встроенную поддержку рекурсии в языке. [21]
В языках программирования, поддерживающих анонимные функции , комбинаторы с фиксированной точкой позволяют определять и использовать анонимные рекурсивные функции , то есть без необходимости связывать такие функции с идентификаторами . В этом случае использование комбинаторов с фиксированной точкой иногда называется анонимной рекурсией . [примечание 4] [22]
Смотрите также
- Итерация с фиксированной точкой
- Анонимная функция
- Лямбда-исчисление
- Пусть выражение
- Лямбда-лифтинг
Заметки
- ^ В этой статьедля сохранения скобок используютсясинтаксические правила, приведенные в Лямбда-исчислении # Обозначения .
- ^ a b Для произвольного лямбда-члена f свойство фиксированной точки может быть подтверждено путем бета-уменьшения левой и правой части: , где а также обозначают синтаксическое равенство по определению и бета-редукцию соответственно. Аналогично первым двум шагам получаем . Поскольку оба условия а также можно свести к одному и тому же сроку, они равны.
- ^
- ^ Эта терминология, по-видимому, в основном фольклорная , но в следующих случаях она встречается:
- Трей Нэш, Accelerated C # 2008 , Apress, 2007, ISBN 1-59059-873-3 , стр. 462–463. В основном заимствовано из блога Уэса Дайера (см. Следующий пункт).
- Анонимная рекурсия Уэса Дайера в C # от 2 февраля 2007 г. содержит в основном аналогичный пример, найденный в книге выше, но с дополнительным обсуждением.
Рекомендации
- ^ а б Пейтон Джонс, Саймон Л. (1987). Реализация функционального программирования . Prentice Hall International.
- ^ а б Хенк Барендрегт (1985). Лямбда-исчисление - его синтаксис и семантика . Исследования по логике и основам математики. 103 . Амстердам: Северная Голландия. ISBN 0444867481.
- ^ Селинджер, Питер. «Конспект лекций по лямбда-исчислению (PDF)» . п. 6.
- ^ «Для тех из нас, кто не знает, что такое Y-Combinator и почему он полезен…» Hacker News . Дата обращения 2 августа 2020 .
- ^ "абстрактная алгебра - Может ли кто-нибудь объяснить Y-комбинатор?" . Обмен математическими стеками .
- ^ Бимбо, Каталин (27 июля 2011 г.). Комбинаторная логика: чистая, прикладная и типизированная . п. 48. ISBN 9781439800010.
- ^ а б Голдберг, 2005
- ^ Алан Мэтисон Тьюринг (декабрь 1937 г.). "The-функция в --конверсия ». Журнал символической логики . 2 (4): 164. JSTOR 2268281 .
- ^ «Многогранность комбинатора с фиксированной точкой» . okmij.org .
- ^ Поливариадный Y в чистом Haskell98 Архивировано 4 марта 2016 г. в Wayback Machine , lang.haskell.cafe, 28 октября 2003 г.
- ^ "рекурсия - комбинатор с фиксированной точкой для взаимно рекурсивных функций?" . Переполнение стека .
- ^ Бене, Адам (17 августа 2017 г.). «Комбинаторы с фиксированной точкой в JavaScript» . Bene Studio . Средний . Дата обращения 2 августа 2020 .
- ^ "CS 6110 S17 Лекция 5. Рекурсия и комбинаторы с фиксированной точкой" (PDF) . Корнельский университет . 4.1 Комбинатор с фиксированной точкой CBV.
- ^ Исходное определение в Data.Function .
- ^ Фелляйзен, Маттиас (1987). Исчисление Lambda-v-CS . Университет Индианы.
- ^ Талкотт, Кэролайн (1985). Сущность рома: теория интенсиональных и экстенсиональных аспектов вычислений типа Lisp (докторская диссертация). Стэндфордский Университет.
- ^ Введение в лямбда - исчислении Архивированных 2014-04-08 в Wayback Machine
- ^ Haskell список рассылки нить на Как определить Y комбинатор в Haskell , 15 сентября 2006
- ^ Геверс, Герман; Веркоелен, Йоп. О комбинаторах с фиксированной точкой и зацикливании в теории типов . CiteSeerX 10.1.1.158.1478 .
- ^ Дэниел П. Фридман , Маттиас Фелляйзен (1986). «Глава 9 - Лямбда The Ultimate». Маленький Лиспер . Научно-исследовательские партнеры . п. 179. «В этой главе мы вывели Y-комбинатор, который позволяет нам писать рекурсивные функции с одним аргументом без использования define».
- ^ Майк Ванье. «Комбинатор Y (небольшой возврат) или: как добиться успеха в рекурсии без реальной рекурсии» . Архивировано из оригинала на 2011-08-22. «В более общем плане Y дает нам способ получить рекурсию на языке программирования, который поддерживает первоклассные функции, но не имеет встроенной рекурсии».
- ↑ If Works, производящие комбинатор Y , 10 января 2008 г.
- Вернер Клюге, Абстрактные вычислительные машины: перспектива лямбда-исчисления , Springer, 2005, ISBN 3-540-21146-2 , стр. 73–77
- Майер Голдберг, (2005) О рекурсивной перечислимости комбинаторов с фиксированной точкой , Отчет БРИКС RS-05-1, Орхусский университет
- Маттиас Фелляйзен . Лекция по Why из Y .
Внешние ссылки
- [1]
- [2]
- Y комбинатор
- "Лекция о том, почему Y"
- «Использование Y-комбинатора в Ruby»
- «Функциональное программирование на Аде»
- Код Розетты - Y комбинатор