Кіріспе
Категориялар теориясындағы категорияның түрі. Категориялар теориясында, егер екі объектінің туындысы бойынша анықталған кез келген морфизмді, осы объектілердің біреуі бойынша анықталған морфизммен табиғи түрде сәйкестендіруге болады, онда бұл категория Картезиан жабық категориясы деп аталады. Бұл категориялар математикалық логика және бағдарламалау теориясында ерекше маңызға ие, себебі олардың ішкі тілі – қарапайым типтелген лямбда-есептеуі. Олар сызықтық типтік жүйелерді ішкі тіл ретінде қолданатын, кванттық және классикалық есептеулерге қолайлы жабық моноидалдық категориялармен жалпыланады.
In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.
Этимология
Француз философы, математигі және ғалымы (1596–1650) құрметіне аталған, оның аналитикалық геометрияны жасауы Картезиандық көбейту ұғымын тудырды, бұл кейіннен категориялық көбейту түсінігіне дейін жалпыландырылды.
Қолданбалар
Картезиялық жабық санаттарда "екі айнымалы функциясы" (морфизм f: X×Y → Z) әрқашан "бір айнымалы функциясы" (морфизм λf: X → ZY) түрінде көрсетілуі мүмкін. Компьютер ғылымында бұл Currying деп аталады; осының арқасында жай типтелген лямбда-есептеуді кез келген Картезиялық жабық санатта интерпретациялауға болады. Curry-Howard-Lambek сәйкестігі интуиционистік логика, жай типтелген лямбда-есептеу және Картезиялық жабық санаттар арасындағы терең изоморфизмді қамтамасыз етеді. Кейбір Картезиялық жабық санаттар, топостар, дәстүрлі жиын теориясының орнына математиканың жалпы ортасы ретінде ұсынылған. Компьютер ғалымы Джон Бэкус айнымалысыз жазбаны немесе Функциялық деңгейде бағдарламалауды жақтады, ол кейіннен Картезиялық жабық санаттардың ішкі тілімен ұқсас екені байқалды. CAML саналы түрде Картезиялық жабық санаттарға негізделген.
Тәуелді сома және өнім
C жергілікті Картезиандық жабық санаты болсын. C-де барлық кері шегінулер бар, себебі Z кодомені бар екі жебенің кері шегінуі C/Z-дегі көбейтіндімен беріледі. Кез келген p: X → Y жебе үшін P, C/Y-дегі сәйкес объектіні белгілесін. P арқылы кері шегінуді алу p* функторын береді: C/Y → C/X, ол сол және оң жақ қосымшаға ие. Сол жақ қосымша тәуелді сома деп аталады және құрастыру арқылы беріледі. Оң жақ қосымша тәуелді көбейтінді деп аталады. P-нің C/Y-дегі экспоненциалы тәуелді көбейтінді арқылы келесі формуламен өрнектеледі. Бұл атаулардың себебі, P-ні тәуелді тип ретінде қарастырғанда, функторлар типі құру операцияларына сәйкес келеді, яғни және сәйкесінше.
The right adjoint is called the dependent product. The exponential by P in C/Y can be expressed in terms of the dependent product by the formula
The reason for these names is because, when interpreting P as a dependent type , the functors and correspond to the type formations and respectively.