[Agda] termination

[James McKinna]

Dear All,

I join this thread rather late in the day, so let me back up to Conor's 
suggestion to use add-with-carry.

I cannot resist a free bit of advertising for Ch.5 of Edwin Brady's PhD 
thesis,

http://www.cs.st-andrews.ac.uk/~eb/writings/thesis.pdf

where he treats adc (and other things) for 2^n-wide words as a 
dependently-typed function of n, the so-called (by us) "Every Number Has 
At Most Two Digits" representation.

The Coq people (in particular, Pierre Letouzey) have recently 
re-implemented the idea in their modular treatment of (machine) 
arithmetic, or so I understood from talking to Pierre a while ago.

So each might be a good place to look for inspiration for an Agda 
treatment...

best wishes,

James McKinna

Permjacov Evgeniy wrote:
> On 03/03/2011 02:45 PM, Conor McBride wrote:
>   
>> 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.
>>
>>     
>
> Ok, it is very possible. However, the problem is, that I does not know
> so much about math. I'm neither computer nor math scinentist. So, I wish
> to ask you, what do you mean?
>
> I think, I have to declare reason, why not to use simple church encoding.
>
> The church encoding, i.e. one with
> data Nat : Set0 where
>   zero : Nat
>   succ : Nat -> Nat
>
> is intuitive and effective for reasoning about numbers themself.
> However, the main representation of numbers in computer is one using
> binominal encoding, with fixed or variable length of bit sequence. So,
> to reason about numbers in computing, one need bitwise encoding. And
> this is the only reason to use more complex enconding than Church one.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>