[Agda] termination

[Permjacov Evgeniy]

On 03/03/2011 01:19 PM, Conor McBride wrote:
>
> On 3 Mar 2011, at 09:32, Permjacov Evgeniy wrote:
>
>> On 03/03/2011 12:02 PM, Conor McBride wrote:
>>>
>>>  How can I write a different but adequate program, which obviously
>>>    terminates?
>>>
>>> May I respectfully suggest that you consider implementing instead
>>> addition-with-carry?
>>>
>>> All the best
>>>
>>> Conor
>>>
>> I do know, how to write similiar program that obviously terminates.
>> That's a little childish,
>
> I'm not sure how to react to that. If it's childish to prefer to
> reduce the complexity of the problem, then I'm an enthusiast for being
> childish.
>
Desire to reduce complexity is very adult. So, why you deals with
computer science? it is quite complex and there are much more simple
jobs. If you work or even tries to work within science, you already have
fallen to desire for challenges, so known sin of pride, that is very
childish in nature.

> There may be good general strategies
> for organising termination proofs, but there's no general method for
> doing them.
>
> If you want to get termination cheaply, you should write with
> termination in mind.
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.