[FOM] on Bas Spitters on "constructive impredicativity?"
gstolzen at math.bu.edu
Wed Mar 29 00:07:53 EST 2006
Here I make a brief response to Bas Spitters' reply to my message,
> On Monday 27 March 2006, Gabriel Stolzenberg wrote:
> > That was then. Now, I am very comfortable with impredicative
> > definitions. In fact, I think some of them are marvelous.
> Which ones do you have in mind?
It's been over 15 years since I looked at them but, if I remember
correctly, e.g., in Thierry Coquand's proof of Kruskal's theorem.
(I'm talking about a version that I'm pretty sure he didn't publish.)
> My impression is that such a (constructive) impredicative definitions is
> usually an invitation to find an inductive definition. This inductive
> definition is usually easier to understand (for me).
> ALF (or agda/alfa as it is now called) is predicative. Coq used to be
> impredicative (based on Coquand/Huet's calculus of constructions), but
> recently (v8.0) they changed the type system so that it is predicative.
> (Well, the computational part of the system is predicative. The issue
> is too technical to go into here.) Their motivation, as I understand
> it was that the impredicative definitions were just too difficult to
> understand for most users. They were contradicting set-theoretical
That's very interesting. The impredicativity seemed so elegant.
How do they now introduce the logcial constants? Also, how does the
shift to predicativity effect type checking?
More information about the FOM