From c59a8c4a2a787b9adda47caca9e0ddf1429e7b5c Mon Sep 17 00:00:00 2001
From: Michael Hemmer <hemmer@mpi-inf.mpg.de>
Date: Fri, 2 Feb 2007 12:00:14 +0000
Subject: [PATCH] fixed rounding mode of div to TOWARDS_ZERO, which is
 compliant to most implementations of integers.

---
 .../AlgebraicStructureTraits_DivMod.tex       | 66 ++++++++++++++++++-
 1 file changed, 64 insertions(+), 2 deletions(-)

diff --git a/Algebraic_foundations/doc_tex/Algebraic_foundations_ref/AlgebraicStructureTraits_DivMod.tex b/Algebraic_foundations/doc_tex/Algebraic_foundations_ref/AlgebraicStructureTraits_DivMod.tex
index 8f46f0a2192..a54d66cd762 100644
--- a/Algebraic_foundations/doc_tex/Algebraic_foundations_ref/AlgebraicStructureTraits_DivMod.tex
+++ b/Algebraic_foundations/doc_tex/Algebraic_foundations_ref/AlgebraicStructureTraits_DivMod.tex
@@ -3,8 +3,70 @@
 \ccDefinition
 
 \ccc{AdaptableFunctor} computes both integral quotient and remainder
-of division with remainder. 
- 
+of division with remainder. The quotient $q$ and remainder $r$ are computed 
+such that $x = q*y + r$ and $|r| < |y|$ with respect to the proper integer norm.
+\footnote{
+For integers this norm is the absolute value.\\ 
+For univariate polynomials this norm is the degree.} 
+In particular, $r$ is chosen to be $0$ if possible.
+For \ccc{RealEmbeddable} \ccc{EuclideanRing}s we require $q$ to be computed 
+as $x/y$ rounded towards zero. 
+
+Note that the last condition is needed to ensure a unique computation of the 
+pair $(q,r)$. However, an other option is to require minimality for $|r|$, 
+with the advantage that
+a {\em mod(x,y)} operation would return the unique representative of the 
+residue class of $x$ with respect to $y$, e.g. $mod(2,3)$ should return $-1$. 
+But this conflicts with nearly all current implementation 
+of integer types. From there, we decided to stay conform with common 
+implementations and require $q$ to be computed as $x/y$ rounded towards zero, 
+for \ccc{RealEmbeddable} \ccc{EuclideanRing}s. 
+
+\ignore{
+Note that in general the above definition does not force a unique computation 
+of the pair $(q,r)$. This could be solved by requiring $|r|$ to be minimal, 
+in particular a {\em mod} operation would return the unique representative of 
+its residue class. But this conflicts with nearly all current implementation 
+of integer types. From there, we decided to stay conform with common 
+implementation and require $q$ to be computed as $x/y$ rounded towards zero, 
+for \ccc{RealEmbeddable} \ccc{EuclideanRing}s. 
+}
+
+The following truth table illustrates the behavior for integers: 
+
+\begin{tabular}{ccc}
+\begin{tabular}{|c|c|c|c|}
+\hline
+ $\ x\ $ & $\ y\ $ & $\ q\ $ & $\ r\ $\\
+\hline
+ 3  &  3  &  1  &  0\\
+ 2  &  3  &  0  &  2\\
+ 1  &  3  &  0  &  1\\
+ 0  &  3  &  0  &  0\\
+-1  &  3  &  0  & -1\\
+-2  &  3  &  0  & -2\\
+-3  &  3  & -1  &  0\\
+\hline
+\end{tabular}
+& - & 
+\begin{tabular}{|c|c|c|c|}
+\hline
+ $\ x\ $ & $\ y\ $ & $\ q\ $ & $\ r\ $\\
+\hline
+ 3  & -3  & -1  &  0\\
+ 2  & -3  &  0  &  2\\
+ 1  & -3  &  0  &  1\\
+ 0  & -3  &  0  &  0\\
+-1  & -3  &  0  & -1\\
+-2  & -3  &  0  & -2\\
+-3  & -3  &  1  &  0\\
+\hline
+\end{tabular}\\
+\end{tabular}
+
+
+
+
 \ccRefines 
 
 \ccc{AdaptableFunctor}