thedeemon: (psychosis)
И там уже n-категории да топосы.

Куда только власти смотрют!
thedeemon: (faculty of numbers)
Q: What is the best way to explain the basic ideas of category theory to my grandmother?

A: If your grandmother is an algebraic topologist, it should be easy: explain how taking the homology group of a topological space is an example of a functor from the category of groups to the category of topological spaces, and then describe how different ways of defining homology groups give different, but naturally isomorphic functors.

(John Baez on Quora)
thedeemon: (Digby)
Как развернуть список на окамле.

Код рабочий. Тащемта, модули успешно заменяют тайпклассы, хоть и громоздко получается.
thedeemon: (Digby)
Сегодня в нашем кружке "теоркат для самых маленьких" урок рисования. Будем рисовать монаду. (А то весной кое-кто писал "если монаду нельзя нарисовать, то её нет".)

Для начала нарисуем что-нибудь совсем простое. Палка, палка, огуречик - получился моноид. Моноид состоит из множества (вообще-то необязательно, может быть и штука побольше чем множество), бинарной ассоциативной операции на нем и выделенного элемента, называемого единицей. Бинарная операция берет любые два элемента из этого множества и выдает какой-нибудь один элемент оттуда же.

Она должна быть ассоциативной, т.е. (a*b)*c = a*(b*c):

Тут мы используем нечто вроде фейнмановских диаграмм, где время на рисунке идет снизу-вверх. В самом низу - что было, в самом верху - что получилось, в середине всякие превращения.Read more... )
thedeemon: (office)
Замечательная презентация про азы теорката для программистов. Содержание тут всем хорошо знакомо, но вот оформление очень порадовало, берите пример.
http://yogsototh.github.io/Category-Theory-Presentation/
thedeemon: (Default)
Допустим, захотелось нам на обед монад. Монада - это troika из (эндо-)функтора и пары естественных преобразований, такие что.. Постойте, а что такое функтор? Это отображение объектов и стрелок категории в объекты и стрелки другой (или той же самой) категории, но не любое, а для которого выполнены определенные законы - сохранение identity морфизмов и сохранение композиций:
Identity: fmap id ≡ id
Composition: fmap (f ∘ g) ≡ fmap f ∘ fmap g
И по сути у нас в функторе два отображения - одно для объектов, второе для стрелок. В привычном нам применении этого дела в программировании первое отображение становится конструктором типов: всякому типу T оно сопоставляет тип F(T), например из Int делает List[Int]. Второе отображение становится функцией fmap с типом вроде (A -> B) -> (F(A) -> F(B)). Функциональные языки позволяют определить эти отображения, но вот проверку выполнения необходимых законов приходится делать в уме - компилятор этим не занимается.

А вот в D, с его умением выполнять код при компиляции, это сделать можно попытаться, хотя бы некоторое приближение.
Read more... )
thedeemon: (Default)
Я в предыдущем посте всех обманул, а меня никто не поправил опять. Я сказал, что если на коммутирующей диаграмме между двумя объектами есть стрелки туда-сюда, то они получаются изоморфизмами. Однако ж нифига, и вот простой контрпример. Возьмем объект А и его произведение с самим собой АхА:

По определению произведения из АхА есть стрелки fst и snd в А, и для любого объекта (например, А), из которого тоже есть стрелки f и g в А (например, f=g=id), есть уникальная стрелка pair(f,g) из этого объекта (А) в АхА, такая, что fst . pair(f,g) = f и snd . pair(f,g) = g, т.е. fst . pair(id,id) = id.
В CPL pair(id,id) имеет тип *a -> prod(*a,*a), а fst имеет тип prod(*a,*b) -> *a, и их композиция fst . pair(id,id) равна id, это нам дает определение произведения. Но вот обратная композиция pair(id,id) . fst нифига не равна id. А значит, определение изоморфизма не вывполнено, и А не изоморфен АхА, что и следовало ожидать. Так что построение стрелок на CPL туда-сюда еще не доказывает изоморфность, нужно явно показать, что обе их композиции равны соответствующим id. Упомянутые в прошлом посте изоморфизмы, дающие арифметические законы, остаются в силе, просто обоснования там неполные, не хватает кое-каких доказательств.
thedeemon: (Default)
А мы продолжаем передачу "теоркат для самых маленьких", в которой я рассказываю сам себе постигнутые азы. Сегодня мы увидим, как из нескольких категорных определений внезапно следуют привычные законы арифметики и как частный случай - арифметика типов. Теория категорий - это такая абстракция над теориями: мы берем какие-то теории, видим в них некоторые сущности и связи между ними, абстрагируемся от содержания (внутренней структуры) этих сущностей, концентрируясь лишь на связях между ними, и так получаем категорию (сущности становятся непрозрачными объектами, связи - стрелками между ними). Довольно разные теории при таком абстрагировании могут нам дать очень похожие категории, и доказав нечто один раз на уровне категорий, мы автоматически получаем множество теорем - по теореме для каждой из вписывающихся в эту категорию теорий. Так чуть ниже парой строк на CPL мы докажем, что
lcm(a, gcd(b,c)) == gcd(lcm(a,b), lcm(a,c))   (a,b,c - натуральные числа)
(a, Either b c) == Either (a,b) (a,c)         (a,b,c - типы данных в Хаскеле)
A & (B | C) == (A & B) | (А & C)              (A,B,C - логические высказывания)

и еще примерно 9213 теорем похожего вида.
Read more... )
thedeemon: (Default)
Лемму Йонеды называют самой сложной тривиальной вещью в математике. Сегодня мы попробуем закодировать ее на Окамле и понять ее связь с продолжениями (continuations). Лемма эта из теории категорий, я буду объяснять на пальцах, не слишком строго. В категории у нас есть коллекция объектов (порой очень большая, настолько, что это даже не обязательно множество) и коллекция стрелок между ними, также называемых морфизмами. Знакомый нам пример категории - где объекты это типы данных, а стрелки - функции между ними. Функтором называется отображение одной категории в другую (или в ту же, тогда это эндофунктор), сохраняющее структуру - "рисунок" стрелок. Он всякому объекту из первой категории сопоставляет некоторый объект из второй, и стрелки переносит соответственно. Конструкторы типов, вроде списка или дерева, - примеры (эндо)функторов в знакомой нам категории. Функтор "список" ('a list) отображает типы вроде int и string в типы вроде int list и string list, а функции вроде int -> string превращает в функции вроде int list -> string list. Такие вещи очень просто записываются на хаскеле, но сегодня я хочу использовать окамл, все-таки он наследник categorical abstract machine language. На окамле функтор в общем виде можно так, например, описать:
module type Functor = sig 
  type 'a t 
  val fmap : ('a -> 'b) -> 'a t -> 'b t 
end 

Это сигнатура модуля, "интерфейс". Реализуя его для конкретных конструкторов типов, вроде списка или дерева, мы получим конкретные функторы.

Если мы в некоторой категории С возьмем произвольный объект А, то Read more... )
thedeemon: (Default)
Я в недавнем посте в одном месте наврал, а меня не поправили. Если мы возьмем категорию, в которой объекты - натуральные числа, а стрелка соединяет два числа, когда первое делится на второе (это обычное частично упорядоченное множество), и мы хотим определить экспоненциал:

(напоминаю, что стрелки тут означают делимость, "произведение" - наименьшее общее кратное двух чисел, и смысл в том, что для любого числа С, для которого СхА кратно В, С должно быть кратно exp(A,B))

Я тогда сказал, что exp(А,В) = lcm(А,В) / А. (lcm - наименьшее общее кратное)
Это неправильная функция, она работает во многих случаях, но не во всех.
Правильная функция выглядит так: нужно взять В, разложить на простые множители в соответствующих им степенях, и убрать те из них, которые встречаются в аналогичном разложении А со степенью большей или равной той, что в В.

Примеры:
А = 30 = 2*3*5
В = 35 = 5*7
простой множитель 5 в А в той же степени, что и В, его убираем, остается 7. exp(A,B)=7

A = 70 = 2*5*7
B = 100 = 2*2 * 5*5
тут в В степени общих с А простых множителей больше, чем в А, поэтому убирать нечего, exp(A,B)=100.
На этом примере как раз изначально предложенная формула неправильный ответ дает.

Вопрос: можно ли эту функцию выразить без явного разложения на множители? Например, через формулу с gcd, lcm и арифметическими операциями.
thedeemon: (Default)
А вот можно ли вычислить ответ на главный вопрос, пользуясь одной лишь теорией категорий? Оказывается, можно. Давным-давно в одной далекой галактике Tatsuya Hagino придумал язык CPL (Categorical Programming Language), а чуть менее давно другой японец Masahiro Sakai сделал годный его интерпретатор. Hagino свою реализацию делал на Лиспе, а Sakai догадался таки задействовать языки программирования - сперва Руби, затем Хаскель (ибо Руби медленный, на Хаскеле в сто раз быстрее заработало). И вот полный текст программы на 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.

Что же тут происходит? Read more... )

Profile

thedeemon: (Default)
Dmitry Popov

May 2017

S M T W T F S
 1234 56
789 10 11 1213
14151617181920
21222324252627
28293031   

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 23rd, 2017 02:52 pm
Powered by Dreamwidth Studios