How far can we go with Induction-Recursion?

by Abhishek Anand, Vincent Rahli
2013

Abstract

Induction-Recursion(IR) is a way of simultaneously constructing an inductive type and a recursive function on that inductive type. We will explain why this is a sensible predicative construction and give examples of some concepts which are best expressed in this manner.

We will show how to encode IR using just indexed(parametric) Induction and why this encoding is problematic when the simultaneously defined function returns a type. Indeed, IR is more than a syntactic convenience -- It increases the proof theoretic strength of a type theory.

We will show how IR lets us define all of the Nuprl's universes(w/o Inductive Types) in a single universe of Agda, and why this cannot be achieved with just Induction. We will conclude with a discussion on how Nuprl's Inductive types can be added to this definition.

Date: November 20, 2013
Time: 4-5pm
Location: Upson 5135

How far can we go with Induction-Recursion?

by Abhishek Anand, Vincent Rahli 2013

by Abhishek Anand, Vincent Rahli
2013