gds (gds) wrote,
gds
gds

А теперь мы займёмся профанацией. Особо-приёбистым "дважды крутым мудакам" просьба не читать. nivanych не соберётся никак, поэтому приходится мне.
Речь пойдёт про индукцию и коиндукцию, кое-как в применении к функциональным языкам программирования. Но чуть-чуть.

[Ко]индукция -- общие принципы протаскивания утверждений по термам, заданным [ко]алгебрами.
Алгебра -- набор операций, из 0..n значений данного типа создающих одно значение этого типа. (Когда есть операция, берущая 0 значений, т.е. константный конструктор, эта алгебра хорошая, "начальная".)
Коалгебра -- способ из одного значения определённого типа определить, какой операцией оно было создано и из каких 0..n значений данного типа. (Когда есть вариант, содержащий 0 значений, эта коалгебра хорошая, "терминальная".)
Примеры:
1. Множество действительных чисел и различные элементарные математические функции -- алгебра. Не коалгебра хотя бы потому, что вы не сможете определить, является ли число двенадцать суммой именно семи и пяти (респект авторам лепросказок и tumarkin).
2. Списки в функциональных языках обладают свойствами как алгебры, так и коалгебры: можно и создать список из начального пустого списка и операции приклеивания бошки, и посмотреть, чем же список является (пустой он или же состоит из элемента, приклеенного к хвосту).
Ещё интересно, что при наличии рекурсивных значений не всякий список можно создать индуктивно (пример -- let rec x = 1 :: x), но всякий список можно разрушить коиндуктивно.
3. Поток событий от вашего любимого оконного менеджера, если его моделировать математически, является коалгеброй: из состояния мира (или из хендла окна) мы сможем получить следующее событие, но там неприменим вопрос в стиле "из каких будущих событий является сложенным текущее состояние окна" -- состояние просто есть, и мы его можем просто "разрушать" (какими-нибудь GetMessage в случае венды, например).

Ещё интересным является то, что коалгебру можно кодировать значениями с типом x -> T x, и это кодирование остаётся приемлемым независимо от ленивости языка программирования, так как имеется лямбда-абстракция в типе.

Зачастую тип T будет представляться индуктивным типом.
Однако, для бесконечных потоков, тип T может быть туплом из пользовательского типа A, значения которого будут возвращаться при разрушении, и из нового значения нашей коалгебры, то есть,
type infinite_stream 'a = ('a * infinite_stream 'a);


Например, если рассмотрим окамловские Stream как коалгебру, в качестве T возьмём следующий тип:

# type stream_coalgebra 'a = [ End_of_stream | Elem of 'a and Stream.t 'a ];
type stream_coalgebra 'a = [ End_of_stream | Elem of 'a and Stream.t 'a ]

# value (stream_destruct : Stream.t 'a -> stream_coalgebra 'a) strm =
    try (Elem (Stream.next strm) strm)
    with [Stream.Failure -> End_of_stream]
  ;
value stream_destruct : Stream.t 'a -> stream_coalgebra 'a = <fun>


(кодирование нечестное из-за мутабельности значений типа Stream.t, но это не мешает иллюстрации)

Пака.
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 32 comments