[Agda] Ensuring termination during equality checking

[Andreas Abel]

I recall you mentioned once to me that, internally, Agda converts 
pattern-matching definitions into case-trees.  But this does not seem to 
happen, so my question is futile.

(In the "rewriting" approach that is implemented and that harmonizes 
with Agda syntax, equality of defined functions is by name and not by 
structure.)

Cheers,
Andreas

Ulf Norell wrote:
> 
> 
> On Sun, Mar 2, 2008 at 7:58 PM, Andreas Abel <abel at cs.chalmers.se 
> <mailto:abel at cs.chalmers.se>> wrote:
> 
>     Hi Ulf,
> 
>     in my experience, it is easier to come up with a strongly normalizing
>     reduction relation for "rewriting", where recursion and pattern matching
>     are tied together, than for "functional languages" where recursion and
>     case trees are used in separation.  [cf. Nicolas Oury's talk at DTP]
> 
>     Now I am interested in the strategy for equality checking used in Agda2.
> 
>     It seems that complications are avoided at the moment by omitting
>     congruence rules for case (and recursion?) altogether.
> 
> 
> I'm not exactly sure what you mean by the congruence rules for case and 
> recursion. In any case, Agda doesn't have a case construct. "with" is a 
> convenient way to define helper functions. For instance,
>  
> 
>     ifzero' : {A : Set} -> Nat -> A -> A -> A
>     ifzero' x a b with x
>     ... | zero = a
>     ... | _    = b
> 
> 
> is equivalent to
> 
> ifzero'-aux : {A : Set} -> Nat -> A -> A -> Nat -> A
> ifzero'-aux x a b zero = a
> ifzero'-aux x a b _ = b
> 
> ifzero' : {A : Set} -> Nat -> A -> A -> A
> ifzero' x a b = ifzero'-aux x a b x
> 
> / Ulf

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/