[Agda] mutual strangeness

[Thorsten Altenkirch]

A few thoughts:

Actually there are two issues with mutually inductive and inductive  
recursive definitions which should be considered independently:
i) We have to avoid to much circularity to make sense. E.g. we can  
only pattern match once we have seen all constructors.
ii) We may have negative occurences if they are on structurally  
smaller instances. This allows the definition of universe-like
      constructions.

Actually, in my intended application (total syntax of Type Theory)  
only the first issue arises, the ii) is not relevant since the syntax  
is finitary.

I believe it should be possible to justify a very liberal approach re  
i). Clearly every constant and definition has to appear before it is  
used. One should expect that all constructors and cases appear  
together, even though there are case where one would like to  
interleave those as well. However, this may get a bit tricky to justify.

For ii) one would hope that it is sufficent to say that negative  
occurences may appear on structurally smaller recursive calls. One  
should hope that this can be justified via Anton's Mahlo universe.

Thorsten

On 1 Feb 2009, at 13:27, Nils Anders Danielsson wrote:

> On 2009-02-01 12:16, Thorsten Altenkirch wrote:
>> On 1 Feb 2009, at 04:43, Nils Anders Danielsson wrote:
>>> A better alternative might be to try to come up with new rules for
>>> mutually recursive definitions, preferably both flexible and easy to
>>> understand.
>> Indeed, and moreover these rules should be justified, ideally by a  
>> translation into a core type theory with a fixed set of combinators.
>
> Indeed. Moreover this translation should ideally be simple and
> transparent, and the core theory simple and consistent. :)
>
> -- 
> /NAD
>
> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


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.