[FOM] constructive impredicativity?

[Bas Spitters]

On Monday 27 March 2006 22:42, 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?

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).

>    In a different direction, I would recommend looking at the role
> of impredicative definitions in constructive high level programming
> languages/formal systems like ALF, Coq or LEGO.

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 intuitions.

Bas

-------------------------------------------------------
Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/
P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands.
spitters at cs.ru.nl Ph:+31-24-3652631 F:+31-24-3652525 Room: A5024