Каррирование
Преобразование функции таким образом, чтобы она принимала только один аргумент

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

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

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

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

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

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

Концепция каррирования была введена Готтлобом Фреге [4] [ 5], развита Моисеем Шёнфинкелем [6] [ 5] [7] [8] [9] [10] [11] и далее развита Хаскеллом Карри [8] [10] [12] [13]

Декаррирование — это двойственное преобразование к каррированию, и его можно рассматривать как форму дефункционализации . Оно берет функцию , возвращаемое значение которой — другая функция , и выдает новую функцию , которая принимает в качестве параметров аргументы для обоих и , и возвращает в качестве результата применение и впоследствии, , к этим аргументам. Процесс можно повторять. ф {\displaystyle f} г {\displaystyle г} ф ′ {\displaystyle f'} ф {\displaystyle f} г {\displaystyle г} ф {\displaystyle f} г {\displaystyle г}

Мотивация

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

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

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

История

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

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

Определение

Каррирование проще всего понять, начав с неформального определения, которое затем можно будет сформулировать так, чтобы оно подходило для многих различных областей. Во-первых, необходимо установить некоторую нотацию. Нотация обозначает все функции от до . Если — такая функция, мы пишем . Пусть обозначают упорядоченные пары элементов и соответственно, то есть декартово произведение и . Здесь и могут быть множествами, или они могут быть типами, или они могут быть другими видами объектов, как будет рассмотрено ниже. Х → И {\displaystyle X\to Y} Х {\displaystyle X} И {\displaystyle Y} ф {\displaystyle f} ф : Х → И {\displaystyle f\двоеточие от X до Y} Х × И {\displaystyle X\times Y} Х {\displaystyle X} И {\displaystyle Y} Х {\displaystyle X} И {\displaystyle Y} Х {\displaystyle X} И {\displaystyle Y}

Дана функция

ф : ( Х × И ) → З {\displaystyle f\двоеточие (X\times Y)\to Z} ,

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

г : Х → ( И → З ) {\displaystyle g\двоеточие X\to (Y\to Z)} .

То есть принимает аргумент типа и возвращает функцию типа . Он определяется как г {\displaystyle г} Х {\displaystyle X} И → З {\displaystyle Y\to Z}

г ( х ) ( у ) = ф ( х , у ) {\displaystyle g(x)(y)=f(x,y)}

для типа и типа . Затем мы также пишем х {\displaystyle x} Х {\displaystyle X} у {\displaystyle у} И {\displaystyle Y}

карри ( ф ) = г . {\displaystyle {\text{карри}}(f)=g.}

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

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

В теории множеств для обозначения набора функций из множества в множество используется нотация . Каррирование — это естественная биекция между набором функций из в и набором функций из в набором функций из в . В символах: И Х {\displaystyle Y^{X}} Х {\displaystyle X} И {\displaystyle Y} А Б × С {\displaystyle A^{B\times C}} Б × С {\displaystyle B\times C} А {\displaystyle А} ( А С ) Б {\displaystyle (A^{C})^{B}} Б {\displaystyle Б} С {\displaystyle С} А {\displaystyle А}

А Б × С ≅ ( А С ) Б {\displaystyle A^{B\times C}\cong (A^{C})^{B}}

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

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

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

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

карри : Хом ( Х × И , З ) → Хом ( Х , Хом ( И , З ) ) , {\displaystyle {\text{curry}}:{\text{Hom}}(X\times Y,Z)\to {\text{Hom}}(X,{\text{Hom}}(Y,Z)),}

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

карри : З Х × И → ( З И ) Х {\displaystyle {\text{карри}}:Z^{X\times Y}\to (Z^{Y})^{X}}

является гомеоморфизмом . Это также имеет место, когда , и компактно порождены , [ 17] : глава 5  [18] хотя есть и другие случаи. [19] [20] Х {\displaystyle X} И {\displaystyle Y} И Х {\displaystyle Y^{X}}

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

оценка : И Х × Х → И ( ф , х ) ↦ ф ( х ) {\displaystyle {\begin{align}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{align}}}

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

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

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

[ Σ Х , З ] ≊ [ Х , Ω З ] {\displaystyle [\Сигма X,Z]\approxeq [X,\Омега Z]}

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

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

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

Теория домена

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

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

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

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

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

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

curry : ( ( X × Y ) → Z ) → ( X → ( Y → Z ) ) {\displaystyle {\text{curry}}:((X\times Y)\to Z)\to (X\to (Y\to Z))}

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

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

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

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

Теория типов

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

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

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

Логика

Согласно соответствию Карри–Ховарда , существование каррирования и декаррирования эквивалентно логической теореме (также известной как экспорт ), поскольку кортежи ( тип продукта ) соответствуют конъюнкции в логике, а тип функции соответствует импликации. ( ( A ∧ B ) → C ) ⇔ ( A → ( B → C ) ) {\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}

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

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

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

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

H o m ( A ⊗ B , C ) ≅ H o m ( A , B ⇒ C ) . {\displaystyle \mathrm {Hom} (A\otimes B,C)\cong \mathrm {Hom} (A,B\Rightarrow C).}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Смотрите также

Ссылки

  1. ^ abc cdiggins (24 мая 2007 г.). «Каррирование != Обобщенное частичное применение?!». Lambda the Ultimate: The Programming Languages ​​Weblog .
  2. ^ abc "Partial Function Application is not Currying". The Uncarved Block . 7 августа 2020 г. Архивировано из оригинала 23 октября 2016 г.
  3. ^ ab Baez, John C.; Stay, Mike (6 июня 2009 г.). "Физика, топология, логика и вычисления: Розеттский камень". В Coecke, Bob (ред.). Новые структуры для физики (PDF) . Lecture Notes in Physics. Vol. 813: Новые структуры для физики. Berlin, Heidelberg: Springer (опубликовано 5 июля 2010 г.). стр.  95–172 . arXiv : 0903.0340 . doi :10.1007/978-3-642-12821-9_2. ISBN 978-3-642-12821-9. S2CID  115169297. Архивировано из оригинала (PDF) 5 декабря 2022 г.
  4. ^ аб Фреге, Готтлоб (1893). «§ 36». Grundgesetze der arithmetik (на немецком языке). Книга из коллекций Университета Висконсина в Мэдисоне, оцифрована Google 26 августа 2008 г. Йена: Герман Поле. стр.  54–55 .
  5. ^ abc Куайн, WV (1967). "Введение в работу Моисея Шёнфинкеля 1924 года "О строительных блоках математической логики"". В Ван Хейеноорт, Жан (ред.). От Фреге до Гёделя: Учебник по математической логике, 1879-1931 . Издательство Гарвардского университета. С.  355–357 . ISBN 9780674324497.
  6. ^ Шёнфинкель, Моисей (сентябрь 1924 г.) [Представлено в Mathematischen Gesellschaft (Математическом обществе) в Геттингене 7 декабря 1920 г. Получено в Mathematische Annalen 15 марта 1924 г.]. Написано в Москве. «Über die Bausteine ​​der mathematischen Logik» [О строительных блоках математической логики] (PDF) . Математические Аннален . 92 ( 3–4 ). Берлин?: Springer: 305–316 . doi : 10.1007/BF01448013. S2CID  118507515.
  7. ^ ab Strachey, Christopher (апрель 2000 г.) [Эта статья составляет суть курса лекций, прочитанных на Международной летней школе по программированию в Копенгагене в августе 1967 г.]. "Fundamental Concepts in Programming Languages". Higher-Order and Symbolic Computation . 13 : 11– 49. CiteSeerX 10.1.1.332.3161 . doi :10.1023/A:1010000313106. ISSN  1573-0557. S2CID  14124601. Существует устройство, созданное Шёнфинкелем, для сведения операторов с несколькими операндами к последовательному применению операторов с одним операндом. 
  8. ^ abc Первоначально опубликовано как Reynolds, John C. (1 августа 1972 г.). "Определительные интерпретаторы для языков программирования высшего порядка". В Shields, Rosemary (ред.). Труды ежегодной конференции ACM - ACM '72. Том 2. ACM Press. С.  717– 740. doi :10.1145/800194.805852. ISBN 9781450374927. S2CID  163294. В последней строке мы использовали трюк, называемый Каррированием (в честь логика Х. Карри), чтобы решить проблему введения бинарной операции в язык, где все функции должны принимать один аргумент. (Рефери замечает, что, хотя «Каррирование» звучит вкуснее, «Шенфинкелинг» может быть точнее.)Переиздано как Reynolds, John C. (1998). "Definitional Interpreters for Higher-Order Programming Languages". Вычисления высшего порядка и символьные вычисления . 11 (4). Бостон: Kluwer Academic Publishers: 363– 397. doi :10.1023/A:1010027404223. 13 – через Сиракузский университет: Колледж инженерии и компьютерных наук - Бывшие кафедры, центры, институты и проекты.
  9. ^ Slonneger, Kenneth; Kurtz, Barry L. (1995). "Curried Functions, 5.1: Concepts and Examples, Chapter 5: The Lambda Calculus". Формальный синтаксис и семантика языков программирования: лабораторный подход (PDF) . Addison-Wesley Publishing Company. стр. 144. ISBN 0-201-65697-3.
  10. ^ abc Curry, Haskell B. (1980). Barwise, Jon; Keisler, H. Jerome; Kunen, Kenneth (ред.). "Some Philosophical Aspects of Combinatory Logic". Симпозиум Клини: Труды симпозиума, состоявшегося 18-24 июня 1978 г. в Мэдисоне, Висконсин, США (Исследования по логике и основаниям математики) . Исследования по логике и основаниям математики. 101. North-Holland Publishing Company, выходной документ Elsevier: 85– 101. doi :10.1016/S0049-237X(08)71254-0. ISBN 9780444853455. ISSN  0049-237X. S2CID  117179133. Некоторые современные логики называют этот способ рассмотрения функции «каррированием», потому что я широко его использовал; но у Шёнфинкеля эта идея возникла примерно за 6 лет до меня.
  11. ^ "Currying Schonfinkelling". Portland Pattern Repository Wiki . Cunningham & Cunningham, Inc. 6 мая 2012 г.
  12. ^ Барендрегт, Хенк; Барендсен, Эрик (март 2000 г.) [декабрь 1998 г.]. Введение в лямбда-исчисление (PDF) (пересмотренная редакция). п. 8.
  13. ^ Карри, Хаскелл ; Фейс, Роберт (1958). Комбинаторная логика . Т. I (2-е изд.). Амстердам, Нидерланды: North-Holland Publishing Company.
  14. ^ Хаттон, Грэм; Джонс, Марк П., ред. (ноябрь 2002 г.). «Часто задаваемые вопросы по comp.lang.functional, 3. Технические темы, 3.2. Каррирование». Ноттингемский университет компьютерных наук .
  15. ^ Хайм, Ирен; Кратцер, Анжелика (2 января 1998 г.). Семантика в генеративной грамматике (PDF) . Молден, Массачусетс: Blackwell Publishers, отпечаток Wiley. ISBN 0-631-19712-5.{{cite book}}: CS1 maint: date and year (link)
  16. ^ Тернер, Дэвид (1 июня 1997 г.). "Язык программирования, каррирование или Шёнфинкелинг?, № 9 / 14". Computer Programming Language Forum . Архивировано из оригинала 3 марта 2022 г. . Получено 3 марта 2022 г. .
  17. ^ ab May, Jon Peter (1999). Краткий курс алгебраической топологии (PDF) . Чикагские лекции по математике. Чикаго, Иллинойс: Издательство Чикагского университета. С.  39–55 . ISBN 0-226-51183-9. OCLC  41266205.
  18. ^ "компактно порожденное топологическое пространство". nLab . 28 мая 2023 г.
  19. ^ Tillotson, J.; Booth, Peter I. (март 1980 г.) [Получено 2 октября 1978 г., пересмотрено 29 июня 1979 г., опубликовано 1 мая 1980 г.]. Написано в Мемориальном университете Ньюфаундленда. "Monoidal closed, Cartesian closed and comfortable categories of topological spaces" (PDF) . Pacific Journal of Mathematics . 88 (1). Беркли, Калифорния: Mathematical Sciences Publishers: 35– 53. doi :10.2140/pjm.1980.88.35. eISSN  1945-5844. ISSN  0030-8730.
  20. ^ "удобная категория топологических пространств". nLab . 11 августа 2023 г.
  21. ^ abc Ротман, Джозеф Джона (1988). "Глава 11". Введение в алгебраическую топологию. Выпускные тексты по математике; 119. Нью-Йорк: Springer-Verlag. ISBN 978-0-387-96678-6. OCLC  17383909.
  22. ^ Barendregt, Hendrik Pieter (1984). "Theorems 1.2.13, 1.2.14". Лямбда-исчисление: его синтаксис и семантика . Исследования по логике и основаниям математики. Т. 103 (Rev. ed.). North-Holland, отпечаток Elsevier. ISBN 978-0-444-87508-2.
  23. ^ Mac Lane, Saunders; Moerdijk, Ieke (1992). "Глава I. Категории функторов; разделы 7. Пропозициональное исчисление, 8. Алгебры Гейтинга и 9. Квантификаторы как сопряженные". Пучки в геометрии и логике: первое введение в теорию топосов . Нью-Йорк: Springer-Verlag, часть Springer Science & Business Media. стр.  48–57 . ISBN 978-0-387-97710-2.
  24. ^ Абрамски, Сэмсон; Коек, Боб (5 марта 2007 г.). "Категорическая семантика квантовых протоколов". Логика в компьютерных науках (LICS 2004): Труды, 19-й ежегодный симпозиум IEEE, Турку, Финляндия, 2004 г.] . IEEE Computer Society Press. стр.  415–425 . arXiv : quant-ph/0402130 . doi :10.1109/LICS.2004.1319636. ISBN 978-0-7695-2192-3.
  25. ^ Ли, Г. Кей (15 мая 2013 г.). «Функциональное программирование за 5 минут». Слайды .
Найдите информацию о каррировании в Викисловаре, бесплатном словаре.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Currying&oldid=1248022439"