Каррирование

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Определение[править | править вики-текст]

Для функции двух аргументов оператор каррирования выполняет преобразование — берёт аргумент типа и возвращает функцию типа . С интуитивной точки зрения, каррирование функции позволяет фиксировать её некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, — функция типа .

Декаррирование (англ. uncurring) вводится как обратное преобразование — восстанавливающее каррированный аргумент: для функции оператор декаррирования выполняет преобразование ; тип оператора декаррирования — .

На практике каррирование позволяет рассматривать функцию, которая получила не все из предусмотренных аргументов. Оператор каррирования встроен в некоторые языки программирования, что позволяет многоместные функции приводить к каррированному представлению, наиболее характерные примеры таких языков — ML и Haskell. Все языки, поддерживающие замыкание, позволяют записывать каррированные функции.

Математическая точка зрения[править | править вики-текст]

В теоретической информатике каррирование предоставляет способ изучения функций нескольких аргументов в рамках очень простых теоретических систем, таких как лямбда-исчисление. В рамках теории множеств, каррирование — это соответствие между множествами и . В теории категорий каррирование появляется благодаря универсальному свойству экспоненциала; в ситуации декартово замкнутой категории это приводит к следующему соответствию. Существует биекция между множествами морфизмов из бинарного произведения и морфизмами в экспоненциал , которая естественна по и по . Это утверждение эквивалентно тому, что функтор произведения и функтор Hom — сопряжённые функторы.

Это является ключевым свойством декартово замкнутой категории, или, более общо, замкнутой моноидальной категории. Первой вполне достаточно для классической логики, однако вторая является удобной теоретической основой для квантовых вычислений. Различие состоит в том, что декартово произведение содержит только информацию о паре двух объектов, тогда как тензорное произведение, используемое в определении моноидальной категории, подходит для описания запутанных состояний[1].

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

Примечания[править | править вики-текст]

  1. John c. Baez and Mike Stay, «Physics, Topology, Logic and Computation: A Rosetta Stone», (2009) ArXiv 0903.0340 in New Structures for Physics, ed. Bob Coecke, Lecture Notes in Physics vol. 813, Springer, Berlin, 2011, pp. 95-174.

Литература[править | править вики-текст]