[TYPES] Re: Reg Axioms of pure type systems

[Thorsten Altenkirch]

Param Jyothi Reddy wrote:

>As Thorsten pointed out PTS does not impose such conditiosn but the
>point being we might loose consistency. Any necessary and sufficient
>conditions on A and R to ensure that PTS is consistent?
>  
>
Paul-Andre Mellies and Benjamin Werner attempted something like this, see
http://pauillac.inria.fr/~werner/pts.dvi.gz
(there may be a newer version).

>Also am i correct in assuming "consistency iff Strong normalization"?
>
>  
>
Seems plausible but there may be monsters. E.g. the empty PTS is
inconsistent
(there isn't an empty type) but strongly normalizing. :-)

T.

>Param
>
>
>On Mon, 27 Dec 2004 08:34:28 +0530, Param Jyothi Reddy <paramr at gmail.com> wrote:
>  
>
>>Hi all,
>>I have a doubt regarding the pure type systems.  Let it be (S, A, R)
>>
>>In A we have sorting relation on the sorts (s_1:s_2 kind of data). Are
>>there any conditions on these? (Not like functional or injective but
>>more inherent for arbitrary PTS).
>>
>>Like for example is circularity allowed (s_1:s_2 and s_2:s_1)?
>>
>>Regards,
>>Param
>>
>>    
>>



This message has been scanned but we cannot guarantee that it and any
attachments are free from viruses or other damaging content: you are
advised to perform your own checks.  Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.