Anubis / Anubis

Commit 4038927f79469363e7f05e17e7eb42c6d6307412

Authored by Alain Prouté
1 parent fcdefa65

Added a library file for handling big relative integers.

Showing 2 changed files with 366 additions and 6 deletions   Show diff stats
Inline Side-by-side
anubis_dev/library/numbers/integers1.anubis 0 → 100644
  Show/Hide comments   View file @4038927
  1 +
  2 +
  3 + The Anubis Project
  4 +
  5 +
  6 + The type 'Int' of big relative integers and related tools.
  7 +
  8 +
  9 + Author: Alain Proute'
  10 +
  11 +
  12 +
  13 + The type of big relative integers.
  14 +
  15 +public type Int:
  16 + positive(Nat abs),
  17 + negative(Nat abs).
  18 +
  19 +
  20 + Because 'positive(0)' and 'negative(0)' must be the same number, we introduce a
  21 + 'normalization' function:
  22 +
  23 +public define Int normalize(Int x).
  24 +
  25 + which returns 'x', except if 'x' is 'negative(0)', in which case it returns
  26 + 'positive(0)'.
  27 +
  28 + All the operations below return normalized integers. If you define new operations
  29 + returning integers, it is better that they return always normalized integers.
  30 +
  31 +
  32 + You may construct relative integers from natural integers. Just add a '+' or '-' sign
  33 + in front of the natural.
  34 +
  35 +public define Int + Nat n.
  36 +public define Int - Nat n.
  37 +
  38 +
  39 +
  40 + A relative integer has an opposite and an absolute value. The absolute value may be
  41 + interpreted either as a relative integers or as a natural integer.
  42 +
  43 +public define Int - Int x.
  44 +public define Int abs(Int x).
  45 +
  46 + abs(Int x) as a 'Nat' is already defined as an implicit destructor in the definition of
  47 + type 'Int'.
  48 +
  49 +
  50 + Comparisons.
  51 +
  52 +public define Bool Int x < Int y.
  53 +public define Bool Int x =< Int y.
  54 +
  55 +
  56 + Arithmetic operations on relative integers.
  57 +
  58 +public define Int Int x + Int y. Addition.
  59 +public define Int Int x - Int y. Substraction.
  60 +public define Int Int x * Int y. Multiplication.
  61 +public define Maybe((Int,Int)) Int x / Int y. Euclidian division.
  62 +
  63 + Of course, division by '0' is meaningless, hence the 'Maybe'. The pair of integers
  64 + returned by the euclidian division is (quotient,remainder) in this order. The remainder
  65 + is always positive, even if the dividend 'x' is negative. The remainder is always
  66 + strictly smaller than the absolute value of the divisor 'y'. In other words, if the
  67 + result is '(q,r)', we have:
  68 +
  69 + x = q*y + r
  70 + 0 =< r < |y|
  71 +
  72 +
  73 +public define (Int,Int,Int) bezout(Int x, Int y). gcd and Bezout coefficients.
  74 +
  75 + This function returns a triplet '(d,u,v)', where 'd' is the gcd (greatest common
  76 + divisor) of 'x' and 'y', 'u' and 'v' a pair of Bezout coefficients. In other words, it
  77 + gives the gcd as a linear combinaison of 'x' and 'y':
  78 +
  79 + d = u*x + v*y
  80 +
  81 + According to the interpretation of this formula in terms of ideals in a principal ring,
  82 + we have:
  83 +
  84 + bezout(0,0) = (0,1,1)
  85 + bezout(x,0) = (x,1,1) if x /= 0
  86 + bezout(0,y) = (y,1,1) if y /= 0
  87 +
  88 +
  89 + We also have:
  90 +
  91 +public define Int gcd(Int x, Int y). The gcd alone.
  92 +public define Int lcm(Int x, Int y). The lcm (least common multiple).
  93 +
  94 + Again, we have:
  95 +
  96 + gcd(0,0) = 0
  97 + gcd(x,0) = x if x /= 0
  98 + gcd(0,y) = y if y /= 0
  99 +
  100 + lcm(0,0) = 0
  101 + lcm(x,0) = 0 if x /= 0
  102 + lcm(0,y) = 0 if y /= 0
  103 +
  104 + Notice that the divisibility relation 'x divides y' turns 'Int' into a preordered set,
  105 + hence into a category. In this category, '0' is the final object, and an object is
  106 + initial if and only if it is an invertible element (in the case of Int, the invertibles
  107 + are '+1' and '-1'). The gcd is the infimum (the categorical product) with respect to
  108 + the divisibility relation and the lcm is the supremum (the categorical sum) with
  109 + respect to the divisibility relation. The above special cases are coherent with this
  110 + interpretation.
  111 +
  112 +
  113 +
  114 + --- That's all for the public part ! --------------------------------------------------
  115 +
  116 +
  117 +define Int normalize(Int x) =
  118 + if x is
  119 + {
  120 + positive(n) then x,
  121 + negative(n) then
  122 + if n = 0
  123 + then positive(0)
  124 + else x
  125 + }.
  126 +
  127 +
  128 +public define Int + Nat n = positive(n).
  129 +public define Int - Nat n = if n = 0 then positive(0) else negative(n).
  130 +
  131 +
  132 +public define Int
  133 + - Int x
  134 + =
  135 + if x is
  136 + {
  137 + positive(n) then if n = 0 then positive(0) else negative(n),
  138 + negative(n) then positive(n)
  139 + }.
  140 +
  141 +
  142 +public define Int
  143 + abs
  144 + (
  145 + Int x
  146 + ) =
  147 + if x is
  148 + {
  149 + positive(n) then x,
  150 + negative(n) then positive(n)
  151 + }.
  152 +
  153 +
  154 +public define Bool
  155 + Int x < Int y
  156 + =
  157 + if x is
  158 + {
  159 + positive(n) then if y is
  160 + {
  161 + positive(m) then n < m,
  162 + negative(m) then false
  163 + },
  164 + negative(n) then if y is
  165 + {
  166 + positive(m) then if n = 0
  167 + then if m = 0
  168 + then false
  169 + else true
  170 + else true
  171 + negative(m) then m < n
  172 + }
  173 + }.
  174 +
  175 +
  176 +public define Bool
  177 + Int x =< Int y
  178 + =
  179 + if x is
  180 + {
  181 + positive(n) then if y is
  182 + {
  183 + positive(m) then n =< m,
  184 + negative(m) then if n = 0
  185 + then if m = 0
  186 + then true // 0 =< 0
  187 + else false // x = 0 and y < 0
  188 + else false // x > 0 and y =< 0
  189 + },
  190 + negative(n) then if y is
  191 + {
  192 + positive(m) then true
  193 + negative(m) then m =< n
  194 + }
  195 + }.
  196 +
  197 +
  198 +
  199 +
  200 +
  201 +public define Int
  202 + Int x + Int y
  203 + =
  204 + if x is
  205 + {
  206 + positive(n) then if y is
  207 + {
  208 + positive(m) then positive(n+m),
  209 + negative(m) then if n >= m
  210 + then positive(n |-| m)
  211 + else negative(m |-| n)
  212 + },
  213 + negative(n) then if y is
  214 + {
  215 + positive(m) then if n > m
  216 + then negative(n |-| m)
  217 + else positive(m |-| n),
  218 + negative(m) then negative(n+m)
  219 + }
  220 + }.
  221 +
  222 +
  223 +
  224 +public define Int
  225 + Int x - Int y
  226 + =
  227 + x + -y.
  228 +
  229 +
  230 +
  231 +public define Int
  232 + Int x * Int y
  233 + =
  234 + if x is
  235 + {
  236 + positive(n) then if y is
  237 + {
  238 + positive(m) then positive(n*m),
  239 + negative(m) then normalize(negative(n*m))
  240 + },
  241 + negative(n) then if y is
  242 + {
  243 + positive(m) then normalize(negative(n*m)),
  244 + negative(m) then positive(n*m)
  245 + }
  246 + }.
  247 +
  248 +
  249 +
  250 +
  251 + The euclidian division for type 'Int'.
  252 +
  253 +public define Maybe((Int,Int))
  254 + Int x / Int y
  255 + =
  256 + if ((:Nat)abs(x)) / ((:Nat)abs(y)) is
  257 + {
  258 + failure then failure,
  259 + success(p) then if p is (Nat q, Nat r) then
  260 + if x is
  261 + {
  262 + positive(n) then if y is
  263 + {
  264 + positive(m) then
  265 + success((positive(q),positive(r))),
  266 +
  267 + negative(m) then // x = q*(-y) + r = (-q)*y + r
  268 + success((normalize(negative(q)),positive(r)))
  269 + },
  270 + negative(n) then if y is
  271 + {
  272 + positive(m) then if r = 0
  273 + then // -x = q*y hence x = (-q)*y + 0
  274 + success((normalize(negative(q)),positive(0)))
  275 + else // -x = q*y + r hence x = (-q)*y - r = (-q-1)*y + (y-r) and 0 =< y-r < |y|
  276 + success((negative(q+1),positive(m |-| r))),
  277 +
  278 + negative(m) then if r = 0
  279 + then // -x = q*(-y) hence x = q*y + 0
  280 + success((positive(q),positive(0)))
  281 + else // -x = q*(-y) + r hence x = q*y - r = (q+1)*y + (-y-r) and 0 =< -y-r < |y|
  282 + success((positive(q+1),positive(m |-| r)))
  283 + }
  284 + }
  285 + }.
  286 +
  287 +
  288 +
  289 +
  290 +
  291 + gcd and Bezout coefficients for type 'Int'.
  292 +
  293 +public define (Int,Int,Int)
  294 + bezout
  295 + (
  296 + Int x,
  297 + Int y
  298 + ) =
  299 + if abs(x) < (:Nat)abs(y)
  300 + then (if bezout(y,x) is (d,u,v) then (d,v,u))
  301 + else
  302 + //
  303 + // Apply Euclid's algorithm.
  304 + //
  305 + if x/y is
  306 + {
  307 + failure then // 'y' is zero: finished
  308 + (x,+1,+1),
  309 +
  310 + success(p) then if p is (q,r) then
  311 + //
  312 + // We have:
  313 + // x =q*y + r and 0 =< r < |y|
  314 + //
  315 + if bezout(y,r) is (d,a,b) then
  316 + //
  317 + // we have the gcd, and:
  318 + //
  319 + // d = a*y + b*r
  320 + // = a*y + b*(x - q*y)
  321 + // = b*x + (a - b*q)*y
  322 + //
  323 + (d,b,a - b*q)
  324 + }.
  325 +
  326 +
  327 + gcd and lcm.
  328 +
  329 +public define Int
  330 + gcd
  331 + (
  332 + Int x,
  333 + Int y
  334 + ) =
  335 + if bezout(x,y) is (d,_,_) then d.
  336 +
  337 +
  338 +public define Int
  339 + lcm
  340 + (
  341 + Int x,
  342 + Int y
  343 + ) =
  344 + if bezout(x,y) is (d,_,_) then
  345 + if x/d is
  346 + {
  347 + failure then // 'x' and 'y' are zero
  348 + +0,
  349 +
  350 + success(p) then if p is (q,r) then // actually r is zero
  351 + q*y
  352 + }.
  353 +
  354 +
  355 +
  356 +
  357 +
0 358 \ No newline at end of file
... ...
anubis_dev/library/predefined.anubis
  Show/Hide comments   View file @4038927
... ... @@ -2826,14 +2826,17 @@ public define ByteArray sha1($T d) = £sha1(serialize(d)).
2826 2826 usual ones (as available for example under UNIX) when 'd' is a byte array. When 'd' is
2827 2827 not a byte array, 'd' is first serialized before the usual algorithm is applied to it.
2828 2828  
2829   - Note: at the time of writting, only sha1 is implemented for both Linux and Windows.
2830   -
2831   -
2832   -
2833   -
  2829 + So, be carefull with strings. If you use one of these functions on a character string,
  2830 + it will not give the standard result. In order to get the standard result, convert your
  2831 + string into a byte array first, like this:
  2832 +
  2833 + sha1(to_byte_array("...."))
  2834 +
  2835 +
  2836 +
  2837 +
2834 2838  
2835 2839  
2836   -
2837 2840 *** (9.2) Symmetric cryptography ('blowfish_encrypt', 'blowfish_decrypt').
2838 2841  
2839 2842 The 'Blowfish' algorithm is a block cipher designed by Bruce Schneier (see his book:
... ...