Subject: Re: acyclicity of constructors Newsgroups: gmane.comp.lang.agda Date: Saturday 28th June 2008 11:34:50 UTC (over 10 years ago) 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 |
|||