[Agda] termination

[Bas Spitters]

A source for the Coq development is:
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry:
Extending Coq with Imperative Features and its Application to SAT
Verification

http://assert-false.net/arnaud/papers/Extending%20Coq%20with%20Imperative%20Features%20and%20its%20Application%20to%20SAT%20Verification.pdf

Robbert Krebbers and I are currently using these machine integers in
our development of exact reals in Coq.
They are quite nice to work with.

Best,

Bas


On Thu, Mar 3, 2011 at 3:18 PM, James McKinna <james.mckinna at cs.ru.nl> wrote:
> 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
>>
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>