[Agda] Problem with coinduction and positivity checker

[Nils Anders Danielsson]

On 2010-01-21 14:57, Simon Foster wrote:
> Is this a bug in Agda or a theoretical problem?

I had a look at the example. If you inline ♭, then the code is accepted:

  mutual
    data ωChain : Set where
      _∷_,_ : ∀ (x : Carrier) (xω : ∞ ωChain) (p : x ≼ xω) → ωChain

    head : ωChain → Carrier
    head (x ∷ _ , _) = x

    ♭′ : {A : Set} → ∞ A → A
    ♭′ (♯ x) = x

    _≼_ : Carrier → ∞ ωChain → Set
    x ≼ xω = x ≤ head (♭′ xω)

I don't suggest that you should inline ♭, though: we are considering
making it a primitive.

Ulf, Thorsten and I have recently discussed extending the termination
checker so that inlining changes the termination behaviour less often.
However, even if we don't do this I would not call this a bug: there
will always be some "correct" program which is not accepted by the
termination checker. It would be better to have a language of
certificates for termination, so that if the termination checker cannot
handle your code, then you can write the proof yourself.

I should also mention that I am not aware of any theoretical work on
coinduction-(co)recursion. Agda allows you to experiment with such
definitions, but don't take Agda's acceptance of your code as a strong
indication that it is correct.

As an alternative you could perhaps use the following definition of
ωChain:

  data ωChain : Carrier → Set where
    _∷_,_ : ∀ x {y} → ∞ (ωChain y) → x ≤ y → ωChain x

--
/NAD