[Agda] termination

[Conor McBride]

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.

> but it is not fair.

What has fairness got to do with it?

> And if it is possible
> here, it is not neccecary possible in general

Neither is proof of termination. 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. Don't complain about getting trouble if
you ask for it. Suffering is very adult.

All the best

Conor