Каррирование: различия между версиями

1382 байта добавлено ,  5 лет назад
оформление формул, формулировки, менее многобуквенно, +кое-какие добавки по идеям из Англовики
(→‎Примеры: список примеров помечен, за время пометки --- не мотивирован обобщающими источниками, стало быть удалён)
(оформление формул, формулировки, менее многобуквенно, +кое-какие добавки по идеям из Англовики)
'''Каррирование''' или '''карринг''' ({{lang-en|currying}}) в [[информатика|информатике]] — преобразование функции от многих аргументов в функцию, берущую свои аргументы по одному. ЭтоВозможность преобразованиетакого былопреобразования введеновпервые [[М.отмечена Шейнфинкель|М. Шейнфинкелем]]в итрудах [[Фреге, Фридрих Людвиг Готлоб|Г.Готтлоба Фреге]], исистематически получилоизучена свое[[Шейнфинкель, названиеМоисей Эльевич|Моисеем Шейнфинкелем]] в честь1920-е годы, а наименование получило по имени [[Карри, Хаскелл|Х.Хаскелла Карри]] — разработчика [[Комбинаторная логика|комбинаторной логики]], в которой сведение к функциям одного аргумента носит основополагающий характер.
 
== Определение ==
Для функции ''h''двух типааргументов ''<math>h :\colon (A ×\times B) \to C''</math> оператор каррирования ''Λ''<math>\Lambda</math> выполняет преобразование ''Λ<math>\Lambda(h) :\colon A \to (B \to C)</math> — берёт аргумент типа <math>A</math> и возвращает функцию типа <math>(B \to C)''</math>.
С интуитивной точки зрения, каррирование функции позволяет фиксировать еееё некоторый аргумент, возвращая функцию от остальных аргументов.
Таким образом, ''Λ(h)'' берет аргумент типа ''A'' и возвращает функцию типа ''B → C''.
Таким образом, <math>\Lambda</math> — функция типа <math>(A \times B \to C) \to (A \to (B \to C))</math>.
С интуитивной точки зрения, каррирование функции позволяет фиксировать ее некоторый аргумент, возвращая функцию от остальных аргументов.
Таким образом, ''Λ'' представляет собой функцию типа ''Λ : (A × B → C) → (A → (B → C))''.
 
{{Якорь|Декаррирование}}'''''Декаррирование''''' ({{lang-en|uncurring}}) вводится как обратное преобразование — восстанавливающее каррированный аргумент: для функции <math>k \colon A \to (B \to C)</math> оператор декаррирования <math>\epsilon</math> выполняет преобразование <math>\epsilon(k) \colon A \times B \to C</math>; тип оператора декаррирования — <math>(A \to (B \to C)) \to (A \times B \to C)</math>.
'''Декаррирование''' вводится как обратное преобразование.
 
На практике каррирование позволяет рассматривать функцию, которая получила одинне все из аргументов,предусмотренных но не всеаргументов. Оператор каррирования встроен в некоторые языки программирования, что позволяет многоместные функции приводить к каррированному представлению., Примеромнаиболее служатхарактерные языкипримеры таких языков — [[ML]] и [[Haskell]]. Все языки, поддерживающие [[Замыкание (программирование)|замыкание]], позволяют записывать каррированные функции.
В другом смысле, преобразование ''ε'', противоположное каррированию, восстанавливает каррированный аргумент.
Для функции ''k'' типа ''k : A → (B → C)'' оператор ''ε'' типа ''ε: (U → V) × U → V'' для произвольных ''a: A'', ''U = A'', ''V = B → C''
выполняет преобразование ''ε[k, a]: B → C''. Остаётся положить ''k = Λ(h)'', и для ''ε: (A →(B → C)) × A → (B → C)'' записываем ''ε[Λ(h), a]: B → C'' и ''ε[k, a] = ε[Λ(h), a]'', что устанавливает связь между каррированой и некаррированной записью функции<ref>Wolfengagen, V.E. ''[http://vew.0catch.com/books/Wolfengagen_CLP-2003-En.djvu Combinatory logic in programming.] Computations with objects through examples and exercises''. — 2-nd ed. — M.: «Center JurInfoR» Ltd., 2003. — x+337 с. ISBN 5-89158-101-9.</ref>.
 
На практике каррирование позволяет рассматривать функцию, которая получила один из аргументов, но не все. Оператор каррирования встроен в некоторые языки программирования, что позволяет многоместные функции приводить к каррированному представлению. Примером служат языки [[ML]] и [[Haskell]]. Все языки, поддерживающие [[Замыкание (программирование)|замыкание]], позволяют записывать каррированные функции.
 
== Математическая точка зрения ==
В теоретической информатике каррирование предоставляет способ изучения функций нескольких аргументов в рамках очень простых теоретических систем, таких как [[лямбда-исчисление]]. В рамках [[теория множеств|теории множеств]], каррирование — это соответствие между множествами <math>\scriptstyle C^{A\times B}</math> и <math>\scriptstyle\left(C^B\right)^A</math>. В [[теория категорий|теории категорий]] каррирование появляется благодаря [[универсальное свойство|универсальному свойству]] [[экспоненциал]]а; в ситуации [[декартово замкнутая категория|декартово замкнутой категории]] это приводит к следующему соответствию. Существует биекция между множествами морфизмов из бинарного [[произведение (теория категорий)|произведения]] <math>\scriptstyle f \colon (X \times Y) \to Z </math> и морфизмами в экспоненциал <math>\scriptstyle g \colon X \to Z^Y </math>, которая [[естественное преобразование|естественна]] по <math>X</math> и по <math>Z</math>. Это утверждение эквивалентно тому, что функтор произведения и [[функтор Hom]] — сопряженныесопряжённые функторы.
 
Это является ключевым свойством декартово замкнутой категории, или, более общо, [[замкнутая моноидальная категория|замкнутой моноидальной категории]]. Первой вполне достаточно для классической логики, однако вторая является удобной теоретической основой для [[квантовый компьютер|квантовых вычислений]]. Различие состоит в том, что декартово произведение содержит только информацию о паре двух объектов, тогда как тензорное произведение, используемое в определении [[моноидальная категория|моноидальной категории]], подходит для описания [[квантовая запутанность|запутанных состояний]]<ref>John c. Baez and Mike Stay, «[http://math.ucr.edu/home/baez/rosetta/rose3.pdf Physics, Topology, Logic and Computation: A Rosetta Stone]», (2009) [http://arxiv.org/abs/0903.0340/ ArXiv 0903.0340] in ''New Structures for Physics'', ed. Bob Coecke, ''Lecture Notes in Physics'' vol. '''813''', Springer, Berlin, 2011, pp. 95-174.</ref>.
 
С точки зрения [[Соответствие Карри — Ховарда|соответствия Карри — Ховарда]] существование функций каррирования (обитаемость типа <math>((A \times B) \to C) \to (A \to (B \to C)</math> и декаррирования (обитаемость типа <math>(A \to (B \to C) \to ((A \times B) \to C)</math>) эквивалентно логическому утверждению <math>((A \and B) \Rightarrow C) \Leftrightarrow (A \Rightarrow (B \Rightarrow C))</math> ([[тип-произведение]] <math>A \times B</math> соответствует [[Конъюнкция|конъюнкции]], а [[функциональный тип]] <math>A \to B</math> — [[Импликация|импликации]]). Функции каррирования и декаррирования [[Непрерывность по Скотту|непрерывны по Скотту]].
 
== Примечания ==
{{примечания}}
 
== См. такжеЛитература ==
* {{книга
* [[Переопределение функции]]
|автор = Бенджамин Пирс
 
|заглавие = Типы в языках программирования
== Ссылки ==
|место =
|издательство = [[Добросвет]]
|ответственный = Пер. с англ.: Г. Бронников, А. Отт
|год = 2011
|страниц = 656
|страницы = 76
|серия =
|isbn = 978-5-7913-0082-9
|тираж =
}}
* {{книга
| заглавие = Homotopy Type Theory: Univalent Foundations of Mathematics
| часть = Type theory
| ссылка = http://homotopytypetheory.org/book/
| викитека =
| место = [[Принстон (Нью-Джерси)|Princeton]]
| издательство = [[Институт перспективных исследований|Institute for Advanced Study]]
| год = 2013
| allpages = 603
| isbn =
| тираж =
| ref = HoTT
}}
 
[[Категория:Функциональное программирование]]
[[Категория:Лямбда-исчисление]]
[[Категория:Статьи с примерами кода C++]]
[[Категория:Статьи с примерами кода D]]
[[Категория:Статьи с примерами кода Erlang]]
[[Категория:Статьи с примерами кода JavaScript]]
[[Категория:Статьи с примерами кода Haskell]]
[[Категория:Статьи с примерами кода PHP]]
[[Категория:Статьи с примерами кода Ruby]]
[[Категория:Статьи с примерами кода Python]]