1
$\begingroup$

I need some help working through the type of the recursor, the eliminator for the inductive type. If

  • $F=\forall a::\alpha.\mathsf{U}_\ell$
  • $P=\mu t:F.K$
  • $K=\sum_c(c:\forall b::\beta.tp[b])$
  • $u::\gamma\subseteq b::\beta$ is a subsequence with $\gamma_i=\forall x::\xi_i.P\pi_i[b,x]$,

and if $\Gamma,b::\beta\vdash p[b]::\alpha$ is a sequence of terms depending on the nonrecursive arguments in $b::\beta$ and $\Gamma,b::\beta,x::\xi_i\vdash\pi_i[b,x]::\alpha$ is also a sequence of terms, then the type of the recursor is given by the following rule:

$$ \frac{\Gamma,t:F\vdash K\ \mathsf{spec}} {\Gamma\vdash\mathsf{rec}_P:\forall C:\kappa.\forall e::\varepsilon.\forall a::\alpha.\forall z:P\ a.C\ a\ z} $$

where $\kappa=\forall a::\alpha.Pa\to\mathsf{U}_u$ and $u$ is a fresh universe variable if $\Gamma;t:F\vdash K\ \mathsf{LE}$, and otherwise $\kappa=\forall a::\alpha.Pa\to\mathbb{P}$; $\varepsilon$ is a sequence of the same length as $K$, where $\varepsilon_c=\forall b::\beta.\forall v::\delta.Cp[b](cb)$; $\delta$ is a sequence of the same length as $\gamma$, where $\delta_i=\forall x::\xi_i.C\pi_i[b,x](u_ix)$.

Can anyone explain this?

Edit: The link to find the paper which discusses Lean's type theory is the following: https://github.com/digama0/lean-type-theory/releases/tag/v1.0

Once on the website, viewing main.pdf will present you with the paper. The definition is in Section 2.6.3 "The recursor".

$\endgroup$
5
  • $\begingroup$ Can you add a link to where you got this info? $\endgroup$
    – cody
    May 10 at 20:15
  • $\begingroup$ @cody just added, it is the paper written for Lean's type theory $\endgroup$
    – Alex Byard
    May 12 at 13:09
  • $\begingroup$ The experts are (also) at proofassistants.stackexchange.com, I think more of the Lean hackers are hanging out there than here. $\endgroup$ May 12 at 19:34
  • $\begingroup$ Ok, though this is sort of a theory question, or at least a "notational" one, I'll try to answer as soon as I get a minute (or @AndrejBauer will get there first) $\endgroup$
    – cody
    May 12 at 20:15
  • $\begingroup$ Be my guest. It's Fruday night over here. $\endgroup$ May 12 at 20:18

1 Answer 1

2
$\begingroup$

Ok, let's try to unpack this a bit. Basically we are trying to define a recursor for a very general inductive datatype in a very complex type theory, with dependent types, universes and impredicativity.

As the authors note, this is the most complicated part of the theory itself.

Let's break it down:

The datatype:

The inductive type $K$ itself, is defined within a given universe $\mathsf{U}_\ell$ with certain parameters, denoted as $a :: \alpha$. In the case of $\mathsf{Vect}$ that might be $\forall n:\mathsf{Nat}.\mathsf{U}_0$.

The constructors:

Here we need a positivity restriction for the recursive bits (that refer to $K$ itself) in the types of the constructor, and, because we're in dependent type theory, we don't want later types to depend on the recursive arguments of the constructors.

Because the types of the constructors are the only important bits in the definition of the inductive type, the body of $K$ itself is just $\Sigma_c(\mbox{the type of the constructor $c$})$. But that means that the "name" of $K$ doesn't actually exist! So, instead, within the type of the constructors, the variable $t$ is used, and it's bound by the $\mu$ construct at the top level of the declaration.

For $\mathsf{Vect}_{\mathbb{Z}}$ (integer valued vectors of fixed length), that would be:

$$ \mu t.\{\mathsf{nil}: t\ 0\} + \{\mathsf{cons}:\forall n, \forall tl:t\ n, \forall e:\mathbb{Z}, t\ (S\ n)\} + 0$$

The recursor:

Ok, so this is starting to take shape. The recursor basically takes, for each constructor, a function of the "result" of the recursive calls, and also the arguments of the constructor (which may be of the inductive type itself!) to the output type $C \ldots$

Note that $C$ is a dependent type shape, it needs to be applied to stuff.

Let's leave aside the large elimination $\mathsf{LE}$ case for the moment.

So we need a way to describe the types those recursive calls, and of course the arguments of the constructors themselves. The recursive calls should have arguments of "shape" $C$, but in the position where the inductive arguments were, and with the extra subterm argument. This is accomplished by replacing the $t\ \mbox{something}$ constructor arguments by $C\ \mbox{something}\ \mbox{subterm}$. This is the part denoted as $$ C\ \pi_i[b, x](u_i x)$$

the result of that call needs to be applied to the term itself, which is the $$C\ p[b]\ (c\ b) $$ bit. For $\mathsf{Vec}_{\mathbb{Z}}$, letting $\mathsf{Vec} = \mu t.\{\mathsf{nil}: t\ 0\} + \{\mathsf{cons}:\forall n, t\ n\rightarrow\mathbb{Z}\rightarrow t\ (S\ n)\} + 0$, as above, that would give $$\mathrm{rec}_{\mathsf{Vec}} : \forall C:\forall n:\mathsf{Nat}, \mathsf{Vec}\ n \rightarrow \mathbb{P},\\ C\ 0\ \mathsf{nil}\rightarrow \left(\forall n:\mathsf{Nat}\ z:\mathbb{Z}\ v:\mathsf{Vec}\ n,C\ n\ v\rightarrow C\ (S\ n)\ (\mathsf{cons}\ n\ z\ v)\right)\rightarrow\\ \forall n:\mathsf{Nat}\ v:\mathsf{Vec}, C\ n\ v$$

(that was hard to get right!)

You can see that the arguments of $\mathrm{rec}$ have similar shape to the constructors, with $C$ substituted in the right places with an additional argument.

If $\mathsf{LE}$ holds, it just means you're allowed to replace $\mathbb{P}$ in the above by the more permissive $\mathsf{U_u}$ for some fresh universe.

Let's just finally note that this is all is a pretty standard fare for a system with dependent types and universes, but grokking it does require some familiarity with such systems first, so if the above still seems impenetrable, you might want to make sure you understand the basics of dependently typed elimination, e.g. Bove and Dybjer's Dependent Types at Work.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.