akuklev: (ДР Цертуса 2011)
В интуиционистских теориях зависимых типов постулируется существование Π-, Σ-, W-, а также той или иной иерархии вселенных Ui. Так вот все из них, кроме вселенных, комплектуются как правилами формирования, так и правилами расформирования. Правила формирования это например конструкторы Pair(a, b) для пары, конструкторы Zero и Succ(pred) для натуральных чисел, ламбда-выражения для Π-типов. А правила расформирования (разкарривание для пары, индукция для натуральных чисел) кроме их практического применения несут посыл, что пара не содержит ничего кроме двух элементов, которые в неё засунули, всякое натуральное число это либо Zero, либо применённый к нему конечное число раз Succ, иными словами размер алгебр Nat, Pair и т.д. фиксируется сверху, правила расформирования запрещают чтобы там были элементы отличимые* от канонических.

Вселенные же не снабжены правилом расформирования, и это как раз потому, что автору никак не хочется ограничивать их, хочется работать в Open World Assumption, т.е. "мы предполагаем, что могут быть такие типы, которые мы не умеем описывать, и это не потому что у нас мало описательных средств, а просто потому что мир разнообразен". Вместо ограничения размера, для вселенных действует противоположный принцип: для типа T общего вида нельзя производить интроспекцию, типа "если этот тип равен Bool, делаем одно, если это Π-тип, делаем другое", т.к. во-первых могут быть типы неизвестных нам сортов, во вторых эквивалентность типов (т.е. вопрос, равен ли данный тип неизвестного сорта Bool'у) неразрешим. Этот принцип приводит к тому, что, например, единственная функция типа ∀T, T -> T, это ничего не делающая функция id. Для всевозможных типов отображений с универсальной квантификацией по типам получаются такого вида theorems for free, а общий принцип называется параметричностью.

Так вот давно существует идея что касательно вселенных в интуиционистских теориях типов следует ввести вместо правила расформирования правило универсальности, ту самую параметричность внутри теории сформулировать. Гипотеза, которая сейчас кружит в разных головах вокруг HoTT (= стандартная интуиционистская теория зависимых типов + аксиома унивалетности) состоит в том, что это правило универсальности это и есть вычислительная форма аксиомы унивалетности. Идея витает уже два года, но на конференции TYPES'15, которая будет через две недели, три или четыре доклада именно на эту тему.


(* Речь идёт об отличимости при помощи сколь угодно большого, но конечного числа наблюдений/измерений сколь угодно высокой, но конечной точности. Как известно (теорема Лёвенгейма — Скулема), во всякую модель бесконечной синтаксической алгебры вроде Nat можно добавить счётно-бесконечный набор элементов-призраков, которые ведут себя как канонические элементы и не могут быть отличены от них наблюдениями, т.е. модели неизоморфны, но наблюдательно-неразличимы.)
akuklev: (ДР Цертуса 2011)
На протяжении 20-го века основным языком классической математики была система NBG (von Neumann-Gödel-Bernays). Теоретико-множественная часть системы NBG называется теорией множеств Цермело-Френкеля с аксиомой выбора (ZFC), разница между ними в том, что на языке ZFC можно говорить только о множествах, и нету грамматического оборота, позволяющего сказать, например, "для всех групп G". А вот NBG это система, где можно определять классы, например всех множеств Set, всех групп Grp, всех колец Rng, при этом она является консервативным расширением ZFC, т.е. все вещи, которые в ней можно доказать "для всех групп Grp" это в точности те же вещи, которые можно доказать про группы в ZFC. Конечно же на языке NBG можно говорить и о таких алгебраических структурах как категории, о классе Cat множеств со структурой категории.

Однако в Cat не входит "категория всех групп", т.к. Grp не множество, я в Cat входят только множества со структурой категории. Зато мы можем отдельно рассматривать два разных понятия,
1) конкретные категории: Классы со структурой категории: Grp, Rng,..
2) малые категории: элементы Cat

На практике от этого получается большая беда, для малых категорий мы можем доказывать общие результаты, скажем "для всякой категории С верно то-то" и производить общие построения, "для всякой категории C мы можем построить Скелет C, Нерв C" и т.д. Но применить эти результаты к большим конкретным категориям навроде Grp мы вообще говоря не можем.

В поисках решения этого вопроса Гротендик придумал понятие иерархии вселенных. Вселенная (Гротендика) это такое множество U, очень похожее на класс всех множеств Set (похожесть выражается в замкнутости относительно базовых тайп-формеров, см. http://en.wikipedia.org/wiki/Grothendieck_universe), но без требования что все другие множества в него входят, в частности U ∉ U. Вместо этого требуется, чтобы для каждого множества s ∈ Set существовала какая-нибудь вселенная U ∋ с. В частности, это означает, что для начиная с любой вселенной U можно построить иерархию U ∈ U' ∈ U'' ∈ ···.
Дальше вместо того чтобы что-то доказывать для (больших) конкретных категорий Grp, Rng и т.п., проводят доказательства для их "усечённых до U" подкатегорий GrpU, RngU. Жить так безусловно можно. Но таскать за собой индексы U в каждой формуле, а впереди каждого высказывания писать "для любой достаточно большой вселенной U" муторно и неэлегантно. (Хотя в Agda так сейчас и живут!)

Решение этого вопроса предлагает теория множеств (strong) ZFC/s Соломона Фефермана: это обычная ZFC/NBG, дополненная постулатом о существовании как минимум одной вселенной Гротендика и схемой генерализации: если мы доказали высказывание pU усечённое до той или иной вселенной U, причём U входит в высказывание только на уровне типов (т.е. связывает свободные переменные), но не термов (это называется proof irrelevance), то автоматически вернен неусечённый вариант p. Отметим, что отдельно постулировать иерархию вселенных не нужно, из определения вселенной и схемы генерализации автоматически следует, что для каждого s ∈ Set существует какая-нибудь вселенная U ∋ с.

Не смотря на то, что сам Феферман недоволен результатом и последние сорок лет периодически возвращается к вопросу о том, как бы вообще обойтись без понятия вселенной при формализации теорката, сами категорные теоретики вполне довольны этим подходом, см. https://golem.ph.utexas.edu/category/2009/11/feferman_set_theory.html, а вопрос детальной работы со вселенными Гротендика, как выяснилось, имеет полезные прикладные стороны как в логике (в отросли интуиционистских теорий типов), так и за её пределами (inter-universal Teichmüller Theory).

Мне же этот вопрос интересен в смысле того, как обращаться со вселенными в функциональных языках программирования и Theorem Prover'ах на базе теорий типов. Думается мне, что будущее за подходом Фефермана, а не за постулированием иерархий вселенных в явном виде.
akuklev: (ДР Цертуса 2011)
В комментах к прошлому посту [livejournal.com profile] krlz прислал линк на более доступное описание (слайды) System S, полиморфного лямбда-исчисления с поддержкой зависимых типов: http://staff.computing.dundee.ac.uk/pengfu/document/talks/rta-tlca-14.pdf.

Выложу ещё из комментов, почему я считаю, что это важно: «Я уже упоминал о вселенском разрыве между тем, как проработаны в смысле computational overhead elimination и оптимизации производительности языки на базе полиморфного лямбда-исчисления (в особенности OCaml и SML), и как убого это выглядит в отношении языков на базе зависимых теорий типов: там вопросы computational overhead elimination и оптимизации — это непаханое поле на десяток лет работы в лучшем случае.

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

Пока мне непонятно, насколько сильна System S. На данный момент у меня впечатление, что я понимаю как там делать indexed containers, но этого мало, на практике хочется умения делать там любые fibered data types, чтобы можно было осуществлять туда трансляцию из Агды. Вообще fibered data types это очень могучая абстракция данных, они включают в себя индексированные индуктивно-индуктивно-рекурсивные типы данных, indexed containers и тем более W-types как мелкие частные случаи. До недавнего времени не было понятно, замкнут ли этот класс типов относительно композиции, и как их описывать так, чтобы для понимания не требовалось 10 лет ботанья жосткого категорного матана, однако судя по всему в этой области недавно случился прорыв: https://pigworker.wordpress.com/2015/01/01/irish-induction-recursion/.

Очень было бы здорово, если бы System S реально предоставляла effective typed (impredicative) lambda-encodings for fibered data types.

Вообще хочется текстбука на тему fibered inductive datatypes, где шаг за шагом разрабатываются примеры хитрых типов данных, начиная от натуральных чисел Nat, конечных чисел Fin(n : Nat), списков List, списков фиксированной длинны Vec(n: Nat), продолжая замысловатыми, но нужными в народном хозяйстве типами данных вроде traffic-dependent session types (включая Conway games, включая surreal numbers), evaluation trees, deduction trees, red-black trees и вообще balanced trees, и заканчивая совсем замысловатыми типами навроде typed abstract syntax trees (incl. case of dependently typed languages), Tarski universes, PER-based and set-theoretic models.

Или можно подождать, пока fibered data types интерпретируют в HoTT/CubTT и обобщат до higher fibered data types (вон Альтенкрих уже весь в работе над higher indexed containers, и вроде там всё гладко), тогда можно будет смело добавлять в текстбук всевозможные quotient types и suspension types:
от Bool получается интервал и спектр сфер, от List получаются Cycle, Collection (aka Finite Multiset) и всевозможные другие Combinatorial Species, от структурированных коллекций всевозможные Concrete Shape Categories; кроме того, можно определить Cauchy Reals, Model of ZFC set theory, univalent universes. Сверхзадачей было бы сделать обогащённое path abstractions (a la Cubical Type Theory) полиморфное лямбда-исчисление, обеспечивающее effective typed (impredicative) lambda-encodings for higher fibered data types.
akuklev: (ДР Цертуса 2011)
One of the most intriguing open problems in the field of Homotopy Type Theory (HoTT) is the internal definition of presheaves on concrete shape categories (simplicial, cubical, dendroidal, opetopic, Segal’s Γ) as well as their variants with extra conditions, leading to internal definition of (weak) ∞-groupoids and (∞, 1)-categories. This is the enabling condition for doing higher category theory internally to HoTT.
In the draft of his Ph.D. Thesis Nicolai Kraus argues that type-valued presheaves on direct categories (including the most basic example of semisimplicial types) can be defined in Homotopy Type Theory augmented by so called Very Dependent Types [Hic96], a powerful generalization of dependent tuples for the case of potentially infinite number of tuple components, that constitute precisely the right structure to contain infinite towers of coherency conditions.

I'm going to explore definability of very dependent types in presence of indexed inductive-recursive types and discuss the right form of elimination rules for them which turns out to be the open induction, necessary for building an internal syntactic model of HoTT, which is an another open problem of tremendous interest.

Term-level Very-Dependent Functions
In Martin-Löf dependent type theories inductive type families come with eliminators that witness the type families being initial objects of their signature. Dependent eliminators are derivable from the non-dependent ones in presence of η-rules.

Analogously, even employing only the non-dependent eliminators for inductive type families, the terms corresponding to very dependent functions can be constructed, but their type render them virtually unusable, until we find a way to fix their type. Let me start with the simplest inductive type Nat = {zero: Nat | succ: Nat -> Nat}. Their non-dependent eliminator nat-rec takes
  T: Type
  zeroVal:
  succVal: (n: Nat, prevVal: T) -> T

and produces a function Nat -> T, i.e. a sequence of the objects of the type T [n0, n1, n2,..]

That's not the most general type of the sequence, a sequence might also have items of different types:
  [n0 : T(0), n1 : T(1), n2 : T(2),..].

Furthermore, type of each next component could be dependent on the value of the previous one:
  [n0 : ZeroT, n1 : SuccT(0, n0), n2 : SuccT(1, n1),..].

Such sequence can be easily defined by mutual recursion on the type and term level, i.e. we'll eliminate Nat into the type (T: Type, value: T):
the recursion base is constituted by pair (ZeroT, zeroVal: ZeroT),
the recursion step is constituted by two functions:
  SuccT: (n: Nat)(T: Type, value: T) -> Type
  succVal: (n: Nat)(T: Type, value: T) -> SuccT(n)(T, value)
.

This construction can be easily used to produce terms for dependent functions on inductive types and dependent pairs: just use Fin(2) as source type and obtain terms for dependent pairs and their special cases: pairs and disjoint unions. Using more involved inductive type families than Nat allows for sequences (or rather trees of potentially infinite depth) with arbitrary manifestly-wellfounded dependency structures. All that appears really nice until we take a look on the types:
  nat-rec(
    (T: Type, T)
    (ZeroT, zeroVal)
    (SuccT; succVal)
 )

has the type Nat -> (T: Type, T). It produces mere pointed sets. There are not many things you can do with objects of the type (T: Type, T) if you adhere to parametrical polymorphism, really not. Except idT, all available maps from this type are constants.

Catching up the Type-Level
We would like to define a type former Nat-recT (ZeroT, SuccT) providing proper type for functions defined in such a way, and improved eliminator
  nat-elim(
    (T: Type, T)
    (ZeroT, zeroVal)
    (SuccT, succVal)
 ) : Nat-recT(ZeroT, SuccT)


Let's try to understand the structure of this type in terms of usual Π- and Σ-types. By employing indexed induction-recursion, we can define the type DepTuple(ZeroT, SuccT): Nat -> Type of dependent sequences truncated to a certain length, together with function prev returning all elements but last. Then we'd be able to define Nat-recT (ZeroT, SuccT) as a Π-Type
  (n: Nat) -> DepTuple(ZeroT, SuccT)(n)
together with rule that longer sequences extend the shorter ones, i.e.
  Nat-recT (ZeroT, SuccT) := (s: (n: Nat) -> DepTuple(ZeroT, SuccT)(n), (n: Nat) -> (s(n) = prev s(n + 1)))

The interesting part is the inductive-recursive definition of DepTuple:

mutual
  DepTuple(ZeroT, SuccT): Nat -> Type
    0 => ZeroT
    succ(n) => (prev: DepTuple(n)) × SuccT(n, last(n, prev))

  last(ZeroT, SuccT): (n: Nat, DepTuple(n)) -> (T: Type, T)
    (0, z: ZeroT) => (ZeroT, z)
    (succ(n), (prev: DepTuple(n), l: SuccT(n, last(n, prev))) => (SuccT(n, last(n, prev)), l)


The case of IIR seems to be perfectly admissible, the dependent pattern matching in definition of "last" does not seem to be a problem either in presence of definitional η-rules. Producing inhabitants of this type seems also quite obvious, we just have to provide a function that produces dependent tuples of fixed length n:

nat-elim-fst(ZeroT, SuccT, zeroVal, succVal): (n: Nat) -> DepTuple(ZeroT, SuccT)(n)
  0 => zeroVal
  succ(p) => nat-elim-fst(ZeroT, SuccT, zeroVal, succVal)(p)

The witness that this sequence is a compatible chain can be easily provided with help of propositional η-conversion.

Thus with help of indexed induction-recursion we obtain a form of very-dependent types. But I'm not sure this is the form we need, because it doesn't provide the strong enough elimination principle per ce.

Eliminators for *-recT: Open induction
Pointwise (aka componentwise if we talk about sequences) transformation of a function f: A -> B means postcomposing it with a function g: (arg: A, fVal: B) -> Y which is dependent on argument arg of f additionally to its value fVal = f(arg). In case of dependently typed function f: (a: A) -> B, the type of postcomposant must be g: (arg: A, fVal: B(arg)) -> Y. When we talk about very-dependent function, the situation gets more complicated. The postcomposant has now to depend on previous values of f and transform values of types of the form (ZeroT | SuccT(n: Nat, prevVal: DepTuple(ZeroT, SuccT)(n))), i.e. f has to be defined for a bi-indexed family of types, the first index is formed by values of inductive type X (domain of f), and the second by values of the type DepTuple. We'll need to be able to define such functions mutually (with respect to DepTuple) recursively (with respect to Nat).

I'm pretty sure such induction principle is exactly the right thing to proceed at the point where Mike Shulman stopped in [Homotopy Type Theory should eat itself]: "At this point I stopped, because I recognized the signs of the sort of infinite regress that stymies many other approaches to semisimplicial types: in order to prove coherence at the n-th level, you need to know (already or mutually) coherence at the (n + 1)-st level, making the whole definition impossible unless you could define infinitely many functions in one mutual recursion."

Very-dependent functions will be used in HoTT to carry the infinitary (but lazily computable) coherence information, we'll need to transform them component-wise by means of an infinite number of functions (one for each component), and define this infinite family of functions mutually-recursively in a way precisely corresponding to open induction a la Berger.

First let's consider the weakly dependent version. Say, we'll be defining function that transforms a sequence (n: Nat) -> Fin(n + 1) by adding element number to each element:
nat-seq-req: (
  InZeroT: Type
    Fin(1)
  InSuccT(n: Nat, _): Type
    Fin(n + 1)

  OutZeroT: Type
    Fin(1)
  OutSuccT(n: Nat, _): Type
    Fin(n + n + 1)

  mapZero: InZeroT -> OutZeroT
    n: Fin(1) => n
  mapSucc(n: Nat)(
    prevInValues: DepTuple(InZeroT, InSuccT)(n)
    lastInValue: InSuccT(n + 1, last(prevValues))
    lastOut: (T: Type, T)
  ) -> OutSuccT(n + 1, lastOut)
    (m: Fin(n)) => n + m
) : Nat-recT (InZeroT, InSuccT) -> Nat-recT (OutZeroT, OutSuccT)


And now there comes the crucial step: we'll allow stepTransformers (mapSucc(n) for succ(n) in case of Nat) to depend on ready sequence transformers restricted to subterms of the eliminated terms (i.e. to n, the only direct subterm of succ(n) in case of Nat). This would presumably allow to define hereditary substitutions in the internal model of HoTT recursively: the substitution function for a term (function which is being defined) can use subsitution functions for subterms as if they were readily defined. Such definition is computationally sane, the recursion will terminate after finite number of steps, because the functional we're defining is known to be continuous already by the fact that we're defining it constructively, but in order to prove it we'll need countable dependent choice. Anyway, here's the updated signature
nat-seq-req: (
  InZeroT: Type
  InSuccT(n: Nat, _): Type

  OutZeroT: Type
  OutSuccT(n: Nat, _): Type

  mapZero: InZeroT -> OutZeroT
  mapSucc(n: Nat)(
    prevInValues: DepTuple(InZeroT, InSuccT)(n)
    lastInValue: InSuccT(n + 1, last(prevValues))
    lastOut: (T: Type, T)
    transform: Nat-recT (InSuccT(n, prev(prevValues)), InSuccT) -> Nat-recT (lastOut.T, OutSuccT)
  ) -> OutSuccT(n, lastOut)
) : Nat-recT (InZeroT, InSuccT) -> Nat-recT (OutZeroT, OutSuccT)


I don't think such powerful form of induction would be readily available in HoTT+IIR, because open induction provides tools to implement a large portion of classical analysis intuitionistically (in particular all sigma-statements derivable under employment of classical (countable) dependent choice are derivable), and provides (modified-)realizability interpretation for the whole classical analysis. It points out that a theory capable of providing that much is much stronger proof-theoretically than usual MLTTs with induction-recursion are (they are known to have proof-theoretical ordinals around Mahlo, whereas the classical analysis Z2 is beyond the tools available in ordinal-theoretic proof theory at the moment).

But still, this form of induction is computationally justified (in contrary to LEM and AC), so it's highly desirable to have a variety of HoTT supporting it and thus capable of doing lots of analysis and higher category theory.
akuklev: (ДР Цертуса 2011)
Николай Краус и коллеги недавно высказали гипотезу, что HoTT можно дополнить ещё одним полезным в хозяйства конструктором зависимых типов данных, впервые упомянутым в 1996 году под названием "очень зависимая функция". Этот конструктор является одновременным обобщением зависимой суммы и зависимого произведения, из-за чего он крайне симпатичен.

Смотрите, это тип пары двух натуральных чисел:
(Nat, Nat)

А вот это тип пары двух натуральных чисел, таких что второе не больше
первого:
(n : Nat, Fin(n))

А вот это тип натуральнозначной функции на натуральных числах:
Nat -> Nat

А вот это более рестриктивный тип, он требует чтобы значение было не больше аргумента:
(n : Nat) -> Fin(n)

Существует совершенно фундаментальная эквивалентность между кортежами (парами, тройками и т.д.) и списками конечной длинны. Для однородных списков это вообще тривиально, (Nat, Nat, Nat) == (Fin(3) -> Nat), для кодирования гетерогенных списков справа потребуются уже зависимые функции:
(A, B, C) == (selector : Fin(3)) -> selector |>
  0 => A
  1 => B
  2 => C


Наша цель в том, чтобы можно было и зависимый кортеж вида
(a : A, b : B(a), c : C(a, b),..)
представить в виде функции. Для этого нам понадобится, чтобы тип значения функции на более старших аргументах мог зависеть от значений этой же самой фукнции на более младших аргументах.
(a : A, b : B(a), c : C(a, b),..) == (sel : Fin(3) -> (\fs => sel |>
  0 => A
  1 => B(fs(0)
  2 => C(fs(1))
))


Именно эта конструкция называется "очень зависимым типом". Она обобщает понятие "зависимого кортежа" на случай кортежей бесконечной длины, индексированных индуктивным семейством типов. Такой конструктор типов позволяет формулировать алгебраические структуры, которые не могут быть конечно аксиоматизированы, и, предположительно, пучки над категорями Риди, в том числе семи-симплициальные и симплициальные типы, слабые омега-группоиды (симплициальные типы Кана), Г-пространства. На данный момент конструкция проработана только для обратных категорий, т.е. случая семи-симплициальных, семи-кубических и т.д. типов.

Указанный выше синтаксис позволяет в теле выражения после -> применять f к любым аргументам, т.е. мы лишены синтаксической защиты от циркулярных определений. При определении конкретной функции f вместе с её типом такую защиту легко организовать. Для начала рассмотрим случай, когда каждый последующий тип кортежа T(n) зависит только от предыдущего значения (а не от всех предыдущих):
mutual
  f: (s : Fin(3)) -> t(s)
    ...

  t: Fin(3) -> Type
    0 => T(0)
    succ(n) => T(n) (f(n))


Тип Fin(3), разумеется, можно заменить на любой другой индуктивный тип, добавив в тело t разбор всех его конструкторов. Тут видно, что как только мы заполним многоточие телом функции f, функция f и её тип будут корректно определены взаимно рекурсивно-индуктивно. Мы без особого труда можем расширить зависимость на ситуацию, когди тип T(n) элемента кортежа зависит от всех предыдущих значений:
mutual
  f: (s : Fin(3)) -> t(s)
    ...

  t: Fin(3) -> Type
    0 => T(0)
    succ(n) => T(n) (fs(n))

  ts: Fin(3) -> Type
    0 => t(0)
    succ(n) => ts(n) × t(n + 1)

  fs: (s: Fin(3)) -> ts(s)
    0 => f(0)
    succ(n) => (fs(n), f(n + 1))


Как и выше, Fin(3) легко обобщается до произвольного индуктивного семейства типов. Как мы видим, синтаксическое определение очень зависимого типа совместно с конкретным представителем такого типа не представляет проблем. Как сформулировать синтаксическое определение очень зависимого типа в отрыве от конкретного представителя? Выше приведён способ развязать этот узел примитивно -- раз тип очень зависимых функций из W определяется функцией t(s: W, fs: subterm(s) -> ...): Type, то и будем писать в качестве формера (s : W) -> (\fs => well-formed type expression), однако возникают вопросы, нет ли более элегантного способа развязать этот узел в духе контейнеров.
akuklev: (ДР Цертуса 2011)
Lean Theorem Prover оказался лучше всех теорем-пруверов, которые я видел до сих пор, удобнее Coq, удобнее Agda (правда, это НЕ язык программирования, это только теорем-прувер). И главное, работает в браузере, не надо ставить всякую древнюю экзотику. И библиотека для гомотопического исчисления построений (HoTT with propositional resizing) сразу приложена. Раньше я экспериментировал с HoTT только на бумаге, неудобно работать было.

Правда синтаксические возможности послабее Агды, это увы. И TeXmode пока, вроде, нет.

[livejournal.com profile] maxim, а вот ещё интересно как оно в сравнении с TLA+ тулбоксом, я его не щупал пока.

Upd: Нету высших индуктивных типов, так что хрен я поиграюсь с тем, что интересно. Ну и взаимно индуктивно-рекурсивных семейств типов тоже ожидаемо нет, она вообще только в Агдачке есть. Охо хо. Нет пока щастья.
akuklev: (ДР Цертуса 2011)
Совсем недавно Андреас Россберг показал, как надо было делать SML, см. http://www.mpi-sws.org/~rossberg/1ml/1ml.pdf. В MLях традиционно (т.е. во всех ML без зависимых типов) существует два независимых уровня языка: языковое ядро и язык описания модулей/функторов. Андреас Россберг, показал как обойтись без такого расслоения, сделать модули first class citizens, и при этом не выйти за рамки System Fω, не потерять разрешимости тайп-чекинга и весьма сильного автовыведения типов, не смотря на довольно сильный сабтайпинг. Конечно знать бы заранее, SML надо было бы основывать именно на этом подходе, он во сто крат элегантнее.

С другой стороны, подход к прозрачности/инкапсуляции в модулях тут ad hoc'овый, в то время как Конор МакБрайд (https://pigworker.wordpress.com/2015/01/05/linear-dependent-types/) показал, как надо. Просто в модулях (они же контексты) поля надо аннотировать элементами моноида {0, 1, *}, 0 это proof-irrelevant-поля, это те самые opaque-поля, значение которых мы не можем смотреть в рантайме, программа относительно них таким образом заведомо параметрично-полиморфна. Элемент * означает, что значение поля можно использовать сколько угодно раз, это как обычно. А вот значение 1, означает что элемент можно использовать ровно один раз, это позволяет представлять resources/entities.

Польза "ООП" в рамках функциональных языков программирования сводится именно к поддержке вот такого синтаксического сахара (не выходяшего за рамки подлежащего исчисления, напр. System Fω), позволяющего удобно описывать тайпклассы и алгебраические структуры более общего вида. Единственное, из соображений того самого удобства, хочется поддержки наследования (не дублировать определения кольца в определении поля) и номинального сабтайпинга (язык должен понимать, что поле это тоже кольцо, раз мы одно от другого унаследовали). Особенно их хочется, когда начинаешь пользоваться орнаментами...
akuklev: (Свечка и валокардин)
То, что прошлый пост написался 31 декабря – чистая случайность. Тем забавнее, что в нём я впервые смог сформулировать математическую мысль которая крутилась на самом деле весь год в голове:
– С тех пор как я поразбирался в HoTT я практически уверен, что это сила, кремень и будущее языков программирования и метаматематики.
– С тех пор как я начитался [livejournal.com profile] codedot'а я понял, что interaction nets рулят. Это реально элегантный, прозрачный, и оптимальный способ записывать пурые вычисления. Не то что машины Тьюринга, алгорифмы Маркова и лямбда-исчисление. Мне всегда казалось, что Fixpoint combinators и Church encoding это некрасивые dirty hacks, привносящие кучу нерелевантного произвола в модель вычислений, а теперь я убедился что это так.

Потом ещё под влиянием размышлений над макросами (спасибо [livejournal.com profile] xeno_by) я стал лиспером мне стало казаться, что тип данных AST должен быть в языках программирования явным и редукция выражений до представлений их значений тоже не должна быть под ковром. А в MLTT оно всё под ковром и очень лямбдёвое в плохом смысле. И вот с тех пор всё крутилось в голове, как бы так скрестить interaction nets и HoTT, да ещё чтобы выражения и их редукция были не под ковром. И вот потом щёлкнуло, что когда мы определяем новую функцию func, то это мы просто дополняем текущий тип AST ещё одним конструктором func, но при этом сразу определяем редукцию, при помощи которой этот конструктор может быть убран. Вот и получился прошлый пост.

На самом деле я уверен, что под тем или иным соусом это точно можно реализовать, и что соответствие Directed Inductive Types ~ Interaction Nets может оказаться весьма глубоким. Например, что такое равенства путей в сетях взаимодействия? — это формализация возможных оптимизаций. Возможно для чего-то может понадобится направленность и на этом уровне, ведь эти самые directed cubical sets как раз используются для того чтобы изучать Higher Automata (n-мерный автомат это просто автомат, у которого n лент ввода, на которые он реагирует независимо, не считая блокировок внутри, которые как раз и есть гомотопические свойства автомата).

Ну и отдельная тема, что HoTT неаскетичная теория, так что в идеале хотелось бы получить её точную истинную модель в рамках какой-нибудь совсем аскетичной теории, где ничего кроме натуральных чисел и диофантовых уравнений. ;-) См. http://akuklev.livejournal.com/1138512.html, естественно. Там всё, конечно, вообще вилами по воде писано, но больно уж красиво.
akuklev: (Свечка и валокардин)
Homotopical Type Theory in its current formulation has a way too huge proof theoretical ordinal strength for a metatheory. It would be practical to have a gradual control over its proof theoretical ordinal by means of adding or removing particular wellfoundness axioms. It seems, it can be easily done: first we have to remove all constructors for product types except linear lambda abstraction (so, no value duplication, no splits, no natrec). We will be able to emulate all this techniques with some help of interaction nets.

In HoTT we can define types with additional equality, for example the circle skeleton and the type of unordered pairs:
Family CircleSkeleton
  GenericPoint (CircleSkeleton)
  Loop (GenericPoint = GenericPoint)
Family Couple (TypeType)
  Couple (T (Type), a (T), b (T) ⇒ Couple[T])
  Mirror (T (Type), a (T), b (T) ⇒ [Couple[T, a, b] = Couple[T, b, a]])

HoTT types form (∞,0)-categories, but we probably could allow nonreflexive arrows on the first H-Level to represent incomplete (or nonterminating) computations. Let's define a type of Natural numbers together with possibly incomplete addition:
Family Nat (Type)
  Zero (Nat)
  Succ (NatNat)
Directed-Family Nat-Plus-Addition extending Nat
  Add (Nat, NatNat-Plus-Addition)
  ZeroReduction (x (Nat) ⇒ [Add [Zero, x] = x])
  SuccReduction (a (Nat), b (Nat) ⇒ [Add[Succ[a], b] = Succ[Add[a, b]]])

Nat-Plus-Addition is now the type of expressions involving natural numbers and addition, and we can, step-by-step, by applying reductions, convert it to a Nat, preserving equality. ZeroReduction and SuccReduction are the computation rules in sense of Interaction Nets. Assuming univalence, ‖Nat-Plus-Addition‖ = Nat means precisely that Nat-Plus-Addition can always be reduced to Nat.

How can we prove that some ‖Type-Plus-Computation‖ = Type?
We certainly can do it only relatively to some wellfoundness postulate. Optimally, we have to represent ordinals α as universal interaction nets Cα of complexity up to α, than map interaction net Type-Plus-Computation in question onto Cα in such a way that elements of type Type are mapped onto Zero. The postulate that o is wellfounded should then have the form Cα = Unit we should be able to conclude that Type-Plus-Computation = Type.
Probably, we could use Takeuti Diagrams (encoded as Directed-Families) as universal interaction nets of corresponding complexities.
akuklev: (Свечка и валокардин)

Introduction


We regard theory as a conglomerate of a language for writing statements, a language for writing valid proofs and a collection of axioms (basis of statements the theory assumes to be true). A theory is said to be consistent if there is no pair of valid proofs proving contradictory statements. A theory is said to be capable of reflection iff it's possible to write the statement "this theory is consistent" in the language of the theory itself.

There are three main results concerning consistency:
1) (Gödel's Second Incompleteness Theorem) All common non-trivial theories cannot prove their own consistency. This applies essentially to all theories that include the notion of an infinite ordered set with a distinguished zero object (e. g. natural numbers) and provide a way to construct a larger object for any given one.

2) (Gentzen's Algorithm) For common theories there is an algorithm that "analytically verifies" their proofs. Analytically checked proofs can be directly shown to be contradiction-free. This does not contradict to the (1) because no theory which is subject to (1) can internally show that verification algorithm holds for every valid input.

3) (Dan Willard's Self-verifying theories) There are non-trivial exceptions to (1). They are not only capable of reflection, but even prove their own consistency.

The theories (3) share a common property: their proofs can be analytically verified inplace. Whereas for theories which Gödel's Theorem (1) applies the algorithm normally requires enormous amounts of additional working space. This goes so far that analytical verification of some proofs could be fundamentally physically infeasible due to finiteness of the visible universe.

This could be a clue to understanding the Gödel's Theorem (1): maybe the true reason we cannot show Gentzent's algorithm to succeed always without additional assumptions exactly because it doesn't phyiscally do so.

In this case we could use a physical estimate for information content of the visible universe and restrict our attention to proofs of the "modest" length which are at least in theory verifiable. Then we'd be pretty sure that these proofs are definitely noncontradictous. If it would turn out that upper bound on proof length is beyond that of normal human-developed proofs, a longstanding question about solidity of mathematical foundations would be at least partially solved.

Now how can we find the upper bound for proof length starting with informational content of the universe? It appears that the following approach could roughly do.

The Programme

Read more... )
Page generated Jul. 20th, 2017 10:33 pm
Powered by Dreamwidth Studios