Fwd: [Agda] Parallel or

[Andreas Abel]

I welcome this discussion!  I am also often confused that the equations 
I write in Agda do not hold definitionally.  Here is a feature request

   http://code.google.com/p/agda/issues/detail?id=408

that equations that do not hold for open terms are distinguished.  E.g., 
in the case

   foo T y = T
   foo x T = T
   foo F F = F

only one of equations 1 and 2 can hold definitionally always.  My 
proposal was to need to give permission to Agda to split on a variable. 
  E.g.

   foo T !y = T
   foo x  T = T
   foo F  F = F

would force Agda to first split on the second argument, because x cannot 
be split.  In this case, foo x T = T would hold, but not foo T y = T for 
neutrals x, y.

Your proposal, Alan, can be generalized to allow any proven equation to 
be used as rewrite rule.  (Isabelle does this, and Coq modulo theories). 
  The hard problem is to maintain confluence and termination.

Cheers,
Andreas

On 16.11.11 11:14 PM, Alan Jeffrey wrote:
> On 11/16/2011 03:56 PM, Dan Doel wrote:
>> On Wed, Nov 16, 2011 at 4:39 PM, Alan Jeffrey<ajeffrey at bell-labs.com>
>> wrote:
>> You want to rule that out entirely? Or just rule out the extra
>> definitional rewrites if the check fails?
>
> I'd be tempted to go for the brutal (oh and not exactly
> backward-compatible) approach and rule it out entirely. I am cruel and
> heartless.
>
>> I'm not sure I'm behind the former, but the latter is what I'd expect.
>> I don't know how hard it is to check either, though.
>>
>> As for why the former is bad, I want to write definitions like:
>>
>> foo T y = true
>> foo x T = true
>> foo x y = false
>>
>> Or, replace x and y with _ if you wish. And imagine that the data type
>> that has T as a constructor also has 7 other nullary constructors, and
>> I don't want to write out all the permutations that the last case
>> covers.
>
> This is true for defining functions, but breaks down a bit when you come
> to prove properties about foo, at which point you discover yourself
> having to write all the cases out anyway. And I find myself proving
> properties about programs more than I do writing them :-) For example:
>
> foo1 : forall x y -> foo x y == true -> (x == T \uplus y == T)
> foo1 T y z = inj1 refl
> foo1 x T z = inj2 refl
> ... oh dear lots of cases needed here ...
>
> Mind you, since we're discussing vaporware programming languages at this
> point, you could say that the fix would be for the pattern-matcher to
> keep track of previously matched patterns, to allow that last line to be
> "foo1 x y ()".
>
> A.
>
>> -- Dan
>>
>>> Of course this would come with its own problems, e.g. checking critical
>>> pairs may be expensive, throws up algorithmic issues (e.g. checking
>>> unification of critical pairs may include recursive calls to the
>>> function
>>> being checked, eeks) and it's yet another syntactic approximation to a
>>> semantic property. So I can well believe there is a tar-pit there.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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