# 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)``` 