[Agda] termination

[Conor McBride]

On 3 Mar 2011, at 10:47, Permjacov Evgeniy wrote:

>>
> Desire to reduce complexity is very adult. So, why you deals with
> computer science? it is quite complex

I study computer science from a desire to reduce its complexity.

>>
> Since I write proofs and definitions that should be formalization of
> very basics of math, I want them be more or less readable. I keep in
> mind complexity of code writing, but this is not the only parameter
> optimized. Splitting function in two, both of wich obviously  
> terminates,
> does work here. However it produces garbage in the namespace and
> requires simply more code to read. That is often a flaw, and agda
> already requires a much of words.
>

You pays your money; you takes your choice. Make sure you compare  
fairly,
though: weigh the program which obviously terminates against the pair of
the more obscurely terminating program with its termination proof.

I'm sorry to have provoked you. I just meant to suggest that solving the
slightly more general problem of addition-with-carry might give you a
cleaner solution, because it has a neater, more compositional structure.

All the best

Conor