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

'''Каррирование''' или '''карринг''' (от {{lang-en|currying}}), виногда — [[информатика|информатике]]''карринг'') — преобразование функции от многих аргументов в набор функций, каждая из которых является функцией от одного аргумента. Возможность такого преобразования впервые отмечена в трудах [[Фреге, Фридрих Людвиг Готлоб|Готтлоба Фреге]], систематически изучена [[Шейнфинкель, Моисей Эльевич|Моисеем Шейнфинкелем]] в 1920-е годы, а наименование получило по имени [[Карри, Хаскелл|Хаскелла Карри]]  — разработчика [[Комбинаторная логика|комбинаторной логики]], в которой сведение к функциям одного аргумента носит основополагающий характер.

Для функции двух аргументов <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>.

Таким образом, <math>\Lambda</math>  — функция типа <math>(A \times B \to C) \to (A \to (B \to C))</math>.

{{Якорь|Декаррирование}}'''''Декаррирование''''' ({{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]]. Все языки, поддерживающие [[Замыкание (программирование)|замыкание]], позволяют записывать каррированные функции.

В [[Теоретическая информатика|теоретической информатике]] каррирование предоставляет способ изучения функций нескольких аргументов в рамках очень простых теоретических систем, таких как [[лямбда-исчисление]]. В рамках [[теория множеств|теории множеств]], каррирование — это соответствие между множествами <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>  — [[Импликация|импликации]]). Функции каррирования и декаррирования [[Непрерывность по Скотту|непрерывны по Скотту]].