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.
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
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
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
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
I (O IHi) applies
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
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
natFold :: a -> (a -> a) -> (a -> a) -> a natFold ihi o i = natFold' ihi where natFold' n = n ? natFold' (o n) ? natFold' (i n)
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)