[Agda] acyclicity of constructors

[Conor McBride]

Hi Dan

Bit of a classic, this one...

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

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

[..]

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

If acyclicity isn't built into unification for pattern
matching, then you're going to need to do the proof by
hand. There are various strategies for doing so, trading
simplicity and genericity (see below).

> (2) Is this behavior intentional, or just an implementation issue?

I don't know how this is done in Agda, but I did just
try this example in Epigram 1 and (to cut a long story
short) discovered to my surprise that I had neglected to
implement acyclicity. Back in the old Lego days, I
automated the disproof of such equations, mostly because
James McKinna told me not to. I didn't port my Lego
treatment to Epigram because I'd thought of a better
one. But I evidently didn't get around to implementing
the new version. I found the place in the code where I
could add it, if only I remembered how any of it worked.

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

Of course, not every occur-check failure corresponds to
a disprovable equation, but one may readily check if
there's a constructor-path to an occurrence (remembering
that the first occurrence may not be the only one).

[..]

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

Until acyclicity is built in, the induction is inevitable:
it's an inherently inductive property. Indeed, in a slightly
less intensional system, /co/constructor cycles could result
in solving with an unfold.

In the meantime, there are lots of ways to do these proofs.
You can reduce all other cyclic equations x = P[x] to
Id n (S n) one by a kind of "division"

   quotP P[x] = S (quotP x)
   quotP _    = 0

but you have to define one quot per constructor path. More
amusing is to define _notLt_ for each type, eg, for trees

   _notLt_ : Tree -> Tree -> Set
   x notLt Leaf = True
   x notLt (Node s t) =
     (Id x s -> False) /\ (x notLt s) /\
     (Id x t -> False) /\ (x notLt t)

Note that (x notLt P[x]) computes to a big tuple somewhere
containing the rather helpful assertion (Id x x -> False).
So prove

   acyclicTree : {s t : Tree} -> Id s t -> s notLt t

However, with a bit more generic programming, one should
really just prove a single acyclicity result expressed via
the generic zipper construction.

And round we go.

All the best

Conor