Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Open recursion in HoTT

In the famous blog article http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/ Mike Shulman says: "[..] I needed to know that the interpretation functions also took composites of substitutions to composites of maps between types. 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."

Defining infinitely many functions in one mutual recursion is precisely what Open Recursion a la Berger is.

First let's take a look on usual well-founded recursion. In type-theoretic setting, there is an inductive type (family) defined by a set of typed constructors. Terms defined by these constructors are by definition finite chains of constructors. If one substitutes a correspondingly typed function for each constructor and performs all reductions, one gets a value, that's how terms can be recursively transformed. Seen from the other perspective, this process can be described filling a dictionary step by step. All terms arising from inductive type family can be enumerated, the relation _is-subterm-of_ is well-founded by definition. In course of recursion, the dictionary term->value is filled step by step by a function that performs case analysis on the root constructor of the term can look up the dictionary entries for its subterms. Wellfoundness of the subterm relation guarantees that this process eventually fills every entry in the dictionary.

Open recursion works on possibly infinite sequences, such that truncations of the sequences are wellfounded, but the sequences as whole are not. (In type theoretic setting this idea can be used to work with untruncated higher inductive type families.) In this case the dictionary-filling performs case analysis on root constructors of the first n entries (n unbounded but guaranteed to be finite), is allowed to perform dictionary lookup for the subterms of inspected truncation and to transform the tail in a computable way. The ability to look unbounded but fixed number of terms ahead makes the thing ill-defined if any recursion rules were allowed, but as long as recursion rules are totally-computable, open recursion is total and productive: computable inbound sequences (in particular the truncated ones) produce computable results.

Now let's try to apply this idea to higher inductive types. Arguably simplest higher inductive type is the sphere S¹:
Family S¹:
  base : S¹
  loop : base = base
For performing recursion we need the following data
Structure S¹-recdata:
  *TargetType : S¹ -> Type
  base-img : TargetType base
  loop-img : base-img =[TargetType loop]= base-img

(We allow for the following abuse of notation: any function f: A -> B can be applied not only to values of the type A, but also on paths p over A, p : (*x: A, *y: A, x = y), the result being action of p on paths of B. We use the mixfix operator of heterogenious equality x =[p]= y, where p is a path X = Y, x: X, y: Y.)

Using r : S¹-recdata you can eliminate both values x : (x : S¹) and paths l: (x = y) for (x, y : S¹). Since S¹ is 2-truncated it suffices to have two eliminators:
S¹-elim : (r : S¹-recdata) -> (x : S¹) -> (r.TargetType x)
βloop/elim : (r : S¹-recdata) -> (S¹-elim r) loop = r.loop-img
For 3-truncated type T we would also need a transformer for CoherentlyEqualVec 3 T = (a, b, c : T, d : a = b, e : b = c, f : d = e), and so on. In general one would like to have a transformer for coherently equal vectors of any length, preferably even infinite one. Infinite coherently equal vectors can be equivalently described as coherently constant functions, const C = (T : Type, f : ||T|| -> C) which naturally leads to the following type of recursor:
C-elim: (r : C-recdata) -> (x : const C) -> r.TargetType x
(Here we extend the above mentioned abuse of notation allowing functions f: A -> B to be applied to const A, resulting in const B, i.e. we perform application of paths to paths on all levels.)

To transit to open recursion, we just supply "ready eliminator" restricted to the corresponding constructor to each constructor eliminator, just like this:
Structure S¹-recdata:
  *TargetType : S¹ -> Type
  base-img : {coh-elim (TargetType base)} -> TargetType base
  loop-img : {coh-elim (TargetType loop)} -> base-img =[Target-Type loop]= base-img
where
coh-elim : {C : Type} -> (T : C -> Type) -> (s : C) -> (c : const (s = s)) -> T c
For truncated types this is certainly trivial, but for nontruncated ones it's far from being so. In particular, open recursion should be able to express definition of heriditary substitution of unbounded level, so combining it with induction would lead to definition of semi-simplicial types and alike.
Subscribe

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments