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

1 байт добавлено ,  2 года назад
м
Бот: замена устаревшего математического синтаксиса в соответствии с mw:Extension:Math/Roadmap
(уборка)
м (Бот: замена устаревшего математического синтаксиса в соответствии с mw:Extension:Math/Roadmap)
Это является ключевым свойством [[Декартово замкнутая категория|декартово замкнутой категории]], или, более общей, [[замкнутая моноидальная категория|замкнутой моноидальной категории]]. Первой вполне достаточно для классической логики, однако вторая является удобной теоретической основой для [[квантовый компьютер|квантовых вычислений]]. Различие состоит в том, что декартово произведение содержит только информацию о паре двух объектов, тогда как тензорное произведение, используемое в определении [[моноидальная категория|моноидальной категории]], подходит для описания [[квантовая запутанность|запутанных состояний]]<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 \andland B) \Rightarrow C) \Leftrightarrow (A \Rightarrow (B \Rightarrow C))</math> ([[тип-произведение]] <math>A \times B</math> соответствует [[Конъюнкция|конъюнкции]], а [[функциональный тип]] <math>A \to B</math> — [[Импликация|импликации]]). Функции каррирования и декаррирования [[Непрерывность по Скотту|непрерывны по Скотту]].
 
== Каррирование с точки зрения програмирования ==