[Agda] Ensuring termination during equality checking

[Ulf Norell]

On Sun, Mar 2, 2008 at 7:58 PM, Andreas Abel <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080302/30dde84e/attachment.html