akuklev: (ДР Цертуса 2011)
[personal profile] akuklev
Предлагается трактовать обозначения [T :> Nat] и [T <: Nat] как [T : NNO] и [T : CoNNO] соответственно, где
@Structure NNO:
  @on N : Type
  zero : N
  succ : N -> N

@Structure CoNNO:
  @on N
  rec[T : NNO](n : N) : T
  rec[:T](zero) = T.zero
  rec[:T](succ(:n)) = T.succ(rec[T](n))


Отметим, что если N1 N2 : NNO ∧ CoNNO, то между типами N1 и N2 имеется изоморфизм, причём каноническим представителем этого класса эквивалентности типов является
@Family Nat:
  zero : Nat
  succ : Nat -> Nat


Для любого индуктивного типа IndT можно автоматически генерировать структуры IND-T и CoIND-T, таким образом проясняя что подразумевается под [T :> IndT] и [T <: IndT]. Наличие таких обозначений позволяет в общем виде описать тип рекурсора для любых индуктивных типов:
IndT.rec[X <: IndT <: Y](x : X) : Y

* * *

В присутствии унивалентности или аксиомы K из обычного рекурсора можно сделать зависимый:
Сперва определим вот такой подтип NNO:
@Structure IndexedNNO:
  @on N : Type
  zero : N
  succ : N -> N
  |(n : N)| : Nat
  |zero| = zero
  |succ(:n)| = succ(|n|)


Разумеется Nat.rec можно примерять и к N : IndexedNNO, более того, для таковых несложно будет показать что lemma1(n : Nat) : |Nat.rec[N](n)| = n. А с другой стороны можно определить
@Structure NatMotive:
  N(n : Nat) -> Type
  zero : N(zero)
  succ(n : Nat) : N(n) -> N(succ(n))


и для любого m : NatMotive снабдить сигма-тип (n : Nat, m.N(n)) структурой inno(m) : IndexedNNO c m.|p| = fst(p), что позволит нам ввести
@def Nat.elim(m : NatMotive, n : Nat): m.N(n)
  apply-path-to-fst(lemma1(n))(Nat.rec[inno(m)](n))


* * *

При всей этой красоте у меня остаются существенные вопросы по семантике.
Если для структуры NNO семантика понятна (NNO-алгебры суть диалгебры для функторов F(N : Type): (Unit, N) и G(N : Type): (N, N)), то со структурой CoNNO семантика мне пока не вполне понятна из-за полифорфности операции rec. Т.е. если зафиксировать конкретную вселенную Type_n, то вполне работает та же диалгебраическая семантика, а если не фиксировать, то вместо одной категории диалгебр у нас будет целое гротендиково расслоение таковых над категорией NNO-алгебр. Аналогичным образом надо бы понять, что такое семантически NNO ∧ CoNNO.
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 03:52 pm
Powered by Dreamwidth Studios