[Agda] Forget Hurken's Paradox, Agda has a quicker route to success

[Andreas Abel]

On 06.09.12 6:47 PM, Nils Anders Danielsson wrote:
> On 2012-09-06 17:21, Andreas Abel wrote:
>> The problem is that Agda considers
>>
>>    F D = \Sigma E : Set. (D ≡ E) * (E → ⊥)
>>
>> as strictly positive in D.
>
> I'm trying to understand if this is actually a problem. Are there any
> dire consequences if we stick to predicative types?

The semantics of Agda's "strictly positive" has not been written down, 
it is a bit of a moving target.  Usually, strictly positive should at 
least imply "monotone", and that is violated by F.  F is antitone.

The problem is that in X \equiv Y, Agda considers X as "unused" and Y as 
"negative" (meaning not strictly positive).  Their status should be both 
"negative".  Agda treats parameters of data type as "unused" even if 
they appear in the indices of one of the constructors (such as in refl).

I have a fix for this (filed as issue 690), that looks also for 
occurrences in the indices.

>> If I try the same in Coq, it is rejected because the definition of D
>> is not considered strictly positiv.
>
> How does Coq's positivity checker work? Is the usual definition of rose
> trees accepted (T A = A × List (T A))?

Coq's checker is much more basic.

Cheers,
Andreas

-- 
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/