### Table of Contents

# Enumerating the Rationals, logically

This is a view at the Functional Pearl "Enumerating the Rationals" from a (functional) logical point of view.

### Boolean Lists

We start with the implementation of `igcd`

. This function takes a rational number which is represented by a denominator and a numerator and yields a list of booleans. This list represents the decisions that would be made in Euclid's subtractive algorithm for computing greatest common divisor.

igcd :: (Int,Int) -> [Bool] igcd (m,n) = if m<n then False:igcd (m,n-m) else if m>n then True:igcd (m-n,n) else []

There is also a function `ungcd`

which takes a boolean list and yields the corresponding rational number.

ungcd :: [Bool] -> (Nat,Nat) ungcd bs = foldr undo (IHi,IHi) bs where undo False (m,n) = (m,n+^m) undo True (m,n) = (m+^n,n)

We aimed at a numeration of all positive rational numbers. In contrast to Haskell in Curry we use non-determinism to solve this task. We simply apply `ungcd`

to a free variable which non-deterministically yields all possible values (in this case all boolean lists). Because we want to get a similar result as the Haskell program does we use an encapsulation to get a list of all non-deterministic values. This is done by applying `searchTree`

we yields a tree that contains all non-deterministic values. We can traverse this tree by using `allValuesB`

which enumerates the leaf of the tree breadth first.

rat1 :: [(Nat,Nat)] rat1 = allValuesB (searchTree (ungcd unknown))

We can as well implement this function in a Haskell like style. In this case we use lists instead of non-determinism.

unknownBoolList :: [[Bool]] unknownBoolList = [] : [b:bs | bs <- unknownBoolList, b <- [False,True]] rat1h :: [(Nat,Nat)] rat1h = map ungcd unknownBoolList

### Natural Numbers

Curry provides a data type for representing natural numbers.

data Nat = IHi | O Nat | I Nat

This data type is isomorphic to `[Bool]`

. Therefore we can define functions `igcdNat`

and `ungcdNat`

which represent the bijective mapping between natural numbers and positive rational numbers. Instead of `foldr`

we use a fold on the `Nat`

data type in `ungcdNat`

.

igcdNat :: (Int,Int) -> Nat igcdNat (m,n) = if m<n then O (igcdNat (m,n-m)) else if m>n then I (igcdNat (m-n,n)) else IHi foldNat :: (a -> a) -> (a -> a) -> a -> Nat -> a foldNat o i ihi = foldNat' where foldNat' IHi = ihi foldNat' (O n) = o (foldNat' n) foldNat' (I n) = i (foldNat' n) ungcdNat :: Nat -> (Nat,Nat) ungcdNat = foldNat undoO undoI (IHi,IHi) where undoO (m,n) = (m,n+^m) undoI (m,n) = (m+^n,n)

We can again enumerate the positive rationals by using a free variable and an encapsulation. This time the variable yields all natural numbers.

rat2 :: [(Nat,Nat)] rat2 = allValuesB (searchTree (ungcdNat unknown))

It would be interesting whether operations on `Nat`

do have a meaning on rationals.

### Signed Integers

It is very easy to extend this to negative rational numbers and zero simply be exchanging `Nat`

by `Int`

which is defined as follows.

data Int = Zero | Neg Nat | Pos Nat foldInt :: (b -> a) -> (b -> a) -> a -> (Nat -> b) -> Int -> a foldInt neg pos zero fromNat = foldInt' where foldInt' Zero = zero foldInt' (Neg n) = neg (fromNat n) foldInt' (Pos n) = pos (fromNat n) ungcdInt :: Int -> (Int,Nat) ungcdInt = foldInt undoNeg undoPos (0,IHi) ungcdNat where undoNeg (m,n) = (Neg m,n) undoPos (m,n) = (Pos m,n) igcdInt :: (Int,Int) -> Int igcdInt (Zero,_) = Zero igcdInt (m@(Neg _),n) = Neg (igcdNat (m,n)) igcdInt (m@(Pos _),n) = Pos (igcdNat (m,n))

### Efficiency

All the presented enumerations are inefficient in the sense that applications to the same argument are computed more often than necessary. For example if you apply `ungcdNat`

to all natural numbers it is applied to `O IHi`

and `I (O IHi)`

among other things. The application of `ungcdNat`

to `I (O IHi)`

applies `ungcdNat`

to `O IHi`

in its recursive call. To prevent this we us an accumulator. First of all we define a function `natUnknown`

that yields all natural numbers but do not use the constructors of `Nat`

but functions that are passed. For example `natUnknown IHi O I`

is a free variable of Type `Nat`

.

natUnknown :: a -> (a -> a) -> (a -> a) -> a natUnknown ihi o i = ihi ? o (natUnknown ihi o i) ? i (natUnknown ihi o i)

Now we define a similar function that uses an accumulator to prevent unnecessary computations. In fact we merge `ungcdNat`

with `unknown`

.

natFold :: a -> (a -> a) -> (a -> a) -> a natFold ihi o i = natFold' ihi where natFold' n = n ? natFold' (o n) ? natFold' (i n)

By using `natFold`

we can define an enumeration that is more efficient.

rat3 :: [(Nat,Nat)] rat3 = allValuesB (searchTree (natFold (IHi,IHi) undoO undoI)) where undoO (m,n) = (m,n+^m) undoI (m,n) = (m+^n,n)

If we enumerate 100.000 rationals it takes 17 seconds with `rat2`

and 4 seconds with `rat3`

. Sadly the separation between the enumeration and the processing is lost here.

There is also a Haskell like version of `rat3`

. Like before we implement a function that enumerates all natural numbers but replaces the constructors by function applications that is we merge the enumeration with the fold.

natsListFold :: a -> (a -> a) -> (a -> a) -> [a] natsListFold ihi o i = natsListFold' ihi where natsListFold' n = n : merge (natsListFold' (o n)) (natsListFold' (i n)) merge (x:xs) ys = x:merge ys xs rat3h :: [(Nat,Nat)] rat3h = natsListFold (IHi,IHi) undoO undoI where undoO (m,n) = (m,n+^m) undoI (m,n) = (m+^n,n)