# Nottingham FP Lab Blog

## Induction-Recursion and Impredicativity

by Venanzio on December 6, 2012.
Tagged as: Lunches, Type theory meetings.

The type theory meeting of Wednesday 5 December was a short introduction to induction-recursion with a divagation about impredicativity.

### Type Universes

Martin-Löf distinguishes universes à la Russell and universes à la Tarski. The difference is that a Russell-style Universe $${\mathsf{U}}$$ is a type such that any of its elements $$A:{\mathsf{U}}$$ is itself a type; while a Tarski-style universe is a set $${\mathsf{U}}$$ of codes together with a decoding function $${\mathsf{Elem}}: {\mathsf{U}}\rightarrow {\mathsf{Type}}$$.

A simple Tarski universe with non-dependent types can be defined by plain induction and the decoding function is given by recursion on it: $\begin{array}{l} {\mathsf{U}}: {\mathsf{Type}}\\ {\mathsf{zero}}: {\mathsf{U}}\\ {\mathsf{one}}: {\mathsf{U}}\\ {\mathsf{plus}}: {\mathsf{U}}\rightarrow {\mathsf{U}}\rightarrow {\mathsf{U}}\\ {\mathsf{times}}: {\mathsf{U}}\rightarrow {\mathsf{U}}\rightarrow {\mathsf{U}}\\ \end{array} \quad \begin{array}{l} {\mathsf{Elem}}: {\mathsf{U}}\rightarrow {\mathsf{Type}}\\ {\mathsf{Elem}}\,{\mathsf{zero}}= \emptyset\\ {\mathsf{Elem}}\,{\mathsf{one}}= \{\bullet\}\\ {\mathsf{Elem}}\,({\mathsf{plus}}\,a\,b) = {\mathsf{Elem}}\,a + {\mathsf{Elem}}\,b\\ {\mathsf{Elem}}\,({\mathsf{times}}\,a\,b) = {\mathsf{Elem}}\,a \times {\mathsf{Elem}}\,b \end{array}$

But when we want to add constructors $${\mathsf{pi}}$$ and $${\mathsf{sigma}}$$ for dependent products and sums to $${\mathsf{U}}$$, then the definitions of $${\mathsf{U}}$$ and $${\mathsf{Elem}}$$ become entangled: $${\mathsf{Elem}}$$ occurs in the type of the constructors of $${\mathsf{U}}$$: $\begin{array}{l} {\mathsf{pi}}: {\Pi\,}a:{\mathsf{U}}, ({\mathsf{Elem}}\, a \rightarrow {\mathsf{U}}) \rightarrow {\mathsf{U}}\\ {\mathsf{sigma}}: {\Pi\,}a:{\mathsf{U}}, ({\mathsf{Elem}}\, a \rightarrow {\mathsf{U}}) \rightarrow {\mathsf{U}}\\ \ \\ {\mathsf{Elem}}\, ({\mathsf{pi}}\,a\,b) = {\Pi\,}x:{\mathsf{Elem}}\, a, {\mathsf{Elem}}\, (b\, x)\\ {\mathsf{Elem}}\, ({\mathsf{sigma}}\,a\,b) = {\Sigma\,}x:{\mathsf{Elem}}\, a, {\mathsf{Elem}}\, (b\, x) \end{array}$ This was the first instance of an inductive-recursive definition: the simultaneous specification of an inductive type and a recursive function on it.

The construction can be iterated and generalized. We can define another universe $${\mathsf{U}}_1$$ that contains $${\mathsf{U}}$$ by the same recursive-inductive specification plus a code $$\mathsf{u}_0:{\mathsf{U}}_1$$ with associated type $${\mathsf{Elem}}\, \mathsf{u}_0 = {\mathsf{U}}$$. In fact, if we already defined an entire family of universes, we can use this construction to create an new universe that contains them all. Eric Palmgren introduced a superuniverse that is closed under this universe-creation rule.

### Induction-Recursion

Peter Dybjer further generalized the construction and invented simultaneous inductive-recursive definitions. These allow us to define an inductive type together with a recursive function on it. The function is allowed to appear in the type of the constructors; but there must be syntactic restrictions to guarantee that it is applied to arguments that are smaller than the one generated by the constructor. Later Dybjer and Anton Setzer devised a elegant type of codes for inductive-recursive definitions (we'll look at it on a future meeting).

A simple example is the type of lists without repetitions, by Catarina Coquand. The type is defined simultaneously with a freshness relation that guarantees that we can only add elements that are not already in the list. $\begin{array}{l} {\mathsf{FList}}\, (A:{\mathsf{Set}}): {\mathsf{Set}}\\ {\mathsf{fnil}}: {\mathsf{FList}}\, A\\ {\mathsf{fcons}}: {\Pi\,}x:A, {\Pi\,}l:{\mathsf{FList}}\, A, {\mathsf{Fresh}}\, x\, l \rightarrow {\mathsf{FList}}\, A\\ \ \\ {\mathsf{Fresh}}: A \rightarrow {\mathsf{FList}}\, A \rightarrow {\mathsf{Prop}}\\ {\mathsf{Fresh}}\, x\, {\mathsf{fnil}}= \top\\ {\mathsf{Fresh}}\, x\, ({\mathsf{fcons}}\, y\, l\, p) = (x\neq y) \land {\mathsf{Fresh}}\, x\, l \end{array}$

Ana Bove and I used inductive-recursive definitions to formalize general recursive functions in type theory. The idea is to characterize the domain of a function by an inductive predicate and then define the function itself by recursion on the proof of the predicate. Take for example the quicksort algorithm. In Haskell it is written as:

quicksort :: [A] -> [A]
quicksort [] = []
quicksort (x:l) = quicksort ll ++ x : quicksort lr
where ll = [y | y <- l, y<=x]
lr = [y | y <- l, y>x]


In this case the function happens to be total: we can prove that the domain predicate is always satisfied, $$H:\forall l:{\mathsf{List}}\,A, {\mathsf{D}_{{\mathsf{qs}}}}\,l$$. Therefore, we can eliminate the dependency on the proof: $${\mathsf{quicksort}}: {\mathsf{List}}\,A \rightarrow {\mathsf{List}}\,A$$, $${\mathsf{quicksort}}\,l = {\mathsf{qs}}\,l\,(H\,l)$$.

If the recursive function we try to implement has nested recursive calls, then we need induction-recursion. Take for example McCarthy's 91 function:

mccarthy :: Int -> Int
mccarthy n | n > 100 = n - 10
| otherwise = mccarthy (mccarthy (n+11))

The function always terminates and returns 91 on every argument less or equal to 101. However, the recursive calls are made on arguments that may be larger than the original input and are nested. We can formalize it in type theory in the same style as the quicksort algorithm:


### Impredicativity

I've been a bit too casual in defining the domain predicates as functions to $${\mathsf{Prop}}$$. There are issues related to the consistency of elimination rules between type universes. You can simply adopt the Curry-Howard correspondence in full and replace $${\mathsf{Prop}}$$ everywhere with $${\mathsf{Set}}$$. However, if instead you have a separate impredicative universe of proposition (as, for example, in Coq), then there are consistency problems.

Impredicativity refers to the possibility of quantifying over a type universe and obtaining an element of that same universe. In general, the formation rule of product types can be formulated as follows: $\dfrac {A:s_1 \quad x:A \vdash B[x]:s_2} {{\Pi\,}x:A, B[x] : s_3}$ where $$s_1$$, $$s_2$$ and $$s_3$$ are sorts (type universes). One can define a Pure Type System by specifying a set of such rules simply by giving the triples $$(s_1,s_2,s_3)$$ and some axioms in the form $$s_1:s_2$$. We have that a sort $$s_1$$ is impredicative if there is an axiom $$s_1:s_2$$ and a rule for $${\Pi\,}$$-types with triple $$(s_2,s_1,s_1)$$. In our specific case, $$s_1 = {\mathsf{Prop}}$$ and $$s_2 = {\mathsf{Set}}$$: we can quantify over any set, including the set of all propositions.

The most famous impredicative theory is Girard's system F. Girard proved that the normalization property of his system was equivalent to the consistency of second order Peano Arithmetic, that is, analysis. He then proved normalization with the new technique of reducibility candidates.

Although pure type systems only have function types, in an impredicative theory we can encode inductive types by the polymorphic quantification of their iterators. For example, the natural numbers can be defined in system F as ${\mathbb{N}}= {\Pi\,}X:{\mathsf{Set}}, X \rightarrow (X\rightarrow X) \rightarrow X$ (In this case it is the sort $${\mathsf{Set}}$$ that's impredicative).

If $${\mathsf{Prop}}$$ is impredicative, eliminating an inductive proposition over a set like I have done is forbidden. Allowing this kind of elimination in general would lead to a contradiction, a version of Girard's paradox described by Thierry Coquand.


### References

• Per Martin-Löf, Intuitionistic type theory, Napoli, Bibliopolis, 1984.

• Eric Palmgren, On universes in type theory, in: G. Sambin and J. Smith (eds.) Twenty Five Years of Constructive Type Theory, Oxford Logic Guides, 1998.

• Peter Dybjer, A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory, J. Symb. Log. 65(2): 525-549 (2000).

• Peter Dybjer and Anton Setzer, A Finite Axiomatization of Inductive-Recursive Definitions, TLCA 1999:129-146.

• Ana Bove and Venanzio Capretta, Nested General Recursion and Partiality in Type Theory, in TPHOLs 2001, LNCS 2152, pages 121-135.

• Henk Barendregt, Lambda calculi with Types, in: Handbook of Logic in Computer Science, Vol 2, OUP, (1992), pp 117-309.

• Jean-Yves Girard, Yves Lafont and Paul Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science, 1989

• Thierry Coquand, An Analysis of Girard's Paradox, LICS 1986: 227-236.