idris coq

Type Theory Proof Theory

  • хроники хасида     тайские хроники


     

    все мы имеем представление о типах данных, скажем "сообщение" или там "список"

    можно параметризовать типы значениями, что даёт возможность сказать

    типы функций тогда могут принимать вид

    вместо более распространённого что ведёт к точным спецификациям

    это и есть ЗАВИСИМЫЕ ТИПЫ

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

    с названиями зависимых типов очень все запутано. попробуем разобраться

    давайте подумаем о ∃ (кванторе существования) с конструктивной точки зрения

    (∃x . P x) значит "я уверен, что у меня есть (пока что - неопределенное) значение х и, ВМЕСТЕ с ним, СПОСОБ доказательства того, что для х имеет место свойство Р"

    а естественным подтверждением существования х является ПАРА, состоящая из самого х и из терма, показывающего, что (Р х) выполнимо. поэтому Сигма-Типы еще называются "зависимыми произведениями". такая структура данных просто-таки требует, чтобы ТИП второго элемента зависел от ЗНАЧЕНИЯ первого

    с точки зрения классической логики (∃x . P x) означает, что (Р х) выполняется, но только вы точно не знаете, для какого именно значения х. таким образом вы понимаете это как: наличие очень большого логического "ИЛИ" (обьединения):

             P(x0) \/ P(x1) \/ P(x2) \/ P(x3) \/ ...  
    
    а поскольку логическая операция "ИЛИ" тесно связана с типами "тэгированного обьединения", то и Сигма-Типы иногда назвают "зависимыми суммами"

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

    в этом случае в формуле (∀x . L x) переменная x пробегает весь ряд натуральных чисел

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

    это сразу наводит на мысль о функциях, а именно - о семействе функций :

      f : nat -> foo
      f : nat -> bar
      f : nat -> baz
           ...
      f : nat -> qux
           ...
    
    т.е. таких, что тип результата (foo|bar|baz|...|qux|...) зависит от x (то есть может быть и bar, и baz, и т.д. и qux и т.д. и даже foo:)

    таким образом в конструктивной логике квантор всеобщности интерпретируется как генерализация функций. поэтому Pi-Типы еще называют "зависимыми функциональными типами"

    в классической логике предикатов универсальный квантификатор (∀x . L x) означает, что вы УВЕРЕНЫ в том, что (L x) выполняется для ВСЕХ натуральных чисел. но это все равно, что сказать, что универсальный квантификатор равнозначен следующей формуле бесконечного логического "И" (пересечения):

                L(0) /\ L(1) /\ L(2) /\ L(3) /\ ... 
    
    а поскольку операция "И" и типы "картезианского произведения" связаны, Pi-Типы часто называют "зависимым произведением"


    зависимый тип B : A → Type - это на самом деле семейство типов

    так вот, "произведение ∏" и "сумма ∑" - имеются в виду произведение и сумма всех типов данного семейства

    например, элемент типа ∏ (x : A) B(x) - это кортеж из |A| значений типов семейства B, по одному B(x) на каждое x:A

    эквивалентно выражается в виде проекций кортежа для каждого индекса x:A - функция π: (x:A) → B x

    элемент типа ∑ (x : A) B(x) - это элемент disjoint union значений типов семейства B. если вспомнить, как пишется disjoint union, ∏ вверх ногами, ∐, и как он определяется - как кортеж из значения и индекса, указывающего, из какого множества это значение взято, то это и есть сигма, ∑. disjoint union иногда так и записывают, через ∑, а не ∐

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