[Agda] acyclicity of constructors

[Thorsten Altenkirch]

Hi Dan,

personally, I'd prefer if acyclicity is not handled by pattern  
matching - since it relies on the fact that the type is inductive and  
I think pattern matching should behave uniformly for inductive and  
coinductive types. The knowledge whether a type is inductive or  
coinductive should only affect termination arguments, i.e. the proof  
of acyclic is only total if we assume that Nat is inductive.

I am not sure what precisely you mean by (2)? Certainly yoo shouldn't  
be allowed to assume that you can solve an acyclic equation either,  
because this would force the type to be coinductive. I.e. the coverage  
checking and unification should be agnostic wrt the question whether  
cyclic equations can be solved.

I have to add that I have no idea what and why is implemented in Agda.

Cheers,
Thorsten

On 28 Jun 2008, at 02:10, Dan Licata wrote:

> Hi everyone,
>
> This morning here at LICS, we were trying a cute little example in
> various proof assistants:
>
> Define (a) raw (untyped) syntax for lambda terms, and (b) inference
> rules for type assignment, where the type of a lambda-bound variable  
> is
> non-deterministically guessed.  Now show that omega (i.e. \ x . x x)  
> is
> not well-typed.
>
> In Twelf and Delphin, there's not much to do because (1) the bound
> variable has a unique type, which means the typing rule for  
> application
> can only be applied by unifying \tau and (\tau arrow \sigma) for some
> \tau,\sigma and (2) the coverage checker notices this cyclic equality,
> and therefore leaves you with 0 cases to consider.
>
> When James Chapman and I tried the problem in Agda, we couldn't get  
> the
> coverage checker to rule out cases automatically based on a cyclic
> equation.  The best we came up with was to do the proof of acyclicity
> ourselves (see an abstracted version below).
>
> So, two questions:
> (1) Is there a better way of handling this right now?
>
> (2) Is this behavior intentional, or just an implementation issue? It
> seems that Agda already commits to constructors being acyclic: when we
> pattern-matched deep enough to force the cyclic equality, Agda told us
> that we couldn't do that because \tau != (\tau arrow \sigma) ---  
> exactly
> the unification failure that should rule out the case!
>
> Thanks!
> -Dan
>
> module Occurs where
>
>  data Nat : Set where
>    Z : Nat
>    S : Nat -> Nat
>
>  data Id : Nat -> Nat -> Set where
>    Refl : forall {m} -> Id m m
>
>  data False : Set where
>
>  invert : forall {m n} -> Id (S n) (S m) -> Id n m
>  invert Refl = Refl
>
>  -- is there a way to write this without doing the induction?
>  acyclic : (n : Nat) -> Id n (S n) -> False
>  acyclic Z ()
>  acyclic (S n) p = acyclic n (invert p)
> _______________________________________________
> 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.