[Agda] mu-nu in Agda

[Andreas Abel]

Hi Thorsten,

On May 29, 2010, at 1:43 PM, Thorsten Altenkirch wrote:
>  the use of
> impredicativity destroys normalisation (try to normalize "f
> bad"). While I assume "Type:Type" System F style impredicativity would
> be sufficent (you only need a "weak large Σ-type to encode T, indeed
> this is the type-theoretic representation of a left Kan extension).
>
> I remember that Thierry once remarked that the structural order in a
> impredicative system isn't always well-founded. I think this example
> is an instance.

This is in Thierry's 1992 paper on pattern matching.  I treat this  
counterexample in Sec. 6.6 of my thesis (page 144 of the printed  
copy).  Guess what: No paradox arises here for sized types.

> Also, Coq seems to avoid this problem by checking that
> structural recursion may only use "recursive arguments", hence the Coq
> terminationchecker isn't untyped.

Bruno Barras is well aware of the trap.

If you look at a simplified version of your T

data T : Set where
   node' : ∀ {X} → (X → T) → T

you will notice that it is not far from

data T : Set where
   node' : (T → T) → T

so you will be able to encode self-application and Omega.  foetus  
assumes predicativity, so Agda's termination checker will not alert you.

> We were also wondering wether it would be already possible to encode
> this example using a predicative hierarchy (which would be bad). Do
> you see a way to do this? I don't.

I'd be surprised.

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/