The author defines an axiom system for rounded arithmetic to be complete iff from any model of the axioms we can recover the exact algebra from whence it came. There are some earlier attempts to axiomatize the algebra of computer arithmetic, but none of them considers the problem of giving a complete axiomatization (in the above sense). The author gradually introduces 45 axioms, culminating with a proof of the following Theorem: If $$ satisfies axioms 1- 45, then there is an ordered field F extending S and a rounding function O mapping F onto S satisfying the conditions: $O(O(x))=O(x)$, $x\le y$ implies O(x)$\le O(y)$, $O(0)=0$, $O(1)=1$ and $O(-x)=-O(x).$ The proof of the above theorem occupies nearly 10 printed pages and as main steps in the proof we mention a (weak) normal form theorem for some reduction system and the ordered group and ordered integral domain case of the main theorem.
Reviewer: Ş.Buzeţeanu