Категорические вычисления
Feb. 22nd, 2012 07:09 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonА вот можно ли вычислить ответ на главный вопрос, пользуясь одной лишь теорией категорий? Оказывается, можно. Давным-давно в одной далекой галактике Tatsuya Hagino придумал язык CPL (Categorical Programming Language), а чуть менее давно другой японец Masahiro Sakai сделал годный его интерпретатор. Hagino свою реализацию делал на Лиспе, а Sakai догадался таки задействовать языки программирования - сперва Руби, затем Хаскель (ибо Руби медленный, на Хаскеле в сто раз быстрее заработало). И вот полный текст программы на CPL:
которая выводит результат
s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.zero
т.е. ровно 42.
Что же тут происходит? В CPL мы начинаем с чистого листа - там изначально нет ни базовых типов, ни каких-либо операций. Зато есть возможность определять универсальные категорные объекты (вот где настоящий объектно-ориентированный язык! :)). В категории у нас есть объекты и есть морфизмы между ними (они же стрелки), подчиняющиеся паре простых правил (наличие и ассоциативность композиции, наличие и годность identity - тождественного морфизма). Я сразу возьму несколько примеров, чтобы на них все примерять. Первый пример категории: объекты - типы данных функционального языка (int, bool, string, etc.), а морфизмы - функции (string_of_int : int -> string, succ : int -> int, etc.). Пример другой категории: объекты - логические высказывания, а стрелки показывают выводимость одного высказывания из другого (have_a_son -> have_a_child, А & B & C -> A...). Третий пример: объекты - натуральные числа, а стрелка соединяет два числа, если первое делится на второе (6 -> 3, 5 -> 5...). Мы можем придумывать какие-то универсальные объекты - они характеризуются наличием определенных связей с другими объектами категории, причем из всех аналогично связанных объектов они "самые-самые": всякий похожий объект связан с нашим уникальным морфизмом. Простейший пример - терминальный объект категории. Это такой объект, в который есть по уникальной стрелке из всех объектов категории. С т.з. универсальности это объект без особенных связей, но всякий похожий объект (а раз никаких особенностей не требуется, то любой объект категории) связан с ним уникальным морфизмом. На CPL это записывается так:
Здесь 1 - название определяемого объекта, ! - название для морфизма, связывающего любой похожий объект (т.е. в данном случае вообще любой объект) с 1, а "right" показывает направление для ! - определяемый объект стоит справа от стрелки:
! : X -> 1
для всех объектов Х.
В категории типов терминальный объект - тип (), он же unit, он же void. Из любого типа Т можно сделать функцию Т -> (), она и станет морфизмом "!". В категории логических высказываний терминальный объект - особое высказывание True, Истина, оно выводится из любого истинного высказывания (то бишь из всех). В категории натуральных чисел, где стрелки означают делимость, терминальный объект - это 1. Всякое натуральное число делится на 1.
Чуть сложнее, но в том же ключе выглядит произведение:
Объект АхВ (обозначенный тут как prod(a,b)) называется произведением объектов А и В, если из него есть стрелка в А, есть стрелка в В (обозначим их pi1 и pi2), и для любого похожего объекта С (т.е. из которого тоже есть стрелки в А и В) есть стрелка из С в наш объект АхВ. Ее назовем pair, а факт того, что определяемый объект в ней справа (pair: C -> AхB), отметим указанием "right". При этом должна работать ("коммутировать" - разные пути между двумя точками должны определять эквивалентные морфизмы) такая диаграмма:
(пунктиром обозначен морфизм, существование которого должно вытекать из существования стрелок, показанных сплошными линиями)
В категории типов данных произведение типов А и В - это тупл (А,В). Стрелки pi1 и pi2 - это функции fst и snd. Если из некоторого типа С тоже есть две стрелки (функции)
fa :: C -> A
fb :: C -> B
то можно сделать функцию
pair_fa_fb :: C -> (A,B)
pair_fa_fb c = (fa c, fb c)
В категории логических высказываний произведение - это связка И (&). Правила избавления от И выглядят как
A&B -> A
A&B -> B
а правило ввода аналогично pair.
В категории с числами и делимостью произведением АхВ будет наименьшее общее кратное (lowest common multiple) lcm(A,B). Оно делится на А, оно делится на В (т.е. из него есть стрелки в А и В), и любое другое натуральное число, которое тоже делится на А и В, делится на lcm(A,B), т.е. из него есть стрелка в АхВ.
Если чуть углубиться в теорию, то произведение prod(A,B) - это функтор СхС -> С, являющийся правым сопряженным для диагонального функтора С -> СхС (и указание "right object" на самом деле говорит о том, что определяемый функтор - именно правый сопряженный), и значит для объектов А, В и С имеется натуральный изоморфизм между множествами стрелок:
Hom(C,A) х HomC(C,B) ~= Hom(C, prod(A,B))
другими словами для любой пары стрелок C -> A и С -> В есть соответствующая им стрелка С -> prod(A,B), это и есть pair. Если же в качестве С подставить сам prod(A,B), получим
Hom(prod(A,B),A) х HomC(prod(A,B),B) ~= Hom(prod(A,B), prod(A,B))
Здесь слева можно найти наши стрелки-проекции pi1 и pi2 и обнаружить, что
pair(pi1, pi2) = I
Т.е. свойства произведения, которые в иных языках спецификаций нужно выражать явно аксиомами, здесь вытекают сами из понятия сопряженных функторов, на которых все строится. Кстати, стрелки pi1 и pi2 тут становятся естественными преобразованиями. Но это если углубляться в теорию, а мы этого делать не будем. :)
Теперь, раз у нас все строится из стрелок, соединящих пары объектов, всегда есть два возможных направления для стрелки - туда и сюда. Что будет, если взять и стрелки все поразворачивать? Если так сделать в определении какого-то объекта, получим двойственный (dual) к нему объект. Например, возьмем и развернем все стрелки в определении произведения. Получим вот что:
Это копроизведение - А+В. На CPL оно тоже определяется путем разворота всех стрелок:
Стрелки проекций pi1 и pi2 превратились в стрелки инъекций in1 и in2, стрелка-факторизатор pair превратилась в стрелку case, идущую в обратном направлении, и теперь это left object, и он вроде как правда левый сопряженный функтор для диагонального.
В категории типов данных копроизведение - это sum type, А+В (в хаскеле - Either A B). Конструкторы Left и Right в Either как раз служат стрелками in1 и in2. Универсальность диктует, что если есть другой похожий объект С, в который тоже есть стрелки из А и В, то должна быть и уникальная стрелка А+В -> С. Действительно, если у нас есть функции
fa :: A -> C
fb :: B -> C
то можно построить функцию
В категории логических высказываний копроизведение - это связка ИЛИ. Правила ввода выглядят в точности как in1 и in2, а правило избавления - в точности как case.
В категории натуральных чисел с делимостью в качестве стрелок копроизведение А и В - это наибольший общий делитель gcd(A,B). На него делится А, на него делится В (стрелки in1, in2), и для любого другого числа С, на которое тоже делятся А и В (т.е. любой общий делитель А и В), gcd(A,B) делится на С, это стрелка-факторизатор case.
Еще один полезный универсальный объект - экспоненциал. Вот его фотокарточка:
Для двух объектов А и В их экспоненциал exp(A,B) характеризуется наличием морфизма eval из произведения exp(A,B) и A в B, а универсальность диктует, что для любого похожего объекта С, для которого тоже есть такой морфизм f из СхА в В, должен быть уникальный морфизм
curry(f): C -> exp(A,B)
На CPL это записывается очень просто:
В категории типов данных exp(A,B) - это функция из А в В. Тогда eval получает данную функцию и ее аргумент типа А, и вычисляет результат типа В (отсюда название). А curry, имея функцию типа
СхА -> В
и значение типа С, делает нам функцию из А в В, это простое каррирование.
В категории логических высказываний exp(A,B) - это импликация А=>B. Стрелки curry и eval полностью совпадают с логическими правилами ввода и избавления от импликации. Например, по правилу избавления из пары утверждений А=>B и А выводится В.
В категории чисел и делимости exp(A,B) = lcm(a,b) / a. Именно такое определение позволяет всем стрелкам на диаграмме сходиться как надо. (Update: тут я наврал, функция не такая, чуть сложнее.) Например, если А=30, В=35 и С=2310, то
exp(A,B) = lcm(30,35)/30 = 210/30 = 7
exp(A,B) x A = lcm(7,30) = 210
C x A = lcm(2310, 30) = 2310
210 делится на 35, 2310 делится на 35, 2310 делится на 210, 2310 делится на 7, все стрелки на месте.
Солнце клонится к закату, а мы еще не приблизились к вычислениям. Давайте определим натуральные числа. Это объект nat, характеризуемый наличием двух стрелок: zero из 1 в него, и succ из nat в nat (для краткости будет просто s), да такой, что всякий похожий объект с ним связан стрелкой-факторизатором pr (означающей "примитивную рекурсию"). И вот такая картинка должна коммутировать:
На CPL это опять очень просто:
Интепретатор CPL умеет без лишних слов понимать про устройство диаграмм, соответствующих описываемым объектам, и из них (и свойств сопряженных функторов) выводить связи между разными морфизмами. Определив объект, можно попросить интерпретатор показать, что он про сей объект понял. Вот, что он выдает про наши объекты (самое интересное см. в графе equations, точка означает композицию стрелок):
Выделенные уравнения про стрелку примитивной рекурсии pr показывают ее суть - имея две операции и натуральное число, она строит их композицию, где одна из операций применяется однажды (она соответствует нулю), а другая - столько раз, какое у нас есть число (т.е. для числа 2 она будет применена дважды). Имея в категории натуральные числа, а также стандартный набор CCC - cartesian closed category - терминальный объект, произведения и экспоненциалы, можно определить сложение чисел, а через него и умножение.
let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
let mult=eval.prod(pr(curry(zero.!), curry(add.pair(eval, pi2))), I);
Тогда можно построить h(x) = x*(x+1):
let h = mult . pair(s, I);
И трижды применить ее к единице (которая s.zero, а не 1 - терминальный объект), чтобы получить 42.
Принцип вычислений примерно такой. Мы берем за основу терминальный объект и смотрим, какие есть морфизмы из него, назовем их элементами. Например, zero: 1 -> nat. В категории типов это функции из () - т.е. те, что могуть дать какое-то значение "из ничего". В логике это высказывания, истинность которых нам известна изначально, они как бы выводятся из True (терминального объекта), а не из каких-то других высказываний. Это те высказывания, из которых мы начинаем свой логический вывод (посылки?). И дальше мы из этих элементов строим конструкции путем композиции стрелок (вроде succ: nat -> nat), использования факторайзеров объектов для получения новых стрелок, их применения и т.д. Такое движение от терминального объекта задает разделение стрелок на два класса. Один - "по ходу движения" - это натуральные преобразования левых объектов и факторизаторы правых, они напоминают конструкторы данных в ЯП. Другой вид получается как бы "против движения" - это факторизаторы левых объектов и натуральные преобразования правых объектов, они напоминают управляющие структуры:
Получается такое разделение на данные и вычисления. В обычных языках программирования это разделение зафиксировано в явном виде, а тут оно возникает само из симметрии теории категорий. Можно придумывать объекты, к ним автоматически создавать двойственные, и разные их компоненты будут сами задавать способы строить данные и определять подходящие к ним управляющие конструкции, такой вот дуализм данных и кода (но совсем не тот, что в лиспе). Вычисления в CPL идут по уравнениям, связывающим морфизмы объектов (выводимым автоматически из свойств объектов), путем замены неканоничных частей выражения на каноничные, пока оно не будет целиком состоять из каноничных, т.е. всякий "код" должен выполниться и должны остаться одни "данные".
right object 1 with ! end object; right object prod(a,b) with pair is pi1: prod -> a pi2: prod -> b end object; right object exp(a,b) with curry is eval: prod(exp,a) -> b end object; left object nat with pr is zero: 1 -> nat s: nat -> nat end object; let add=eval.prod(pr(curry(pi2), curry(s.eval)), I); let mult=eval.prod(pr(curry(zero.!), curry(add.pair(eval, pi2))), I); let h = mult . pair(s, I); simp h.h.h.s.zero;
которая выводит результат
s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.zero
т.е. ровно 42.
Что же тут происходит? В CPL мы начинаем с чистого листа - там изначально нет ни базовых типов, ни каких-либо операций. Зато есть возможность определять универсальные категорные объекты (вот где настоящий объектно-ориентированный язык! :)). В категории у нас есть объекты и есть морфизмы между ними (они же стрелки), подчиняющиеся паре простых правил (наличие и ассоциативность композиции, наличие и годность identity - тождественного морфизма). Я сразу возьму несколько примеров, чтобы на них все примерять. Первый пример категории: объекты - типы данных функционального языка (int, bool, string, etc.), а морфизмы - функции (string_of_int : int -> string, succ : int -> int, etc.). Пример другой категории: объекты - логические высказывания, а стрелки показывают выводимость одного высказывания из другого (have_a_son -> have_a_child, А & B & C -> A...). Третий пример: объекты - натуральные числа, а стрелка соединяет два числа, если первое делится на второе (6 -> 3, 5 -> 5...). Мы можем придумывать какие-то универсальные объекты - они характеризуются наличием определенных связей с другими объектами категории, причем из всех аналогично связанных объектов они "самые-самые": всякий похожий объект связан с нашим уникальным морфизмом. Простейший пример - терминальный объект категории. Это такой объект, в который есть по уникальной стрелке из всех объектов категории. С т.з. универсальности это объект без особенных связей, но всякий похожий объект (а раз никаких особенностей не требуется, то любой объект категории) связан с ним уникальным морфизмом. На CPL это записывается так:
right object 1 with ! end object;
Здесь 1 - название определяемого объекта, ! - название для морфизма, связывающего любой похожий объект (т.е. в данном случае вообще любой объект) с 1, а "right" показывает направление для ! - определяемый объект стоит справа от стрелки:
! : X -> 1
для всех объектов Х.
В категории типов терминальный объект - тип (), он же unit, он же void. Из любого типа Т можно сделать функцию Т -> (), она и станет морфизмом "!". В категории логических высказываний терминальный объект - особое высказывание True, Истина, оно выводится из любого истинного высказывания (то бишь из всех). В категории натуральных чисел, где стрелки означают делимость, терминальный объект - это 1. Всякое натуральное число делится на 1.
Чуть сложнее, но в том же ключе выглядит произведение:
right object prod(a,b) with pair is pi1: prod -> a pi2: prod -> b end object;
Объект АхВ (обозначенный тут как prod(a,b)) называется произведением объектов А и В, если из него есть стрелка в А, есть стрелка в В (обозначим их pi1 и pi2), и для любого похожего объекта С (т.е. из которого тоже есть стрелки в А и В) есть стрелка из С в наш объект АхВ. Ее назовем pair, а факт того, что определяемый объект в ней справа (pair: C -> AхB), отметим указанием "right". При этом должна работать ("коммутировать" - разные пути между двумя точками должны определять эквивалентные морфизмы) такая диаграмма:
(пунктиром обозначен морфизм, существование которого должно вытекать из существования стрелок, показанных сплошными линиями)
В категории типов данных произведение типов А и В - это тупл (А,В). Стрелки pi1 и pi2 - это функции fst и snd. Если из некоторого типа С тоже есть две стрелки (функции)
fa :: C -> A
fb :: C -> B
то можно сделать функцию
pair_fa_fb :: C -> (A,B)
pair_fa_fb c = (fa c, fb c)
В категории логических высказываний произведение - это связка И (&). Правила избавления от И выглядят как
A&B -> A
A&B -> B
а правило ввода аналогично pair.
В категории с числами и делимостью произведением АхВ будет наименьшее общее кратное (lowest common multiple) lcm(A,B). Оно делится на А, оно делится на В (т.е. из него есть стрелки в А и В), и любое другое натуральное число, которое тоже делится на А и В, делится на lcm(A,B), т.е. из него есть стрелка в АхВ.
Если чуть углубиться в теорию, то произведение prod(A,B) - это функтор СхС -> С, являющийся правым сопряженным для диагонального функтора С -> СхС (и указание "right object" на самом деле говорит о том, что определяемый функтор - именно правый сопряженный), и значит для объектов А, В и С имеется натуральный изоморфизм между множествами стрелок:
Hom(C,A) х HomC(C,B) ~= Hom(C, prod(A,B))
другими словами для любой пары стрелок C -> A и С -> В есть соответствующая им стрелка С -> prod(A,B), это и есть pair. Если же в качестве С подставить сам prod(A,B), получим
Hom(prod(A,B),A) х HomC(prod(A,B),B) ~= Hom(prod(A,B), prod(A,B))
Здесь слева можно найти наши стрелки-проекции pi1 и pi2 и обнаружить, что
pair(pi1, pi2) = I
Т.е. свойства произведения, которые в иных языках спецификаций нужно выражать явно аксиомами, здесь вытекают сами из понятия сопряженных функторов, на которых все строится. Кстати, стрелки pi1 и pi2 тут становятся естественными преобразованиями. Но это если углубляться в теорию, а мы этого делать не будем. :)
Теперь, раз у нас все строится из стрелок, соединящих пары объектов, всегда есть два возможных направления для стрелки - туда и сюда. Что будет, если взять и стрелки все поразворачивать? Если так сделать в определении какого-то объекта, получим двойственный (dual) к нему объект. Например, возьмем и развернем все стрелки в определении произведения. Получим вот что:
Это копроизведение - А+В. На CPL оно тоже определяется путем разворота всех стрелок:
left object coprod(a,b) with case is in1: a -> coprod in2: b -> coprod end object;
Стрелки проекций pi1 и pi2 превратились в стрелки инъекций in1 и in2, стрелка-факторизатор pair превратилась в стрелку case, идущую в обратном направлении, и теперь это left object, и он вроде как правда левый сопряженный функтор для диагонального.
В категории типов данных копроизведение - это sum type, А+В (в хаскеле - Either A B). Конструкторы Left и Right в Either как раз служат стрелками in1 и in2. Универсальность диктует, что если есть другой похожий объект С, в который тоже есть стрелки из А и В, то должна быть и уникальная стрелка А+В -> С. Действительно, если у нас есть функции
fa :: A -> C
fb :: B -> C
то можно построить функцию
g_fa_fb :: Either A B -> C g_fa_fb x = case x of Left a -> fa a Right b -> fb b
В категории логических высказываний копроизведение - это связка ИЛИ. Правила ввода выглядят в точности как in1 и in2, а правило избавления - в точности как case.
В категории натуральных чисел с делимостью в качестве стрелок копроизведение А и В - это наибольший общий делитель gcd(A,B). На него делится А, на него делится В (стрелки in1, in2), и для любого другого числа С, на которое тоже делятся А и В (т.е. любой общий делитель А и В), gcd(A,B) делится на С, это стрелка-факторизатор case.
Еще один полезный универсальный объект - экспоненциал. Вот его фотокарточка:
Для двух объектов А и В их экспоненциал exp(A,B) характеризуется наличием морфизма eval из произведения exp(A,B) и A в B, а универсальность диктует, что для любого похожего объекта С, для которого тоже есть такой морфизм f из СхА в В, должен быть уникальный морфизм
curry(f): C -> exp(A,B)
На CPL это записывается очень просто:
right object exp(a,b) with curry is eval: prod(exp,a) -> b end object;
В категории типов данных exp(A,B) - это функция из А в В. Тогда eval получает данную функцию и ее аргумент типа А, и вычисляет результат типа В (отсюда название). А curry, имея функцию типа
СхА -> В
и значение типа С, делает нам функцию из А в В, это простое каррирование.
В категории логических высказываний exp(A,B) - это импликация А=>B. Стрелки curry и eval полностью совпадают с логическими правилами ввода и избавления от импликации. Например, по правилу избавления из пары утверждений А=>B и А выводится В.
В категории чисел и делимости exp(A,B) = lcm(a,b) / a. Именно такое определение позволяет всем стрелкам на диаграмме сходиться как надо. (Update: тут я наврал, функция не такая, чуть сложнее.) Например, если А=30, В=35 и С=2310, то
exp(A,B) = lcm(30,35)/30 = 210/30 = 7
exp(A,B) x A = lcm(7,30) = 210
C x A = lcm(2310, 30) = 2310
210 делится на 35, 2310 делится на 35, 2310 делится на 210, 2310 делится на 7, все стрелки на месте.
Солнце клонится к закату, а мы еще не приблизились к вычислениям. Давайте определим натуральные числа. Это объект nat, характеризуемый наличием двух стрелок: zero из 1 в него, и succ из nat в nat (для краткости будет просто s), да такой, что всякий похожий объект с ним связан стрелкой-факторизатором pr (означающей "примитивную рекурсию"). И вот такая картинка должна коммутировать:
На CPL это опять очень просто:
left object nat with pr is zero: 1 -> nat s: nat -> nat end object;
Интепретатор CPL умеет без лишних слов понимать про устройство диаграмм, соответствующих описываемым объектам, и из них (и свойств сопряженных функторов) выводить связи между разными морфизмами. Определив объект, можно попросить интерпретатор показать, что он про сей объект понял. Вот, что он выдает про наши объекты (самое интересное см. в графе equations, точка означает композицию стрелок):
> show object prod
right object prod(+,+)
- natural transformations:
pi1: prod(*a,*b) -> *a
pi2: prod(*a,*b) -> *b
- factorizer:
f0: *a -> *b f1: *a -> *c
------------------------------
pair(f0,f1): *a -> prod(*b,*c)
- equations:
(REQ1): pi1.pair(f0,f1)=f0
(REQ2): pi2.pair(f0,f1)=f1
(RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
(RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
- unconditioned: yes
- productive: (yes,yes)
> show object coprod
left object coprod(+,+)
- natural transformations:
in1: *a -> coprod(*a,*b)
in2: *b -> coprod(*a,*b)
- factorizer:
f0: *b -> *a f1: *c -> *a
--------------------------------
case(f0,f1): coprod(*b,*c) -> *a
- equations:
(LEQ1): case(f0,f1).in1=f0
(LEQ2): case(f0,f1).in2=f1
(LFEQ): coprod(f0,f1)=case(in1.f0,in2.f1)
(LCEQ): g.in1=f0 & g.in2=f1 => g=case(f0,f1)
- unconditioned: yes
- productive: (no,no)
> show object exp
right object exp(-,+)
- natural transformations:
eval: prod(exp(*a,*b),*a) -> *b
- factorizer:
f0: prod(*a,*b) -> *c
---------------------------
curry(f0): *a -> exp(*b,*c)
- equations:
(REQ1): eval.prod(curry(f0),I)=f0
(RFEQ): exp(f0,f1)=curry(f1.eval.prod(I,f0))
(RCEQ): eval.prod(g,I)=f0 => g=curry(f0)
- unconditioned: yes
- productive: (no,no)
> show object nat
left object nat
- natural transformations:
zero: 1 -> nat
s: nat -> nat
- factorizer:
f0: 1 -> *a f1: *a -> *a
-------------------------
pr(f0,f1): nat -> *a
- equations:
(LEQ1): pr(f0,f1).zero=f0
(LEQ2): pr(f0,f1).s=f1.pr(f0,f1)
(LFEQ): nat=pr(zero,s)
(LCEQ): g.zero=f0 & g.s=f1.g => g=pr(f0,f1)
- unconditioned: no
- productive: ()
Выделенные уравнения про стрелку примитивной рекурсии pr показывают ее суть - имея две операции и натуральное число, она строит их композицию, где одна из операций применяется однажды (она соответствует нулю), а другая - столько раз, какое у нас есть число (т.е. для числа 2 она будет применена дважды). Имея в категории натуральные числа, а также стандартный набор CCC - cartesian closed category - терминальный объект, произведения и экспоненциалы, можно определить сложение чисел, а через него и умножение.
let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
let mult=eval.prod(pr(curry(zero.!), curry(add.pair(eval, pi2))), I);
Тогда можно построить h(x) = x*(x+1):
let h = mult . pair(s, I);
И трижды применить ее к единице (которая s.zero, а не 1 - терминальный объект), чтобы получить 42.
Принцип вычислений примерно такой. Мы берем за основу терминальный объект и смотрим, какие есть морфизмы из него, назовем их элементами. Например, zero: 1 -> nat. В категории типов это функции из () - т.е. те, что могуть дать какое-то значение "из ничего". В логике это высказывания, истинность которых нам известна изначально, они как бы выводятся из True (терминального объекта), а не из каких-то других высказываний. Это те высказывания, из которых мы начинаем свой логический вывод (посылки?). И дальше мы из этих элементов строим конструкции путем композиции стрелок (вроде succ: nat -> nat), использования факторайзеров объектов для получения новых стрелок, их применения и т.д. Такое движение от терминального объекта задает разделение стрелок на два класса. Один - "по ходу движения" - это натуральные преобразования левых объектов и факторизаторы правых, они напоминают конструкторы данных в ЯП. Другой вид получается как бы "против движения" - это факторизаторы левых объектов и натуральные преобразования правых объектов, они напоминают управляющие структуры:
Получается такое разделение на данные и вычисления. В обычных языках программирования это разделение зафиксировано в явном виде, а тут оно возникает само из симметрии теории категорий. Можно придумывать объекты, к ним автоматически создавать двойственные, и разные их компоненты будут сами задавать способы строить данные и определять подходящие к ним управляющие конструкции, такой вот дуализм данных и кода (но совсем не тот, что в лиспе). Вычисления в CPL идут по уравнениям, связывающим морфизмы объектов (выводимым автоматически из свойств объектов), путем замены неканоничных частей выражения на каноничные, пока оно не будет целиком состоять из каноничных, т.е. всякий "код" должен выполниться и должны остаться одни "данные".
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-03-07 06:12 pm (UTC)no subject
Date: 2012-03-07 07:17 pm (UTC)Редукцию морфизмов можно понимать синтаксически, просто правила ее диктуются теоркатом. Берем категорное определение натуральных чисел, там два морфизма: zero и succ. Причем zero очень хороший - он из терминального объекта идет. Из них мы можем композицией получить новые морфизмы: succ.zero, succ.succ.zero и т.д. Они тоже из терминального объекта исходят, получается, нас как раз такие интересуют, это наши "данные". Теперь определили произведение, там говорится, что ежели у нас есть объекты А и В и их произведение АхВ (из которого идут морфизмы pi1 и pi2 в А и В), то для любого объекта С, если из него есть тоже похожие морфизмы в А и В, назовем их f0 и f1, должен существовать морфизм из С в АхВ, назовем его pair(f0,f1). Описывается такое определение в CPL так, что тот знает, из существования чего должно вытекать существование чего, знает, какая диаграмма должна коммутировать. Из нее он выводит правила, например такое:
pi1.pair(f0,f1)=f0
Это всего лишь запись того, что на картинке про произведение композиция стрелок pair(f0,f1) и pi1 дает то же, что и стрелка f0. Смысл категорный, но уравнение получилось чисто синтаксическое, получилось правило для редукции.
Теперь возьмем построенные недавно морфизмы zero и succ.zero. Они исходят из одного и того же объекта (1 - терминального), а значит их можно поставить в формулу выше в качестве f0 и f1. Тогда если мы напишем выражение
pi1.pair(zero, succ.zero)
то интерпретатор может его редуцировать до просто zero. Профит!
no subject
Date: 2013-05-15 01:10 am (UTC)Стоило всего лишь вынести немного теоркатов себе в диплом.
no subject
Date: 2013-05-15 05:57 am (UTC)