KnowledgeBase » SEMINAR » ID = 718

Quotient Types in Nuprl

by Mark Bickford
2013

Abstract:

One of the ways that Nuprl differs from Coq and Agda is that Nuprl has quotient types. The quotient type T//E is the type T with the equality relation E. We use quotients to, for example, construct the rational numbers, the integers "mod n", and the type Bag(T) = List(T)//permutation.

We recently added a new type constructor per(R) that is defined by a partial equivalence R on the terms in type Base. The per-type is a generalization of the quotient type and we can now define the quotient type using the per type.

The advantage of this is that we can reason about the per-type using only four primitive rules (and these four rules have all been proved correct by Vincent from the definitions using Coq) whereas there had previously been ten rules for reasoning about the primitive quotient type.

I will discuss how quotients are used in Nuprl, look at some example proofs, and then show the new definition from the per-type and look at the rules for the per-type.

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