The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

In a predicative setting:
Uniform datatypes can be reduced to W-types (in an extensional setting).

However, it is not clear wether we can do this for non-uniform datatypes.
(Actually I think we can't).

If this is true then do non-uniform datatypes extend the strength of the
system?

And is there a universal type like W covering non-uniform operators?

Thorsten

On 24/11/2011 08:55, "Andreas Abel" 
<andreas.abel AT ifi.lmu.de>
 wrote:

>If you want some literature on this, I can advertise the paper by Ralph
>and myself:
>
>Fixed Points of Type Constructors and Primitive Recursion
>Andreas Abel and Ralph Matthes
>Computer Science Logic, 18th International Workshop, CSL 2004, 13th
>Annual Conference of the EACSL
>Karpacz, Poland, September 2004. LNCS 3210,  Springer.
>
>http://www2.tcs.ifi.lmu.de/~abel/publications.html#csl04
>
>It is about Fomega, no dependencies, but the principles stay the same
>for CC.
>
>Cheers,
>Andreas
>
>On 21.11.11 2:36 AM, Peter LeFanu Lumsdaine wrote:
>>>> On Wed, 16 Nov 2011, Bruno Barras wrote:
>>>>
>>>>> Putting what Matthieu already said with my own words:
>>>>> non-uniform parameters behave
>>>>> (1) like normal indices w.r.t. recursive schemes
>>>>> (2) like parameters w.r.t. dependent pattern-matching (check out
>>>>> list'_case)
>>
>> Many thanks to those who replied both on- and off-list; this makes a
>> lot of sense now.
>>
>> Best,
>> Peter.
>>
>>
>
>-- 
>Andreas Abel  <><      Du bist der geliebte Mensch.
>
>Theoretical Computer Science, University of Munich
>Oettingenstr. 67, D-80538 Munich, GERMANY
>
>andreas.abel AT ifi.lmu.de
>http://www2.tcs.ifi.lmu.de/~abel/


This message and any attachment are intended solely for the addressee and may 
contain confidential information. If you have received this message in error, 
please send it back to me, and immediately delete it.   Please do not use, 
copy or disclose the information contained in this message or in any 
attachment.  Any views or opinions expressed by the author of this email do 
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.