KnowledgeBase » SEMINAR » ID = 711

The power of bar induction in constructive type theory

by Mark Bickford
2013

Abstract:
What is the relation between Coq's Calculus of Inductive Constructions and Nuprl's Constructive Type Theory? Can one be embedded in the other? Vincent & Abhishek are working on an embedding of (most of) Nuprl in Coq, using Stuart Allen's PER semantics. I am interested in the other direction. In Coq, the inductive constructions are (a very powerful) primitive, but are not primitive in Nuprl. Can we build these inductive constructions in Nuprl? And, if so, what primitive building blocks do we need?

I think that we can build inductive constructions using a parameterized family of W-types, and further that we can build such families from the "well founded part" of a co-recursive family of types dual to the W-types. Some people name these co-W-types, M-types, but we prefer to call them Spreads. We can build co-recursive types and families of types using the natural numbers and intersection. We can then define the "well founded part" of these types and get the induction principle we need using the bar induction rule.

To introduce the ideas we need for this construction, I will first review the bar induction rule and some of its easier consequences. For example, we can use bar induction to show that there is an induction principle for any relation R that has a positive form of "no infinite descending chain".

Next, we will define the Spread type, the co-inductive version of the W-type, and, time permitting, I will show how to construct the W-type from the Spread, using bar induction to prove the induction principle.

If there is time I will discuss how these constructions can be generalized to the mutually recursive families of types that are needed to get the full power of Coq's inductive constructions.

A pleasing conjecture is that Coq can be proved sound using Nuprl + Bar Induction and that Nuprl (without Bar Induction) can be proved sound in Coq. Thus, Bar Induction is, in a sense, the only axiom that must be assumed.

Date: September 25, 2013
Time: 4:00 - 5:00 pm
Location: Upson 5130