Enumerating the Rationals, logically

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

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

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.

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

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)

Jan Christiansen