<p>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.</p>
<p>As the authors note, this is the most complicated part of the theory itself.</p>
<p>Let's break it down:</p>
<p><strong>The datatype:</strong></p>
<p>The inductive type <span class="math-container">$K$</span> itself, is defined within a given universe <span class="math-container">$\mathsf{U}_\ell$</span> with certain parameters, denoted as <span class="math-container">$a :: \alpha$</span>. In the case of <span class="math-container">$\mathsf{Vect}$</span> that might be <span class="math-container">$\forall n:\mathsf{Nat}.\mathsf{U}_0$</span>.</p>
<p><strong>The constructors:</strong></p>
<p>Here we need a positivity restriction for the recursive bits (that refer to <span class="math-container">$K$</span> 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.</p>
<p>Because the types of the constructors are the only important bits in the definition of the inductive type, the body of <span class="math-container">$K$</span> itself is just <span class="math-container">$\Sigma_c(\mbox{the type of the constructor $c$})$</span>. But that means that the &quot;name&quot; of <span class="math-container">$K$</span> doesn't actually exist! So, instead, within the type of the constructors, the variable <span class="math-container">$t$</span> is used, and it's bound by the <span class="math-container">$\mu$</span> construct at the top level of the declaration.</p>
<p>For <span class="math-container">$\mathsf{Vect}_{\mathbb{Z}}$</span> (integer valued vectors of fixed length), that would be:</p>
<p><span class="math-container">$$ \mu t.\{\mathsf{nil}: t\ 0\} + \{\mathsf{cons}:\forall n, \forall tl:t\ n, \forall e:\mathbb{Z}, t\ (S\ n)\} + 0$$</span></p>
<p><strong>The recursor:</strong></p>
<p>Ok, so this is starting to take shape. The recursor basically takes, for each constructor, a function of the &quot;result&quot; of the recursive calls, and <em>also</em> the arguments of the constructor (which may be of the inductive type itself!) to the output type <span class="math-container">$C \ldots$</span></p>
<p>Note that <span class="math-container">$C$</span> is a dependent type <em>shape</em>, it needs to be applied to stuff.</p>
<p>Let's leave aside the large elimination <span class="math-container">$\mathsf{LE}$</span> case for the moment.</p>
<p>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 &quot;shape&quot; <span class="math-container">$C$</span>, but in the position where the inductive arguments were, and with the extra subterm argument. This is accomplished by replacing the <span class="math-container">$t\ \mbox{something}$</span> constructor arguments by <span class="math-container">$C\ \mbox{something}\ \mbox{subterm}$</span>. This is the part denoted as
<span class="math-container">$$ C\ \pi_i[b, x](u_i x)$$</span></p>
<p>the result of that call needs to be applied to the term itself, which is the
<span class="math-container">$$C\ p[b]\ (c\ b) $$</span>
bit. For <span class="math-container">$\mathsf{Vec}_{\mathbb{Z}}$</span>, letting <span class="math-container">$\mathsf{Vec} = \mu t.\{\mathsf{nil}: t\ 0\} + \{\mathsf{cons}:\forall n, t\ n\rightarrow\mathbb{Z}\rightarrow t\ (S\ n)\} + 0$</span>, as above, that would give
<span class="math-container">$$\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$$</span></p>
<p>(that was hard to get right!)</p>
<p>You can see that the arguments of <span class="math-container">$\mathrm{rec}$</span> have similar shape to the constructors, with <span class="math-container">$C$</span> substituted in the right places with an additional argument.</p>
<p>If <span class="math-container">$\mathsf{LE}$</span> holds, it just means you're allowed to replace <span class="math-container">$\mathbb{P}$</span> in the above by the more permissive <span class="math-container">$\mathsf{U_u}$</span> for some fresh universe.</p>
<p>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 <a href="http://www.cse.chalmers.se/%7Epeterd/papers/DependentTypesAtWork.pdf" rel="nofollow noreferrer">Dependent Types at Work</a>.</p>

CC BY-SA 4.0
2023-05-16T23:06:09.137Z
2023-05-16T23:06:09.137Z
cody
<p>I need some help working through the type of the recursor, the eliminator for the inductive type. If</p>
<ul>
<li><span class="math-container">$F=\forall a::\alpha.\mathsf{U}_\ell$</span></li>
<li><span class="math-container">$P=\mu t:F.K$</span></li>
<li><span class="math-container">$K=\sum_c(c:\forall b::\beta.tp[b])$</span></li>
<li><span class="math-container">$u::\gamma\subseteq
   b::\beta$</span> is a subsequence with <span class="math-container">$\gamma_i=\forall
   x::\xi_i.P\pi_i[b,x]$</span>,</li>
</ul>
<p>and if <span class="math-container">$\Gamma,b::\beta\vdash p[b]::\alpha$</span> is a sequence of terms depending on the nonrecursive arguments in <span class="math-container">$b::\beta$</span> and <span class="math-container">$\Gamma,b::\beta,x::\xi_i\vdash\pi_i[b,x]::\alpha$</span> is also a sequence of terms, then the type of the recursor is given by the following rule:</p>
<p><span class="math-container">$$
\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}
$$</span></p>
<p>where <span class="math-container">$\kappa=\forall a::\alpha.Pa\to\mathsf{U}_u$</span> and <span class="math-container">$u$</span> is a fresh universe variable if <span class="math-container">$\Gamma;t:F\vdash K\ \mathsf{LE}$</span>, and otherwise <span class="math-container">$\kappa=\forall a::\alpha.Pa\to\mathbb{P}$</span>; <span class="math-container">$\varepsilon$</span> is a sequence of the same length as <span class="math-container">$K$</span>, where <span class="math-container">$\varepsilon_c=\forall b::\beta.\forall v::\delta.Cp[b](cb)$</span>; <span class="math-container">$\delta$</span> is a sequence of the same length as <span class="math-container">$\gamma$</span>, where <span class="math-container">$\delta_i=\forall x::\xi_i.C\pi_i[b,x](u_ix)$</span>.</p>
<p>Can anyone explain this?</p>
<p>Edit: The link to find the paper which discusses Lean's type theory is the following: <a href="https://github.com/digama0/lean-type-theory/releases/tag/v1.0" rel="nofollow noreferrer">https://github.com/digama0/lean-type-theory/releases/tag/v1.0</a></p>
<p>Once on the website, viewing main.pdf will present you with the paper. The definition is in Section 2.6.3 &quot;The recursor&quot;.</p>

CC BY-SA 4.0
2023-05-10T20:15:51.757Z
Can you add a link to where you got this info?
cody
CC BY-SA 4.0
2023-05-12T13:09:06.877Z
@cody just added, it is the paper written for Lean's type theory
Alex Byard
CC BY-SA 4.0
2023-05-12T19:34:36.937Z
The experts are (also) at https://proofassistants.stackexchange.com, I think more of the Lean hackers are hanging out there than here.
Andrej Bauer
CC BY-SA 4.0
2023-05-12T20:15:15.003Z
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)
cody
CC BY-SA 4.0
2023-05-12T20:18:12.767Z
Be my guest. It's Fruday night over here.
Andrej Bauer
<type-theory>
Type of the Recursor in Lean
Alex Byard
# Type of the Recursor in Lean

(Asked by: username_0 on 2023-05-10)

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".

**Tags:** type-theory

> **Comments:**
> **username_1**: Can you add a link to where you got this info?  
> **username_0**: @username_1 just added, it is the paper written for Lean's type theory  
> **username_2**: The experts are (also) at https://proofassistants.stackexchange.com, I think more of the Lean hackers are hanging out there than here.  
> **username_1**: 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)  
> **username_2**: Be my guest. It's Fruday night over here.  

---

## 1 answers

### Answer by username_1 on 2023-05-16. Score: 2 | Accepted answer

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](http://www.cse.chalmers.se/%7Epeterd/papers/DependentTypesAtWork.pdf).


---

