каррирование

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

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

В прототипном примере все начинается с функции $f:(X\times Y)\to Z$ это принимает два аргумента, один из $X$ и один из $Y,$ и производит объекты в $Z.$ Каррированная форма этой функции рассматривает первый аргумент как параметр, чтобы создать семейство функций. $f_{x}:Y\to Z.$ Семейство устроено так, что для каждого объекта $x$ в $X,$ есть ровно одна функция $f_{x}.$

В этом примере ${\mbox{curry}}$ сама становится функцией, которая принимает $f$ в качестве аргумента и возвращает функцию, которая отображает каждый $x$ к $f_{x}.$ Правильная нотация для выражения этого — многословная. Функция $f$ принадлежит набору функций $(X\times Y)\to Z.$ Тем временем, $f_{x}$ принадлежит набору функций $Y\to Z.$ Таким образом, что-то, что отображает $x$ к $f_{x}$ будет типа $X\to [Y\to Z].$ С помощью этого обозначения ${\mbox{curry}}$ — это функция, которая принимает объекты из первого набора и возвращает объекты из второго набора, поэтому пишут ${\mbox{curry}}:[(X\times Y)\to Z]\to (X\to [Y\to Z]).$ Это несколько неформальный пример; более точные определения того, что подразумевается под «объектом» и «функцией», приведены ниже. Эти определения варьируются от контекста к контексту и принимают разные формы в зависимости от теории, над которой работает человек.

Каррирование связано с частичным применением , но не совпадает с ним . Приведенный выше пример можно использовать для иллюстрации частичного применения; это очень похоже. Частичное применение — это функция ${\mbox{apply}}$ для этого нужна пара $f$ и $x$ вместе в качестве аргументов и возвращает $f_{x}.$ Используя те же обозначения, что и выше, частичное применение имеет подпись ${\mbox{apply}}:([(X\times Y)\to Z]\times X)\to [Y\to Z].$ Написанное таким образом приложение можно считать сопряженным с каррированием.

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

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

Понятие каррирования было введено Готтлобом Фреге , разработанный Моисеем Шёнфинкелем , и далее развит Haskell Curry .

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

Мотивация

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

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

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

История

Слово «Карри» в слове «Карри» является отсылкой к логику Хаскеллу Карри , который широко использовал эту концепцию, но Моисею Шенфинкелю за шесть лет до Карри. идея пришла в голову Было предложено альтернативное название «Шенфинкелизация». В математическом контексте этот принцип можно проследить до работы Фреге в 1893 году .

Происхождение слова «карри» неясно. Дэвид Тернер говорит, что это слово было придумано Кристофером Стрейчи в его конспектах лекций 1967 года « Фундаментальные концепции языков программирования» . но этот источник представляет концепцию как «устройство, созданное Шёнфинкелем», и термин «каррирование» не используется, тогда как Карри упоминается позже в контексте функций высшего порядка. Джон К. Рейнольдс дал определение «карри» в статье 1972 года, но не утверждал, что придумал этот термин.

Определение

Каррирование легче всего понять, начав с неформального определения, которое затем можно адаптировать для множества различных областей. Прежде всего, необходимо установить некоторые обозначения. Обозначения $X\to Y$ обозначает все функции из $X$ к $Y$. Если $f$ есть такая функция, пишем $f\colon X\to Y$. Позволять $X\times Y$ обозначим упорядоченные пары элементов $X$ и $Y$ соответственно, то есть произведение декартово $X$ и $Y$. Здесь, $X$ и $Y$ могут быть множествами, типами или объектами других типов, как описано ниже.

Дана функция

$f\colon (X\times Y)\to Z$,

каррирование создает новую функцию

$g\colon X\to (Y\to Z)$.

То есть, $g$ принимает аргумент типа $X$ и возвращает функцию типа $Y\to Z$. Это определяется

$g(x)(y)=f(x,y)$

для $x$ типа $X$ и $y$ типа $Y$. Затем мы также пишем

${\text{curry}}(f)=g.$

Uncurrying — это обратное преобразование, и его легче всего понять с точки зрения его правого сопряженного — функции $\operatorname {apply} .$

Теория множеств

В теории множеств обозначение $Y^{X}$ используется для обозначения множества функций из множества $X$ на съемочную площадку $Y$. Каррирование — это естественная биекция между множеством $A^{B\times C}$ функций из $B\times C$ к $A$, и набор $(A^{C})^{B}$ функций из $B$ к набору функций из $C$ к $A$. В символах:

$A^{B\times C}\cong (A^{C})^{B}$

Действительно, именно эта естественная биекция оправдывает экспоненциальное обозначение множества функций. Как и во всех случаях каррирования, приведенная выше формула описывает присоединенную пару функторов : для каждого фиксированного набора $C$, функтор $B\mapsto B\times C$ остается сопряженным с функтором $A\mapsto A^{C}$.

В множеств объект категории $Y^{X}$ называется экспоненциальным объектом .

Функциональные пространства

В теории функциональных пространств , например, в функциональном анализе или теории гомотопий , обычно интересуются непрерывными функциями между топологическими пространствами . Один пишет ${\text{Hom}}(X,Y)$ ( функтор Hom ) для множества всех функций из $X$ к $Y$и использует обозначение $Y^{X}$ для обозначения подмножества непрерывных функций. Здесь, ${\text{curry}}$ это биекция

${\text{curry}}:{\text{Hom}}(X\times Y,Z)\to {\text{Hom}}(X,{\text{Hom}}(Y,Z)),$

в то время как uncurrying - это обратная карта. Если набор $Y^{X}$ непрерывных функций из $X$ к $Y$ задана компактно-открытая топология и если пространство $Y$ локально компактен по Хаусдорфу , то

${\text{curry}}:Z^{X\times Y}\to (Z^{Y})^{X}$

является гомеоморфизмом . Это также тот случай, когда $X$, $Y$ и $Y^{X}$ генерируются компактно , хотя случаев больше.

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

${\begin{aligned}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{aligned}}$

является непрерывным, когда $Y^{X}$ компактно-открыт и $Y$ локально компактный Хаусдорф. Эти два результата являются центральными для установления непрерывности гомотопии , т. е. когда $X$ это единичный интервал $I$, так что $Z^{I\times Y}\cong (Z^{Y})^{I}$ можно рассматривать либо как гомотопию двух функций из $Y$ к $Z$или, что то же самое, один (непрерывный) путь в $Z^{Y}$.

Алгебраическая топология

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

$[\Sigma X,Z]\approxeq [X,\Omega Z]$

где $[A,B]$ — множество гомотопических классов отображений $A\rightarrow B$, и $\Sigma A$ является подвеской A , и $\Omega A$ является петель A . пространством По сути, подвеска $\Sigma X$ можно рассматривать как декартово произведение $X$ с единичным интервалом по модулю отношения эквивалентности, чтобы превратить интервал в цикл. Каррированная форма затем отображает пространство $X$ в пространство функций из циклов в $Z$, то есть из $X$ в $\Omega Z$. Затем ${\text{curry}}$ — это присоединенный функтор , который отображает подвески в пространства петель, а uncurrying — двойственный функтор.

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

В гомологической алгебре связь между каррированием и некарингированием известна как присоединение тензорного хома . Здесь возникает интересный поворот: функтор Hom и функтор тензорного произведения могут не подняться до точной последовательности ; это приводит к определению функтора Ext и функтора Tor .

Теория предметной области

В теории порядка , то есть теории решеток множеств частично упорядоченных , ${\text{curry}}$ является непрерывной функцией , если решетке задана топология Скотта . Непрерывные по Скотту функции были впервые исследованы в попытке обеспечить семантику лямбда-исчисления (поскольку обычная теория множеств для этого не подходит). В более общем смысле, непрерывные по Скотту функции теперь изучаются в теории предметной области , которая включает изучение денотационной семантики компьютерных алгоритмов. Обратите внимание, что топология Скотта сильно отличается от многих распространенных топологий, которые можно встретить в категории топологических пространств ; Топология Скотта обычно тоньше и не является трезвой .

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

Лямбда-исчисления

В теоретической информатике каррирование дает возможность изучать функции с несколькими аргументами в очень простых теоретических моделях, таких как лямбда-исчисление , в которых функции принимают только один аргумент. Рассмотрим функцию $f(x,y)$ принимая два аргумента и имея тип $(X\times Y)\to Z$, что следует понимать так, что x должен иметь тип $X$, y должен иметь тип $Y$, а сама функция возвращает тип $Z$. Каррированная форма f определяется как

${\text{curry}}(f)=\lambda x.(\lambda y.(f(x,y)))$

где $\lambda$ является абстрактором лямбда-исчисления. Поскольку карри принимает на вход функции типа $(X\times Y)\to Z$, можно сделать вывод, что сам тип карри

${\text{curry}}:((X\times Y)\to Z)\to (X\to (Y\to Z))$

Оператор → часто считается правоассоциативным , поэтому тип каррированной функции $X\to (Y\to Z)$ часто пишется как $X\to Y\to Z$. И наоборот, применение функции считается левоассоциативным , так что $f(x,y)$ эквивалентно

$(({\text{curry}}(f)\;x)\;y)={\text{curry}}(f)\;x\;y$.

То есть круглые скобки не требуются для устранения неоднозначности порядка приложения.

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

Теория типов

В теории типов общая идея системы типов в информатике формализуется в конкретную алгебру типов. Например, при написании $f\colon X\to Y$, намерение состоит в том, что $X$ и $Y$ являются типами , а стрелка $\to$ — это конструктор типа , в частности, тип функции или тип стрелки. Аналогично, декартово произведение $X\times Y$ типов создается конструктором продукта типа $\times$.

Теоретико-типовый подход выражен в таких языках программирования, как ML , а также в языках, производных от него и вдохновленных им: CaML , Haskell и F# .

Теоретико-типический подход обеспечивает естественное дополнение к языку теории категорий , как обсуждается ниже. Это связано с тем, что категории, и в частности, моноидальные категории , имеют внутренний язык , причем просто типизированное лямбда-исчисление наиболее ярким примером такого языка является . Это важно в этом контексте, поскольку его можно построить на основе конструктора одного типа — типа стрелки. Затем каррирование наделяет язык естественным типом продукта. Соответствие между объектами в категориях и типах затем позволяет переинтерпретировать языки программирования как логику (через соответствие Карри-Ховарда ) и как другие типы математических систем, как описано ниже.

Логика

В соответствии с соответствием Карри-Ховарда существование каррирования и некарингирования эквивалентно логической теореме. $((A\land B)\to C)\Leftrightarrow (A\to (B\to C))$ (также известный как экспорт ), поскольку кортежи ( тип продукта ) соответствуют конъюнкции в логике, а тип функции соответствует импликации.

Экспоненциальный объект $Q^{P}$ в категории алгебр Гейтинга обычно записывается как материальная импликация $P\to Q$. Дистрибутивные алгебры Гейтинга являются булевыми алгебрами , а экспоненциальный объект имеет явный вид $\neg P\lor Q$, тем самым давая понять, что экспоненциальный объект на самом деле является материальной импликацией .

Теория категорий

Вышеупомянутые понятия каррирования и некаррирования находят свое наиболее общее и абстрактное утверждение в теории категорий . Каррирование является универсальным свойством экспоненциального объекта и приводит к присоединению в декартовых замкнутых категориях . То есть существует естественный изоморфизм между морфизмами бинарного произведения $f\colon (X\times Y)\to Z$ и морфизмы экспоненциального объекта $g\colon X\to Z^{Y}$.

Это обобщается до более широкого результата в закрытых моноидальных категориях : Каррирование — это утверждение, что тензорное произведение и внутренний Hom являются сопряженными функторами ; то есть для каждого объекта $B$ существует естественный изоморфизм :

$\mathrm {Hom} (A\otimes B,C)\cong \mathrm {Hom} (A,B\Rightarrow C).$

Здесь Hom обозначает (внешний) Hom-функтор всех морфизмов категории, а $B\Rightarrow C$ обозначает внутренний функтор hom в замкнутой моноидальной категории. Для категории множеств это одно и то же. Когда произведение является декартовым произведением, тогда внутреннее hom $B\Rightarrow C$ становится экспоненциальным объектом $C^{B}$.

Каррирование может сломаться одним из двух способов. Один из них — если категория не является замкнутой и, следовательно, не имеет внутреннего функтора hom (возможно, потому, что для такого функтора существует более одного выбора). Другой способ — если он не является моноидальным и, следовательно, не имеет произведения (то есть не имеет способа записи пар объектов). Категории, которые имеют как продукты, так и внутренние homs, являются в точности закрытыми моноидальными категориями.

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

Разница между этими двумя заключается в том, что произведение для декартовых категорий (таких как категории множеств , полные частичные порядки или алгебры Гейтинга ) является просто декартовым произведением ; он интерпретируется как упорядоченная пара элементов (или список). Просто типизированное лямбда-исчисление является внутренним языком декартовых замкнутых категорий; и именно по этой причине пары и списки являются основными в теории типов LISP типами , Scheme и многих функциональных языков программирования .

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

Контраст с применением частичной функции

Основная статья: Частичное применение

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

Дана функция типа $f\colon (X\times Y\times Z)\to N$, карри производит ${\text{curry}}(f)\colon X\to (Y\to (Z\to N))$. То есть, хотя оценку первой функции можно представить как $f(1,2,3)$, оценка каррированной функции будет представлена ​​как $f_{\text{curried}}(1)(2)(3)$, применяя каждый аргумент по очереди к функции с одним аргументом, возвращенной предыдущим вызовом. Обратите внимание, что после вызова $f_{\text{curried}}(1)$, у нас остается функция, которая принимает один аргумент и возвращает другую функцию, а не функция, которая принимает два аргумента.

Напротив, применение частичной функции относится к процессу фиксации ряда аргументов функции, в результате чего создается другая функция меньшей арности. Учитывая определение $f$ выше, мы могли бы исправить (или «привязать») первый аргумент, создав функцию типа ${\text{partial}}(f)\colon (Y\times Z)\to N$. Вычисление этой функции можно представить как $f_{\text{partial}}(2,3)$. Обратите внимание, что результатом применения частичной функции в этом случае является функция, принимающая два аргумента.

Интуитивно понятно, что применение частичных функций говорит: «Если вы зафиксируете первый аргумент функции, вы получите функцию остальных аргументов». Например, если функция div обозначает операцию деления x / y , то div с параметром x, фиксированным равным 1 (т. е. div 1), является другой функцией: такой же, как функция inv , которая возвращает мультипликативную обратную величину своего аргумента, определенного по inv ( y ) знак равно 1/ y .

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

Частичное применение можно рассматривать как оценку каррированной функции в фиксированной точке, например, заданной $f\colon (X\times Y\times Z)\to N$ и $a\in X$ затем ${\text{curry}}({\text{partial}}(f)_{a})(y)(z)={\text{curry}}(f)(a)(y)(z)$ или просто ${\text{partial}}(f)_{a}={\text{curry}}_{1}(f)(a)$ где ${\text{curry}}_{1}$ карри первый параметр f.

Таким образом, частичное применение сводится к каррированной функции в фиксированной точке. Кроме того, каррированная функция в фиксированной точке (тривиально) является частичным применением. Для дальнейшего доказательства отметим, что для любой функции $f(x,y)$, функция $g(y,x)$ можно определить так, что $g(y,x)=f(x,y)$. Таким образом, любое частичное применение может быть сведено к одной операции карри. Таким образом, карри более уместно определить как операцию, которая во многих теоретических случаях часто применяется рекурсивно, но которая теоретически неотличима (если рассматривать ее как операцию) от частичного применения.

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

См. также

• Присоединение Тензор-хом
• Ленивая оценка
• Замыкание (информатика)
• см  ​
  n   теорема
• Замкнутая моноидальная категория