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)