search

lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"
12 stars 0 forks source link

https://lawrencecpaulson.github.io/2024/07/25/Numeric_types.html #46

Open utterances-bot opened 1 month ago

utterances-bot commented 1 month ago

The mysteries and frustrations of numerical proofs

https://lawrencecpaulson.github.io/2024/07/25/Numeric_types.html

fhaftmann commented 1 month ago

A remark on the transition from two complement signed binary numerals (isomorphic to int) to the current unsigned binary numerals (isomorphic to nat): the main drawback of signed numerals is that you need an explicit conversion from int to nat to apply them to natural numbers, making all non-positive values zero. Mechanic tools on nat (provers, code generator) then have to use separate procedures to find out whether a numeral expression is indeed a positive value or just zero. Unsigned binary numerals avoid that while still maintaining the advantages of a radix representation. One drawback of unsigned binary numerals is that rewrite rules for bit operations AND OR XOR NOT become tricky.

lawrencecpaulson commented 3 weeks ago

The point of a two’s complement format over signed-magnitude is to eliminate case analyses on signs. How else can we compute the integer sum i+j without checking whether the operands have the same sign and if not, seeing which has the greater magnitude? With two's complement, you simply add the binary representations and it all works, exactly as in hardware.