![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Fully coherent HITs and open recursion
Nov. 29th, 2014 05:21 amFor n-truncated higher inductive types
> Infinitary loop types
Loop space of A: Type is the type ΩA(a: A) := (p: a = a) that contains paths from a to a, i.e. loops. For example the loop space of a S1 is Z. Higher loop spaces may be also defined:
Ω^2 a := (p1: a = a) × (p2: p1 = p1)
Ω^3 a := (p1: a = a) × (p2: p1 = p1) × (p3: p2 = p2)
One can also define the infinitary loop type
So, the triv constructor is used to denote an element followed by an infinite chain of refl's, and the cons constructor is used to construct the nontrivial values. Every map f: (x: X) -> Y between HITs A and B induces the map coh(f): ω(x) -> ω(f x)
(Note to self: probably, ω should be defined as a 0-truncation of the above definition.)
For n-truncated types T, the infinitary loop type ω should be equal to Ω^m for m >= n, but for the HITs of infinite h-level the infinitary loop type ω necessarily contains at least sequences of arbitrary length, but might also contain (it's the case if T is has constructor branching at every level) sequences of infinite length. In this case, the infinitary loop type ω has structure of a cantor set.
> Open recursion
Open recursion comes into play when we want to define a function from a type of infinite h-level. Typically, it's easy to define the action of the function on the constructors of the source type, but hard (or impossible with usual means) to show that the function respects all the coherence conditions of the source type, i.e. that nontrivialy equal source terms are mapped onto equal target terms.
Usual recursion on inductive types goes as follows: to define f: (x: X) -> Y(x) you provide a recursor for each constructor c(a, b,.., z) of X. The recursor is an expression defining the value of f(c(a, b,.., z)) assuming the values of f for each subterm a, b,..,c of c(a, b,.., z) is already known.
When performing recursion on HITs we should in a fact construct not only the function f(x), but also the coherence map coh(f)(x). This can be naturally done by simultaneously providing f(x) and coh(f)(x) for each constructor of a HIT while assuming that f(x) and coh(f)(x) are both known for subterms of x. This generalization allows functions to have nontrivial actions on loop spaces and restricts equalities of HITs to be infinitely coherent syntactically. This form of recursion is strictly stronger than the usual one. It is is equivalent to open recursion as introduced by Berger[1], which is tightly connected to bar recursion.
[1] Ulrich Berger, "A Computational Interpretation of Open Induction", http://www.cs.swan.ac.uk/~csulrich/ftp/open-ieee.pdf
> Infinitary loop types
Loop space of A: Type is the type ΩA(a: A) := (p: a = a) that contains paths from a to a, i.e. loops. For example the loop space of a S1 is Z. Higher loop spaces may be also defined:
Ω^2 a := (p1: a = a) × (p2: p1 = p1)
Ω^3 a := (p1: a = a) × (p2: p1 = p1) × (p3: p2 = p2)
One can also define the infinitary loop type
data ω: {T: Type} -> (e: T) -> Type where
triv: (e: T) -> ω(e)
cons: (e: T) -> (l: Ω(e)) -> ω(l) -> ω(e)
triv-to-cons: (e: T) -> ((triv e) = (cons e (refl e) (triv refl e)))
head: ω(e) -> Ω(e)
head (triv e) = refl e
head (cons e p ps) = a
tail: (x: ω(e)) -> ω(head x)
tail (triv e) = triv (refl e)
tail (cons e p ps) = cons p (head ps) (tail ps)So, the triv constructor is used to denote an element followed by an infinite chain of refl's, and the cons constructor is used to construct the nontrivial values. Every map f: (x: X) -> Y between HITs A and B induces the map coh(f): ω(x) -> ω(f x)
(Note to self: probably, ω should be defined as a 0-truncation of the above definition.)
For n-truncated types T, the infinitary loop type ω should be equal to Ω^m for m >= n, but for the HITs of infinite h-level the infinitary loop type ω necessarily contains at least sequences of arbitrary length, but might also contain (it's the case if T is has constructor branching at every level) sequences of infinite length. In this case, the infinitary loop type ω has structure of a cantor set.
> Open recursion
Open recursion comes into play when we want to define a function from a type of infinite h-level. Typically, it's easy to define the action of the function on the constructors of the source type, but hard (or impossible with usual means) to show that the function respects all the coherence conditions of the source type, i.e. that nontrivialy equal source terms are mapped onto equal target terms.
Usual recursion on inductive types goes as follows: to define f: (x: X) -> Y(x) you provide a recursor for each constructor c(a, b,.., z) of X. The recursor is an expression defining the value of f(c(a, b,.., z)) assuming the values of f for each subterm a, b,..,c of c(a, b,.., z) is already known.
When performing recursion on HITs we should in a fact construct not only the function f(x), but also the coherence map coh(f)(x). This can be naturally done by simultaneously providing f(x) and coh(f)(x) for each constructor of a HIT while assuming that f(x) and coh(f)(x) are both known for subterms of x. This generalization allows functions to have nontrivial actions on loop spaces and restricts equalities of HITs to be infinitely coherent syntactically. This form of recursion is strictly stronger than the usual one. It is is equivalent to open recursion as introduced by Berger[1], which is tightly connected to bar recursion.
[1] Ulrich Berger, "A Computational Interpretation of Open Induction", http://www.cs.swan.ac.uk/~csulrich/ftp/open-ieee.pdf
