часть первая структуры

имхо, [для обучения программировать] достаточно всего двух пунктов: итерация ; ветвление
чтобы был иллюстративный материал, тоже два пункта: комбинаторика ; алгебраические структуры

остальное нахрен не нужно

Андрей Мельников к Максиму Сохацкому
December 1 2014, 19:27:12 UTC

 

алгоритмы

  • λ-исчисление
  • абстрактные типы данных
  • арифметика типов
  • функтор
  • аппликативный функтор
  • логика высказываний второго порядка

  • теорема Гёделя о неполноте

    теорема Гёделя сама по себе не нуждается в семантике - ей не нужно ни N, ни понятие "истинности" утверждений. она сугубо синтаксична.

    если есть некоторая теория T, достаточно сложная (могущая доказать некоторые свойства натуральных чисел) и рекурсивная (множество аксиом конечно или описывается алгоритмом), то эта теория неполна: неверно, что она может доказать или опровергнуть любое утверждение

    речь идёт только о ВОЗМОЖНОСТИ доказать/опровергнуть, т.е. о существовании каких-то формальных последовательностей символов (формальных доказательств из аксиом данной теории)

    из того, что теория T неполна, мы можем мгновенно заключить, что она не "описывает" N, т.к. для "описывания" N ей пришлось бы доказывать все истинные в N утверждения и опровергать все ложные; т.к. любое утверждение либо истинно в N, либо ложно, T должна была бы быть полной теорией

    Гёделево утверждение G для PA верно в N (неформальный аргумент), и мы это можем формально доказать, но не в самой PA (она это не может доказать, потому что внутри неё вообще нельзя определить "истинность в N"), а в куда более мощной ZFC. ZFC мощна, и потому мы можем определить нашу семантическую "вселенную" N в ней в качестве синтаксического объекта-множества N, и свести любое семантическое утверждение об истинности в N к синтаксическому утверждению о доказуемости соответствующего утверждения о множествах.

    Гёделево утверждение G для ZFC в каком-то неформальном смысле тоже "истинно", но формализовать эту "истинность" нам уже просто негде. разница между PA и ZFC вот в чём. и та и другая - формальные теории, некий набор аксиом, однако для первой N не является частью теории, а является какой-то канонической моделью, которую мы выбрали, и в которой мы проверяем истинность или ложность утверждений PA или любых других утверждений в том же языке арифметики, когда нам это удобно. для ZFC же N - это объект, описываемый теорией, это множество, как любое другое множество, о котором ZFC что-то может доказать. если мы посмотрим на какую-то модель ZFC (очень гипотетически, т.к. существование такой модели мы не можем доказать вследствие 2-й теоремы Гёделя о неполноте), то N в ней будет *элементом*, а не самой моделью. N для ZFC - это как отдельное натуральное число для PA


    λ-исчисление

    John Harrison

    забудем про операции ввода-вывода и допустим, что программа работает конечное время, производя какой-либо результат. рассмотрим выполнение в абстрактном виде:

     σ0 → σ1 → σ2 → · · · → σn 
    программа начинает работу с начального состояния σ0, содержащего входные значения для программы. программа заканчивает работу в конечном состоянии σn, содержащем результат(ы) работы программы. состояние изменяется конечное число раз из σ0 в σn; в принципе, каждая команда может изменить состояние.

    избегая использования переменных и операций присваивания, мы получаем следующие преимущества:

  • ясная семантика
  • параметризация и модульность программ
  • способы представления бесконечных данных
  • чтобы создать надлежащую семантику для императивных методов, нам необходимо явно определить состояние. например, мы можем создавать команды как:

  • частичные функции σ → σ
  • отношения σ × σ
  • предикатные преобразователи (σ → bool) → (σ → bool)
  • даже если позволить существование goto, то этого все-равно мало и нам еще нужна семантика, основанная на продолжениях

    все эти методы достаточно сложны, но в функциональных программах у нас есть возможность проверить их корректность, а также корректность некоторых преобразований и оптимизаций

    нотация

    λ-нотация – это способ определения функций, предложенный Алонзо Чёрчем. мы пишем:

     λx. E 
    чтобы определить «функцию от x, которая возвращает E». здесь E – это выражение, которое содержит или не содержит x. если оно содержит х, то х является связанной переменной, а если не содежит - то х называется свободной переменной

    используя только:

  • переменные, например, x, y
  • константы, например, 3, true, +
  • применение функции к аргументам, например, f x
  • λ-абстракцию выражения над переменными, например λx. x + y
  • мы составим основной «абстрактный синтаксис» математики

    возможности λ-нотации полезны для унификации понятия связанных переменных. в математике переменные обычно выражают зависимость некоторого выражения от значения этой переменной

    в логике применяются кванторы ∀x.P[x] и ∃x.P[x]; в теории множеств — абстрактные множества, наподобие {x | P[x]}, а также индексированные объединения и пересечения. в таких случаях говорят, что переменная должна быть связанной (bound)

    при использовании λ-нотации выражения λx.E[x] и λy.E[y] являются эквивалентными; это называется альфа-эквивалентностью, а процесс преобразования одного выражения в другое — альфа-преобразованием. следует особо оговорить, что переменная y не должна быть свободной в выражении E[x], иначе его значение изменится

    λ-абстракция выглядит как подходящий примитив, в терминах которого проводится анализ связывания переменных. эта идея уходит корнями к записи логики высшего порядка в λ-нотации, использованной Чёрчем. идея использования λ-нотации в качестве универсального абстрактного синтаксиса была введена Мартином-Лёфом

    λ-термы

    основой λ-исчисления служит формальное понятие λ-термов, которые строятся из переменных и некоторого фиксированного множества констант при помощи операций применения (аппликации) функций и λ-абстракции. это значит, что всевозможные λ-термы разбиваются на четыре класса:

    λ-термы строятся по индукции. это может быть выражено следующей грамматикой BNF:

     Exp = Var | Const | Exp Exp | λ Var. Exp 
    так как синтаксис задан по индукции, то мы можем определять сущности с помощью примитивной рекурсии и доказывать сущности с помощью структурной индукции

    обозначим множество свободных переменных в терме s через FV(s) и дадим его рекурсивное определение:

    FV (x) = {x}
    FV (c) = ∅
    FV (s t) = FV (s) ∪ FV (t)
    FV (λx. s) = FV (s) − {x}
    
    аналогично вводится и понятие множества связанных переменных BV(s):
    BV (x) = ∅
    BV (c) = ∅
    BV (s t) = BV (s) ∪ BV (t)
    BV (λx. s) = BV (s) ∪ {x}
    

    одним из правил является соглашение о том, что λ-абстракция и применение функции представляют собой взаимно обратные операции. то есть, если мы возьмём терм λx.s и применим его как функцию к терму-аргументу t, результатом будет терм s, в котором все свободные вхождения переменной x заменены термом t

    обозначим операцию подстановки терма s вместо переменной x в другой терм t как t[s/x]

    x[t/x] = t
    y[t/x] = y, если x != y
    
    c[t/x] = c
    
    (s1 s2)[t/x] = s1[t/x] s2[t/x]
    
    (λx.s)[t/x] = λx. s
    (λy.s)[t/x] = λy.(s[t/x]), x != y и либо x !∈ FV(s), либо y !∈ FV(t)
                  в противном случае λz.(s[z/y][t/x]), z !∈ FV(s) ∪ FV(t)
    

    ещё одной из основ λ-исчисления служат три «преобразования» — операции получения по заданному терму другого, равного ему в интуитивном смысле. традиционно их обозначают буквами греческого алфавита: α (альфа), β (бета) и η (эта)

    пример β-редукции:

     
        fst (M , N) ==> M
        snd (M , N) ==> N
        
        (λx.M) N ==> M[N/x]
     

    пример μ-редукции:

        M : A ✗ B ==> (fst M , snd M)
    
        M : A -> B  ==> (λx. M x) : B 
     

    η-преобразование воплощает принцип экстенсиональности. два свойства называются экстенсионально эквивалентными, если этими свойствами обладают в точности одни и те же объекты. в теории множеств принята аксиома экстенсиональности, согласно которой два множества совпадают, если они состоят из одних и тех же элементов. аналогично, будем говорить, что две функции эквивалентны, если области их определения совпадают, а значения функций для всевозможных аргументов также одинаковы

    введение η-преобразования делает наше понятие λ-эквивалентности экстенсиональным. в самом деле, пусть f x и g x равны для произвольного значения x; в частности, f y = g y, где переменная y выбирается так, чтобы она не была свободной как в f, так и в g

    согласно последнему из приведённых выше правил эквивалентности, λy.f y = λy.g y

    применив дважды η-преобразование, получаем, что f = g

    из экстенсиональности следует, что всевозможные η-преобразования не нарушают эквивалентности, поскольку согласно правилу β-редукции (λx.t x) y = t y для произвольного y, если переменная x не является свободной в терме t

      s →α t или s →β t или s →η t
      ----------------------------
                 s = t
    
      -----
      t = t
    
      s = t
      -----
      t = s
      
      s = t и t = u
      -------------
         s = u
    
        s = t
      --------
      s u = t u
    
        s = t
      ---------
      u s = u t
    
          s = t
      -------------
      λx. s = λx. t
    

    программа на функциональном языке представляет собой выражение, а её выполнение — вычисление этого выражения. то есть, в терминах, изложенных выше, мы собираемся начать процесс вычислений с соответствующего терма и применять к нему правила редукции до тех пор, пока это возможно. нормальные формы, если они существуют, являются единственными с точностью до α-преобразования. это даёт нам первое обоснование того, что отношение λ-эквивалентности нетривиально, т. е. что существуют неэквивалентные термы. например, поскольку λx y.x и λx y.y несводимы друг к другу исключительно при помощи α-преобразований, они не эквивалентны

    комбинаторы

    будем называть комбинатором терм λ-исчисления без свободных переменных. такие термы также принято называть замкнутыми, поскольку их значение не зависит от значений каких-либо переменных. оказывается, что произвольный терм может быть выражен при помощи определённого множества комбинаторов и всевозможных переменных, операция λ-абстракции становится ненужной. в частности, замкнутый терм может быть представлен исключительно через эти комбинаторы. дадим их определения:

    I = λx. x
    K = λx y. x
    S = λf g x. (f x)(g x)
    

    чтобы легче их запомнить, можно воспользоваться простыми мнемоническими правилами

    комбинатор I представляет собой тождественную функцию («идентичность»)

    комбинатор K порождает семейство константных функций: после применения к аргументу 'a' он даёт функцию 'λy.a'

    S — комбинатор «совместного применения», который принимает в качестве аргументов две функции, применяемые к общему аргументу

    на самом деле достаточно использования S и K, ибо I = S K K

    рекурсия

    кажется, что сложно определить рекурсивную функцию не задав ей имени. однако, мы можем это сделать, используя комбинаторы неподвижной точки. говорят, что Y – комбинатор неподвижной точки, если, применив его к функции f , мы получим неподвижную точку x для f, то есть такое x, что f(x)=x. для всех f имеем:

     f (Y f) = Y f 

    Как альтернативу Y , можно задать выражение:

     T = (λx y. y (x x y)) (λx y. y (x x y)) 

    оно имеет более сильное свойство: T f → f (T f )

    типы

    так что же всё-таки «термы» означают в λ-исчислении? какой смысл в применении функции к самой себе, как в f f? некоторый смысл есть для таких функций, как тождество λx.x или константная функция λx.y, но, в основном, это выглядит подозрительно

    допустим, что у нас есть некий набор константных типов, например int и bool, и мы можем создавать из них новые типы, используя

    в общем случае у нас может быть сколь угодно много конструкторов типов и любое количество констант, типы которых содержат эти конструкторы

    мы думаем о типах, как о множествах, в которых объекты обозначаются термами, и t:σ читается как t∈σ - это система явных типов. однако предпочительнее использовать неявную типизацию, когда мы используем контекст Γ, который задаёт назначение типов для переменных и констант:

    Γ |- t : σ 

    в типизированном λ-исчислении у любого типизируемого терма есть нормальная форма, и все последовательности редукций завершаются на нормальной форме. это свойство называется сильной нормализацией. это замечательно — любая программа завершается. однако, это означает, что мы не можем написать все вычислимые, или даже все интересные, функции. мы не можем определять произвольные рекурсивные функции, иначе мы смогли бы определить функцию, которая никогда не завершается

    нормальный порядок редукции («вызов по имени») является наилучшей редукционной стратегией, потому что если хоть какая-то стратегия завершается, то эта тоже. однако, встаёт вопрос эффективности:

     (λx. x + x + x) (10 + 5) 

    нормальный порядок редукции даст

     (10 + 5) + (10 + 5) + (10 + 5) 

    и нам придётся три раза вычислять одно и тоже выражение! было бы эффективнее сначала вычислить аргумент 10 + 5. существует два решения проблемы, которые делят мир функционального программирования на части:

    ленивое вычисление выполняет нормальный порядок редукции, но имеет хитрые способы совместного использования выражений, сохраняя их в виде графа (не)вычисленных термов. при таком способе выражения вычисляются только один раз и только когда это понадобится

    энергичное вычисление просто вычисляет сперва аргументы («аппликативный порядок редукции»), и программист должен следить, чтобы не было зацикливаний

    в некотором роде ленивое вычисление элегантнее и мощнее. однако, его не так просто реализовать

    верификация

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


    абстрактные типы данных

    каноническая реализация картезианского произведения двух типов есть

     Pair a b = (a , b) 

    столь же каноническая реализация тегированной суммы двух типов есть

     Either a b = Left a | Right b 

    применяемые раздельно, произведение и сумма используются в разных структурах данных, но реальная их мощь проявляется при комбинировании:

          a * (b + c) = a * b + a * c
    
    LHS соответствует типу      
     (a , Either b c) 
    RHS соответствует типу      
     Either (a , b) (a , c) 

    эта адская смесь называется "полукольцом". это не "полное кольцо", поскольку отсутствует операция обращения (принципиально невозможная на типах)

    теперь - обобщим:

              0              Void
              1              ()
              
              a + b          Either a b     = Left a | Right b
              a * b          Pair a b       = (a , b)
    
              a * 1          (a , ())
              1 * a          (() , a)
              
              2 = 1 + 1      data Bool      = True | False
              
              1 + a          data Maybe     = Nothing | Just a
              1 + a          Either () a
              a + 1          Either a ()
              a + 1          data Maybe     = Just a | Nothing
    
              a + 0          Either a Void  = Left a | Y Void
              0 + a          Either Void a  = Y Void | Right a
    
              a * 0 = 0      (a , Void)     = Void      --  uninhabited
    
              
              1 + a * x      data List a    = Nil | a :: List a          
    

    и для булевой алгебры:

             false           Void
             true            ()
             a || b          Either a b     = Left a | Right b
             a && b          Pair a b       = (a , b)
    

    решение уравнений на символах - это алгебра и именно поэтому такие типы данных называются алгебраическими

    тип данных a -> b называют "экспоненциальным" и обозначают ba. такая нотация имеет смысл

    функция из типа Bool может принимать только один из двух аргументов: либо True либо False. все возможные функции Bool -> Int составляют множество пар (Int,Int) общее число которых |Int|^2

    а сколько значений может представить картеж из 256 переменных типа Bool? в точности 2^256, но это и есть число всевозможных функций Char -> Bool

    точно таким же образом можно подсчитать число всевозможных функций Bool -> Char как 256^2, и так далее

    таким образом экспоненциальная нотация имеет прямой смысл

    обобщим для экспонент:

    
                            a^0 = 1      Void -> a = ()
    
                            1^a = 1      a -> () = () 
    
                            a^1 = a      () -> a = a
    
                a^(b+c) = a^b | a^c      fun : Either b c -> a
                                         fun x = case x of
                                           Left b => ...  
                                           Right c => ... 
    
                  (a^b)^c = a^(b,c)      fun : b -> c -> a
                                         fun : b -> (c -> a)
                                         fun : (b , c) -> a
    
              (a,b)^c = (a^c , b^c)      fun : c -> (a , b)
                                         fun : c -> ((c -> a) , (c -> b))
    

    Haskell:
    data K a x = K a
    data I x = I x
    data Sum p q x = L (p x) | R (q x) 
    data Prod p q x = P (p x) (q x) 
    
    instance Functor (K a) where
      fmap f (K x) = K x
    
    instance Functor I where
      fmap f (I x) = I (f x)
    
    instance (Functor p, Functor q) => Functor (Sum p q) where
      fmap f (L p) = L (fmap f p)
      fmap f (R q) = R (fmap f q)
    
    instance (Functor p, Functor q) => Functor (Prod p q) where
      fmap f (P p q) = P (fmap f p) (fmap f q)

    import Data.Bifunctor
    
    data K a x y = K a
    data Fst x y = Fst x
    data Snd x y = Snd y
    data (Sum p q) x y = L (p x y) | R (q x y)
    data (Prod p q) x y = P (p x y) (q x y)
    
    instance Bifunctor (K a) where
      bimap f g (K x) = K x
      
    instance Bifunctor Fst where
      bimap f g (Fst x) = Fst (f x)
      
    instance Bifunctor Snd where
      bimap f g (Snd y) = Snd (g y)
      
    instance (Bifunctor p, Bifunctor q) => Bifunctor (Sum p q) where
      bimap f g (L p) = L (bimap f g p)
      bimap f g (R q) = R (bimap f g q)
      
    instance (Bifunctor p, Bifunctor q) => Bifunctor (Prod p q) where
      bimap f g (P p q) = P (bimap f g p) (bimap f g q)

    арифметика типов

    Дмитрий Попов

    возьмем логику высказываний и логическую связку ИЛИ (|) оттуда, дизъюнкцию. ее определением служат правила Intro и Elim

    правила Intro:
    если доказана достоверность высказывания А, то доказана и достоверность А|В
    если доказано В, то также доказано А|В

    правило Elim:
    если доказаны импликации А=>C и В=>С и доказано А|В, то доказана достоверность С

    сумма

    очень похоже выглядит сумма двух типов в ЯП (в Хаскеле это Either a b)


    если есть значение х типа а, то можно построить значение Left х типа Either a b
    аналогично из значения х типа b можно построить значение Right x того же типа Either a b

    что можно с такими значениями делать, кроме как где-то хранить и куда-то передавать? можно только одно - использовать в выражении case (и сводящемся к нему паттерн-матчинге)

    конструкция case берет по сути две функции:

  • одна что-то умеет делать со значением типа "а"
  • другая - со значением типа "b"
  • обе они возвращают результат одного типа "с", этот тип становится типом всего выражения case

    h :: Either Int String -> Float
    h x = case x of
      Left i -> fromIntegral i + 2.0
      Right s -> read s + 3.0
    

    сходство суммы типов и связки ИЛИ кристаллизуется в категорном определении суммы:

    объект sum(А,В) называется суммой объектов А и В, если

  • из А и из В в него есть стрелки, и
  • для любого другого объекта С, в который тоже есть стрелки из А и В, должна существовать уникальная стрелка из sum(A,B) в C да такая, чтобы получающаяся диаграмма коммутировала:
  • "диаграмма коммутирует" означает, что если на ней между двумя точками (объектами) есть несколько различных путей, то неважно каким путем двигаться из первой точки во вторую, результат будет одинаковый. применим ли мы сразу fromIntegral i + 2.0 к целому числу или сперва обернем в Left, а затем разберем через case и ту же функцию - результат один. воспользуемся ли сразу импликацией А => С для вывода С из доказанного А или сперва выведем достоверность А|В, а затем с помощью той же импликации и правила избавления от | выведем С, результат не изменится

    если у нас есть объект sum(A,B), то что можно сказать о sum(B,A)?

    это какой-то другой объект, но в него тоже есть стрелки из А и В, а значит должна быть стрелка из sum(A,B) в sum(B,A), этого требует определение. назовем ее f1. аналогично, должна быть и стрелка из sum(B,A) в sum(A,B), назовем ее f2. тогда их композиция f2 . f1 есть стрелка из sum(A,B) в sum(A,B)

    в категории у каждого объекта есть стрелка id в самого себя, а поскольку обсуждаемые стрелки тут таковы, что получаемые диаграммы с ними должны коммутировать, то не важно, попадем мы из sum(A,B) в себя по стрелке id или по стрелке f2.f1, а значит f2.f1=id

    обратная композиция, f1.f2 аналогично идет из sum(B,A) в sum(B,A) и по тем же соображениям f1.f2=id т.е. f1 и f2 - изоморфизмы, они делают объекты sum(A,B) и sum(A,B) изоморфными. для теории категорий такие объекты - близнецы-братья, т.к. все связи одного объекта автоматически есть и у другого, ибо определение категории требует наличие стрелки-композиции для каждой пары последовательных стрелок

    мы только что показали коммутативность сложения: sum(A,B) == sum(В,А), где == означает изоморфность

    в категории, где объекты - типы данных, а стрелки - функции, изоморфность означает не равенство типов, а эквивалентность в том, какую информацию значения этих типов содержат. изоморфность означает наличие стрелок-изоморфизмов, композиция которых равна id, а значит между такими типами должны существовать функции конверсии такие, что их композиция не теряет информации: сконвертив значение туда-обратно мы получим его же без изменений

    мы выше определили, что right и left - это стрелки типов b -> sum(a,b) и a -> sum(a,b)

    тип f1: sum(a,b) -> sum(b,a) соответственно, f1.f1 будет иметь тип sum(a,b) -> sum(a,b), а значит f1.f1=id (диаграмма должна коммутировать), и f1 - морфизм, доказывающий изоморфность этих двух объектов

    и при переводе на Хаскель это превращается в:

    f1 :: Either a b -> Either b a
    f1 x = case x of
      Left a -> Right a
      Right b -> Left b

    инициальный объект

    в некоторых категориях бывает определен инициальный объект. он характеризуется тем, что из него есть по уникальной стрелке во все объекты категории

    в логике высказываний таким объектом выступает особое высказывание ⊥ - "абсурд". его нельзя построить конструктивно (нет правила ввода), зато из него есть импликации во все возможные высказывания (из абсурда следует что угодно)

    в теории типов это пустой тип , у которого нет значений. у него нет особенных стрелок кроме универсального морфизма в каждый из объектов категории

    тождественный морфизм, имеющийся у каждого объекта: I : a -> a т.е. для любого объекта А есть стрелка из А в А. а по определению суммы, из А есть стрелка left в А+0. и поскольку эти стрелки таковы, что соответствующие диаграммы обязаны коммутировать, наличие стрелок из А в А+0 и обратно опять нам дает изоморфизм, поэтому А+0 == А (я для простоты буду писать А+В вместо sum(A,B)). значит, инициальный объект 0 - нейтральный элемент для сложения

    в логике это превращается в знакомое правило P | False == P

    в типах Either a ⊥ == a (ведь значения типа слева всегда будут вида Left х, ибо в Right нам подставить нечего)

    продукт

    сумму объектов в теоркате часто называют ко-продуктом, потому что это dual к произведению: одно получается из другого разворотом всех стрелок

    соответственно, произведением объектов А и В называется такой объект prod(A,B), из которого есть стрелки в А и в В (назовем их fst и snd), и для любого похожего объекта С (из которого тоже есть стрелки в А и В) есть уникальная стрелка pair из С в prod(A,B):

    опять, диаграмма должна коммутировать, т.е. fst.pair(f,g) = f и т.д.

    ровно те же рассуждения что и с суммой позволяют показать коммутативность произведения

    тип prod(a,b) -> prod(b,a) служит изоморфизмом между А*В и В*А, доказывающим их изоморфность

    в логике произведением служит связка И, в категории типов - тупл

    терминальный обьект

    двойственным объектом к инициальному (0) является терминальный (1), характеризующийся наличием уникальных стрелок из всех объектов категории в него

    в логике высказываний это особое высказывание "верно"

    в ЯП это тип unit (он же ()), с единственным значением (). его построить можно из чего угодно, функция f x = () служит стрелкой из любого типа в () ее тип: a -> ()

    как несложно догадаться, терминальный объект для произведения подобен инициальному для копроизведения - это нейтральный элемент, т.е. А*1 == А

    выражение "pair(I, ())" имеет тип a -> prod(a,1), а fst дает обратную стрелку из prod(a,1) в a. композиции их дают стрелки из a в a и из prod(a,()) в prod(a,()), т.е. это изоморфизмы, и действительно А*1 == А

    в категории с числами и делимостью 1 - это само число 1, на него делятся все натуральные числа. получаем знакомые соотношения

    (a, ()) == a

    P & True == Р

    lcm(a, 1) = a

    exponential

    дальше нам понадобится экспоненциал

    в логике это импликация (A => B) , в ЯП это функциональный тип (a -> b)

    в категории с экспоненциалами можно доказать дистрибутивность умножения относительно сложения.

    стрелка d1 типа sum (prod(a,b) , prod(a,c)) -> prod (a , sum(b,c)), т.е. из A*B + A*C в A * (B+C)

    d1 :: Either (a,b) (a,c) -> (a, Either b c) d1 x = (a,b) where a = case x of Left p -> fst p ; Right p -> fst p b = case x of Left p -> (Left . snd) p ; Right p -> (Right . snd) p

    а вот так можно определить обратную:

    d2 :: (a, Either b c) -> Either (a,b) (a,c) d2 x = ((cs . snd) x) (fst x) where cs s = case s of Left b -> \a -> Left (a,b) Right c -> \a -> Right (a,c)

    стрелка d2 типа prod (a , sum(b,c)) -> sum (prod(a,b) , prod(a,c)), т.е. это стрелка из A * (B+C) в A*B + A*C

    вместе d1 и d2 служат изоморфизмами, доказывая A*(B+C) == A*B+A*C, дистрибутивность

    конечно, d2 можно записать проще:

    d2' :: (a, Either b c) -> Either (a,b) (a,c)
    d2' (a, e) = case e of
                   Left b -> Left (a, b)
                   Right c -> Right (a, c)
    

    но загвоздка в том, что в категорном определении case он параметризуется стрелками (функциями): одна стрелка здесь должна уметь из значения "b" сделать Left(a,b), а вторая из "с" сделать Right(a,c), но где им для этого взять "а"? по сути, эти функции в d2' - замыкания, они берут значение "а" из окружения. приходится их реализовать более явно: не имея значения "а", мы возвращаем не Left(a,b), а функцию, которая из "a" сделает Left(a,b). аналогично с Right(a,c)

    тип у этих двух возвращаемых функций одинаковый, и он становится типом всего выражения case. и возвращенная им функция уже применяется к параметру типа "а", взятому из исходной пары. именно поэтому нам потребовались экспоненциалы

    раз уж у нас появился экспоненциал, докажем кое-какие его свойства

    напомню, что exp(A,B) означает для ЯП тип функции А -> В, для логики импликацию А => В , но экспоненциалом называется в силу схожести с В^A - "В в степени А". от возведения в степень разумно ожидать, что А^1=A и 1^A=1 для любого А, т.е. exp(1,A) == А и exp(A,1) == 1

    e1 имеет тип exp(1,a) -> a, т.е. дает нам стрелку из А^1 в A

    e2 имеет тип a -> exp(b, prod(a,b)), для любых объектов А и В е2 дает стрелку из А в exp(B, A*B), в частности для В=1 это стрелка из А в (A*1)^1, а про А*1 мы уже знаем, что он изоморфен А. это вроде как доказывает(?) A^1==A.

    выражение е3 имеет тип a -> exp(b,1) и для произвольных объектов A и B дает стрелку из A в 1^B, в частности из 1 в 1^B. ну а стрелка из 1^B в 1 всегда есть по определению 1 как терминального объекта. и опять в силу характера этих стрелок, наличие двух стрелок туда-обратно между объектами делает стрелки изоморфизмами, а объекты изоморфными. значит, 1^A == 1 для любого А

    как следствие a -> () == () для типов и (P => True) == P для логических высказываний

    итого, из категорных определений произведения, копроизведения, экспоненциала, инициального и терминального объектов мы вывели как следствия такие арифметические свойства:

    a+b == b+a
    a*b == b*a
    a+0 == 0+a == a
    a*1 == 1*a == a
    a*(b+c) == a*b + a*c
    a^1 == a
    1^a == 1

    и из этого набора можно получить другие следствия. например, обозначив 1+1 за 2, получим

    a*2 == a*1 + a*1 == a + a

    т.е. умножение (на натуральное число) выражается через сложение не только в привычной арифметике натуральных чисел, но и в арифметике типов

    кроме того можно показать, что a^2 == a*a, т.е. возведение в натуральную степень выражается через произведение. необходимые изоморфизмы на хаскеле выглядят так:

    type Two = Either () () p1 :: (a,a) -> (Two -> a) p1 (a,b) = \i -> case i of { Left _ -> a; Right _ -> b } p2 :: (Two -> a) -> (a,a) p2 f = (f (Left ()), f (Right ()))

    вот такая вот арифметика

    поправка про изоморфизмы

    я всех обманул. я сказал, что если на коммутирующей диаграмме между двумя объектами есть стрелки туда-сюда, то они получаются изоморфизмами. однако ж нифига, и вот простой контрпример.

    возьмем объект А и его произведение с самим собой АхА:

    по определению произведения из АхА есть

  • стрелки fst и snd в А, и
  • для любого объекта (например, А), из которого тоже есть стрелки f и g в А (для A это будут f = g = id)
    есть уникальная стрелка pair (f , g) из этого объекта (например А) в АхА, такая, что
    fst . pair (f , g) = f
    snd . pair (f , g) = g
    т.е. fst . pair (id , id) = id
  • pair(id,id) имеет тип a -> prod(a,a), а fst имеет тип prod(a,b) -> a, и их композиция fst . pair(id,id) равна id, это нам дает определение произведения

    но вот обратная композиция pair(id,id) . fst нифига не равна id, а значит, определение изоморфизма не выполнено, и А не изоморфен АхА, что и следовало ожидать. построение стрелок туда-сюда еще не доказывает изоморфность, нужно явно показать, что обе их композиции равны соответствующим id

    упомянутые в прошлом изоморфизмы остаются в силе, просто обоснования там неполные, не хватает кое-каких доказательств

    нужно иметь в уме, или перед глазами, определение изоморфности двух объектов в категории: для доказательства изоморфности нужно не только построить стрелки из одного объекта в другой и обратно, но и показать, что композиции стрелок, претендующих на роль изоморфизмов, действительно равны id

    функтор

    Idris:

        interface Functor (f : Type -> Type) where
          map : (m : a -> b) -> f a -> f b
    

    функтор - это особенный тип функций. это функция на алгебрах. говоря точнее, это функция, которая отображает одну алгебру на другую алгебру

    то есть, однажды построив алгебру на типе А, с помощью функтора вы можете перенести ее на тип В

    OCaml:

        (*  funct.ml  *)
    
     module type Functor =
      sig
        type 'a t
        val map : ('a -> 'b) -> 'a t -> 'b t
      end
    
    module OptionF : Functor with type 'a t = 'a option = 
      struct
        type 'a t = 'a option
        let map f = function | Some a -> Some (f a) | _ -> None
      end
    
    module IntToOpt (A: Functor) =
      struct
        let dblInt x = x * 2
        let dblOpt x = A.map dblInt x
      end
    
    module D = IntToOpt (OptionF) ;;
    
    let t1 = D.dblOpt (Some 5) ;;
    let t2 = D.dblOpt None ;;
    

    $> ocaml
    
                  OCaml version 4.03.0
    
    # #use "funct.ml";;
                  
    module type Functor = sig type 'a t val map : ('a -> 'b) -> 'a t -> 'b t end
    module OptionF :
      sig type 'a t = 'a option val map : ('a -> 'b) -> 'a t -> 'b t end
    
    module IntToOpt :
      functor (A : Functor) ->
        sig
          val dblInt : int -> int
          val dblOpt : int A.t -> int A.t
        end
    module D :
        sig
          val dblint : int -> int
          val dblOpt : int OptionF.t -> int OptionF.t
        end
                  
    val t1 : int OptionF.t = Some 10
    val t2 : int OptionF.t = None
    

    чтобы ваше отображение было функтором, необходимо соблюсти два условия:

  • map id x = id x
  • map g (map f x) = map (g ° f) x
  • второе условие иногда применяют непосредственно в коде и называют в этом случае fusion

    резюмируя: функтором называется отображение одной категории в другую, сохраняющее структуру - "рисунок" стрелок. он всякому объекту из первой категории сопоставляет некоторый объект из второй, и стрелки переносит соответственно

    конструкторы типов, вроде списка или дерева, - примеры функторов

    функтор "список" ('a list) отображает типы вроде int и string в типы вроде int list и string list,

    а функции вроде int -> string превращает в функции вроде int list -> string list

    естественное преобразование

    если у нас есть категории A и B, и два функтора F и G, каждый из которых отображает категорию A в категорию B, то можно представить отображение одного функтора в другой. оно каждому объекту x из A сопоставит стрелку в B, идущую из F(x) в G(x), т.е. опишет как превратить образ, получающийся первым функтором, в образ, получающийся вторым. такое отображение функторов (с выполненными требованиями сохранения структуры) называется естественным преобразованием

    все полиморфные функции, вроде head и tail для списков, fst и snd для туплов, - это естественные преобразования. они работают с формой структуры данных, не трогая ее наполнение, не зная конкретного её типа, т.е. превращают один функтор в другой

    аппликативный функтор как вычислительный базис

    Дмитрий Попов

    вот такая программа на Хаскеле вычисляет и выводит ответ на жизнь, вселенную и вообще:

    import Control.Applicative main = print $ answer succ 0 where one = pure <*> (pure :: a -> b -> a) inc = (<*>) ((<*>) <$> pure) mul = (<*>) <$> pure h = mul <*> inc answer = h . h . h $ one

    аппликативный функтор характеризуется наличием двух функций:

    class Functor f => Applicative f where  
      pure  :: a -> f a
      (<*>) :: f (a -> b) -> f a -> f b
    

    фишка в том, что для ((->) a) эти две функции - комбинаторы K и S

    instance Applicative ((->) a) where
      pure = const
      (<*>) f (g x) = f x (g x)
    

    мы знаем, что через S и K можно выразить любую лямбда-функцию. возьмем, например, функцию

    h x = x * (x + 1) 

    задействуем числа Черча: число представляется функцией, которая берет другую функцию и ее аргумент, и применяет ту функцию n раз. так, единица применяет другую функцию f один раз:

    one f x = f x 

    чтобы увеличить число n на 1, нужно применить f на один раз больше, чем это делает n:

    inc n f x = f (n f x) 

    умножение a на b делается применением b a раз:

    mul a b f x = a (b f) x 

    x тут можно "сократить" и не писать. тогда h будет выглядеть как

    h x = mul x (inc x) 

    теперь возьмем комбинаторный базис:

    s x y z = (x z) (y z)
      
    k x y = x
    

    пользуясь простым алгоритмом конверсии, наши арифметические функции можно выразить через S и K:

    one = s k k
    
    inc = s (s (k s) k)  
    
    mul = s (k s) k
    
    h = s mul inc
    

    теперь осталось лишь вспомнить, что

    k = pure
      
    s = <*>
      
    pure x <*> y = x <$> y 
    

    подставив их вместо S и K, получим программу

    представляете, какие открываются горизонты? я тоже нет. разве что обфускатор можно написать. :)

    comments

    не, две функции - это уже скучно.
    одноточечный универсальный базис слабо =) ?
    легко, но не так весело. просто тут приколько совпал базис с известным стандартным интерфейсом
    это нифига не случайное совпадение, а собствено базовая мотивация интерфейса аппликативных функторов
    оно ж не для каждого ап.функтора справедливо. одно дело засунуть в функтор и применить какую-то свою функцию, другое - как здесь - реализовать функцию на самом интерфейсе ап.функтора
    > оно ж не для каждого ап.функтора справедливо
    аппликативный функтор - это функтор, "переносящий" лямбда-исчисление из одной категории в другую, - так его определили
    метод "переноса" заключается в том, что мы можем переписать лямбда-выражения через S и K комбинаторы и заменить их на <*> и pure
    в исходной работе по аппликатианым функторам (“Applicative programming with effects”, Conor McBride, Ross Paterson) для <*> и pure используются обозначения \mathbb{S} и \mathbb{K}, и написано прямым текстом: «This class generalises S and K from threading an environment to threading an effect in general»
    у аппликативных функторов возможен и _другой_ интерфейс, связь которого с комбинаторной логикой менее очевидна;
    в той же работе объясняется, что аппликативный функтор - это strong lax monoidal functor, т.е. вместо S и K его можно снабжать тензорным произведением и тензорной силой, эффект будет тот же
    можно кстати сделать интерфейс через одноточечный базис комбинаторной логики навроде X; но неудобно
    в таком богатом языке-хосте это хм... почти столь же удобно и нужно, как вычисления на шаблонах в С++. :)
    ну так скучно в деревне :)
    вместо обфускатора можно написать транслятор в унлямбду или с унлямбды. там как раз SKI используется.
    да, транслятор в унлямбду - очень нужная в хозяйстве вещь! :)
    также, inc = S mul а посему, h = inc inc как же так?!
    >inc = S mul
    с чего бы?
    удивительно, но факт! ты подставь
    inc = S (S (K S) K)
    mul = S (K S) K
    
    я тоже как-то не мог понять, и в виде mul a b f x = a (b f) x этого не видно.
    зато раз x можно "сократить", то выходит mul a b x = a (b x)
    (даже больше: mul = (.)), а inc n f x = f ((n f) x) = mul f (n f) x
    полиморфизм!
    а вообще да, действительно
    Prelude> let h = inc inc
    Prelude> (h . h . h $ one) (+1) 0
    42
    
    хотя типы ghci выводит разные для inc и s mul
    думаю, ещё сильно зависит от того, как mul задать
    если задать слишком строго (т.е. не сокращать x в типе), то хотя всё равно реализация mul = (.), но это будет специализация (.) для функций вида (a->b)->(c->d) и не получится использовать mul в inc, т.к. в inc используется версия mul без x [ версия (.) для функций вида a->b ]

    категории

    категория морфизмов, в которой id-морфизм является единичным элементом, а композиция морфизмов - бинарной операцией, является моноидом

    категория, где все морфизмы обратимы, называется группоидом


    логика высказываний второго порядка

    HOL = функциональное программирование + конструктивная логика

    логика второго порядка — формальная система, расширяющая логику первого порядка возможностью квантификации общности и существования не только над аргументами, но и над самими предикатами

    для перехода к высшему порядку сами предикаты рассматриваются как "изменяемые объекты", а не условия, которые просто кем-то как-то когда-то откуда-то свыше "даны". такой "предикат" может менять свои показания даже при одном и том же значении "аргумента" - ну, например, обладать "памятью" обращений к нему (при этом должно строго выполняться одно условие: всякая информация о былом состоянии должна быть недоступна никому, кроме самого предиката)

    в логике высокого порядка как объекты трактуются сами отношения и функции, рассматриваемые в логике предикатов. это позволяет формировать утверждения обо всех отношениях, например, если потребуется точно определить, что означает понятие транзитивного отношения. логика высокого порядка является строго более выразительной, чем логика предикатов, в том смысле, что некоторые весьма полезные высказывания логики высокого порядка не могут быть выражены с помощью любого конечного количества высказываний логики предикатов

    в логике второго порядка квантификация допустима как в отношении переменных, так и в отношении предикатов или функций от переменных

    предположим, что мы хотим выразить некий факт о структуре арифметики Пеано, выраженной сигнатурой:

       { N ; 0, S, <, +, × }
    
    используя кванторы ∀ и ∃

    мы можем сформулировать предложение

      ∀x (x < S x)

    которое отражает тот факт, что каждое последующее число больше предыдущего. но трудность возникает, когда мы захотим выразить отношение строгого порядка на множестве натуралных чисел: а именно, что любое непуcтое множество натуральных чисел имеет минимальный элемент

    если P является одноместным предикатом, тогда мы можем записать наличие элемента, для которого предикат "быть минимальным" выполняется:

       ∃x Px → ∀y (Py → y = x)
    
    эта формула верна в языке первого порядка, но у нас нет возможности записать такую же формулу с первым квантором общности

    но если мы добавим квантор общности к предикату P:

       ∀P [ ∃x Px → ∀y (Py → y = x) ] 
    
    то сразу же получим желаемое свойство, но в логике высшего порядка

    используя логику второго порядка мы можем сказать, что рассматриваемый универсум бесконечен, просто выразив обязательное наличие транзитивного отношения для любого элемента к другому, но не к самому себе:

       ∃R [ ∀x ∀y ∀z (xRy ^ yRz → xRz)  ^  ∀x (¬ xRx ^ ∃y xRy) ]
    
    здесь квантор второго поряка ∃R выражает существование бинарного отношения в универсуме

    в логике второго порядка мы можем выразить индукцию натуральных чисел как:

       ∀P [ (P0 ^ ∀y(Py → PSy)) → ∀y Py ]
    

    для множества действительных чисел мы можем выразить отношение B "быть least-upper-bound" с помощью высказывания:

       ∀B [ ∃y ∀z(Bz → z ≤ y)  ^  ∃z Bz → ∃y∀y′(∀z(Bz → z ≤ y′) ↔ y ≤ y′) ]
    

    хорошо известен пример из области лингвистики, предложенный Джорджем Булем:

       “есть критики, которые ценят только друг друга”
    
    это предложение предполагает существование людей с особым свойством, но оно не влечет суждения, что два таких человека ценят только друг друга и больше никого

    в классической трактовке теории множеств не делается различия между абстрактными объектами и объектами, существование которых можно подтвердить построением - на бесконечные множества экстраполировали свойства и законы конечных совокупностей

       "all xs are ys"     -    "X  = Y"
       "some xs are ys"    -    "XY = V" ,  V - nonempty class
       "no xs are ys"      -    "XY = 0" ,  0 - empty class
    

    аксиома выбора - "для любого семейства попарно непересекающихся непустых множеств существует по меньшей мере одно множество, содержащее по одному (и только одному) элементу из каждого из множеств семейства"

    но что значит "выбрать из множества"? выбрать какой-то элемент — значит ли это определить этот элемент так, чтобы не было сомнения, что все имеют в виду один и тот же элемент?

    Гёдель доказал, что аксиома выбора не противоречит аксиомам теории множеств, если эти последние сами непротиворечивы, а Коэн - что отрицание аксиомы выбора не противоречит другим заранее непротиворечивым аксиомам теории множеств


    Андрей Бовыкин, питерские лекции