Fwd: [Agda] Parallel or

[wren ng thornton]

On 11/16/11 4:39 PM, Alan Jeffrey wrote:
> 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.

Alternatively, rather than trying to automatically determine the 
equivalence of the RHS, we could enforce it syntactically / require it 
intensionally by introducing or-patterns a la OCaml. Thus,

     or True _ || or _ True = True
     or False False = False

(using whatever syntax you'd prefer.)

That's still just a syntactic approximation to semantic properties, but 
at least it's a relatively decent syntactic approximation instead of 
something completely ad hoc.



Yet a different alternative is that we could take the masking as a 
feature rather than a burden. Thus defining,

     or False False = False
     or _ _ = True

In theory, given (or x y) if we can prove either x=True or y=True, then 
we should be able to force the whole expression to evaluate to True. 
This approach would also work for addition on naturals. However, it 
doesn't scale as well as the or-pattern option, because it's not clear 
how to get it to cover non-atomic cases like

     mplus Nothing (Just x) || mplus (Just x) Nothing = Just x

and the moral equivalents, where we're binding variables but we don't 
care about exactly where they come from.

-- 
Live well,
~wren