The Coq mailing list

[Neel Krishnaswami <krishnan AT cs.bham.ac.uk>]

On 11/08/14 11:51, Andrej Bauer wrote:> On Sun, Aug 10, 2014 at 10:25 
PM, Abhishek Anand
> 
<abhishek.anand.iitg AT gmail.com>
 wrote:
>> The terms (v1:A1 -> B1)  and (v2:A2 -> B2) denote equal PI types in 
Nuprl
>> iff
>> A1 and A2 are equal types
>> and
>> forall terms a1 and a2 such that a1 and a2 are equal members of A1,
>> B1[v1\a1] and B2[v2\a2] are equal types.
>
> Unless you intend to introduce crazy recursive types this is not a
> problem: equality on PI_{x:A} B(x) is defined in terms of equality on
> A and equality on B, where these two equalities have been previously
> defined. So this is still a fixpoint which uses structural recursion
> on the structure of a type. Why would you be unhappy with that?

If you try to formulate the typing rules in the obvious way --- by
giving mutually-recursive judgements for context well-formedness, type
and term well-formedness, and equality --- then the definition of the
type system is clearly structural. However, you will not be able to do
induction on derivations to prove that weakening is sound, which in
turn prevents you from being able to show the soundness of
substitution in any easy way.

AFAIK, Nuprl avoids these problems by defining only the universe of
types and their corresponding PERs recursively, but showing that this
definition is well-founded requires a surprisingly powerful fixed
point principle (at least, it surprised me).

In particular, if you look at Bob Harper's *Constructing Type Systems
Over an Operational Semantics*, you'll see that he needs the fact that
a monotone (note: not continuous) function on a CPPO has a least fixed
point, which is a fixed point principle he establishes by transfinite
induction and excluded middle. (This is stronger than either the Kleene
or Knaster-Tarski fixed point theorems.)

(Martin Escardo and Paul Taylor tell me that Dito Pataraia showed that
this fixed point theorem also holds in intuitionistic set theory, but
to my knowledge there isn't a predicative version of it.)

-- Neel