[Agda] Positivity checker

[Peter Dybjer]

On Dec 8, 2008, at 10:10 AM, Nils Anders Danielsson wrote:
>>
>> The reason why this data type is ok, is because it is isomorphic to  
>> the corresponding family defined by induction on n.
>> But what is the induction principle? Except induction on n?
>
> Do you suggest that one could inadvertently introduce new (stronger)
> induction principles by accepting this type (or similar types)?

It depends on what the termination checker would do when pattern  
matching on this data type. But my feeling is that there is no natural  
induction principle associated with this type, except induction on n.

My feeling is that the recursive function version is the basic one  
conceptually, and the data type version is just an encoding of that,  
which inserts extra constructors. It is still not "morally"  
inductively defined. If you try to build a model of the theory  
extended with this new data type you would again do induction on n.

I find your arguments for prefering inductively to recursively defined  
families interesting, but hardly conclusive. My own feeling is that it  
depends on the situation which is better. For cases like Vec, the  
inductive one is a "generator" and the recursive one simplifies.

For the case in question (with negative occrurences) I would want  
stronger arguments before it feels worth-while trying to extend the  
positivity checker with some general principle which would instantiate  
to this one. If we after all extend the system we should make sure  
that it is correct:

1. (Extensional correctness.) It should satisfy the "meaning  
explanations" which says that all functions in the extended system  
should terminate in a suitable sense. To prove this rigourously one  
could build a (realizability) model.

2. (Intensional correctness.) It should result in a system with  
decidable type-checking in the usual sense.

Peter