Module Data.BinInt

This library contains data types for a binary representation of natural and integers. It is based on the paper Declaring Numbers by Brassel/Fischer/Huch ENTCS 216, 2008.

The advantage of this algebraic definition in contrast to built-in integers is the possibility to use them also for narrowing, i.e., functional logic programming. Since the operations are also quite efficient compared to a simple Peano representations, this library is also the basis of the implementation of integers in the Curry implementation KiCS2.

Version: December 2020

Summary of exported operations:

succ :: Nat -> Nat  Deterministic 
Successor, O(n)
pred :: Nat -> Nat  Deterministic 
Predecessor, O(n)
(+^) :: Nat -> Nat -> Nat  Deterministic 
Addition, O(max (m, n))
(-^) :: Nat -> Nat -> BinInt  Deterministic 
Subtraction
mult2 :: BinInt -> BinInt  Deterministic 
Multiplication by 2
(*^) :: Nat -> Nat -> Nat  Deterministic 
Multiplication, O(m*n)
div2 :: Nat -> Nat  Deterministic 
Division by 2
mod2 :: Nat -> BinInt  Deterministic 
Modulo by 2
cmpNat :: Nat -> Nat -> Ordering  Deterministic 
Comparison of natural numbers, O(min (m,n))
quotRemNat :: Nat -> Nat -> (BinInt,BinInt)  Deterministic 
Quotient and remainder.
lteqInteger :: BinInt -> BinInt -> Bool  Deterministic 
Less-than-or-equal on BinInt
cmpInteger :: BinInt -> BinInt -> Ordering  Deterministic 
Comparison on BinInt, O(min (m, n))
neg :: BinInt -> BinInt  Deterministic 
Unary minus.
inc :: BinInt -> BinInt  Deterministic 
Increment
dec :: BinInt -> BinInt  Deterministic 
Decrement
(+#) :: BinInt -> BinInt -> BinInt  Deterministic 
Adds two BinInts.
(-#) :: BinInt -> BinInt -> BinInt  Deterministic 
Subtracts two BinInts.
(*#) :: BinInt -> BinInt -> BinInt  Deterministic 
Multiplies two BinInts.
quotRemInteger :: BinInt -> BinInt -> (BinInt,BinInt)  Deterministic 
Quotient and Remainder, truncated against zero
divModInteger :: BinInt -> BinInt -> (BinInt,BinInt)  Deterministic 
Quotient and Remainder, truncated against negative infinity
divInteger :: BinInt -> BinInt -> BinInt  Deterministic 
Integer divisor, truncated towards negative infinity.
modInteger :: BinInt -> BinInt -> BinInt  Deterministic 
Integer modulo, truncated towards negative infinity.
quotInteger :: BinInt -> BinInt -> BinInt  Deterministic 
Integer quotient, truncated towards zero.
remInteger :: BinInt -> BinInt -> BinInt  Deterministic 
Integer remainder, truncated towards zero.

Exported datatypes:


Nat

Algebraic data type to represent natural numbers.

Constructors:

  • IHi :: Nat : most significant bit
  • O :: Nat -> Nat : multiply with 2
  • I :: Nat -> Nat : multiply with 2 and add 1

BinInt

Algebraic data type to represent integers.

Constructors:

  • Neg :: Nat -> BinInt
  • Zero :: BinInt
  • Pos :: Nat -> BinInt

Exported operations:

succ :: Nat -> Nat  Deterministic 

Successor, O(n)

Further infos:
  • solution complete, i.e., able to compute all solutions

pred :: Nat -> Nat  Deterministic 

Predecessor, O(n)

(+^) :: Nat -> Nat -> Nat  Deterministic 

Addition, O(max (m, n))

Further infos:
  • solution complete, i.e., able to compute all solutions

(-^) :: Nat -> Nat -> BinInt  Deterministic 

Subtraction

mult2 :: BinInt -> BinInt  Deterministic 

Multiplication by 2

Further infos:
  • solution complete, i.e., able to compute all solutions

(*^) :: Nat -> Nat -> Nat  Deterministic 

Multiplication, O(m*n)

Further infos:
  • solution complete, i.e., able to compute all solutions

div2 :: Nat -> Nat  Deterministic 

Division by 2

mod2 :: Nat -> BinInt  Deterministic 

Modulo by 2

Further infos:
  • solution complete, i.e., able to compute all solutions

cmpNat :: Nat -> Nat -> Ordering  Deterministic 

Comparison of natural numbers, O(min (m,n))

quotRemNat :: Nat -> Nat -> (BinInt,BinInt)  Deterministic 

Quotient and remainder.

lteqInteger :: BinInt -> BinInt -> Bool  Deterministic 

Less-than-or-equal on BinInt

cmpInteger :: BinInt -> BinInt -> Ordering  Deterministic 

Comparison on BinInt, O(min (m, n))

neg :: BinInt -> BinInt  Deterministic 

Unary minus. Usually written as "- e".

Further infos:
  • solution complete, i.e., able to compute all solutions

inc :: BinInt -> BinInt  Deterministic 

Increment

dec :: BinInt -> BinInt  Deterministic 

Decrement

(+#) :: BinInt -> BinInt -> BinInt  Deterministic 

Adds two BinInts.

(-#) :: BinInt -> BinInt -> BinInt  Deterministic 

Subtracts two BinInts.

(*#) :: BinInt -> BinInt -> BinInt  Deterministic 

Multiplies two BinInts.

Further infos:
  • solution complete, i.e., able to compute all solutions

quotRemInteger :: BinInt -> BinInt -> (BinInt,BinInt)  Deterministic 

Quotient and Remainder, truncated against zero

divModInteger :: BinInt -> BinInt -> (BinInt,BinInt)  Deterministic 

Quotient and Remainder, truncated against negative infinity

divInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer divisor, truncated towards negative infinity.

modInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer modulo, truncated towards negative infinity.

quotInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer quotient, truncated towards zero.

remInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer remainder, truncated towards zero.