4.12.07
Arithmetic for lists
Here are analogues of sum, product, and exponentiation for lists. Each takes two lists of values, of types a and b, and forms the list of all values of sum, product, and function (exponent) types.
The first two of these are already built-in to Haskell, in the form of append and list-comprehensions. The third is also quite useful, and I suggest it should be added to the standard List module. For example, if you want to form a truth table for the list of variables in names, your can do so using [True,False]^^^names to form all 2^n mappings of names to truth variables (where n is the length of names).
In case you doubt whether these actually correspond to sum, product, and exponentiation, here are Peano's definitions:
And here are the above operations, rewritten to correspond to Peano's definitions:
type Sum a b = Either a b
type Prod a b = (a,b)
type Exp a b = [(b,a)] -- represents functions from b to a
(+++) :: [a] -> [b] -> [Sum a b]
xs +++ ys = map Left xs ++ map Right ys
(***) :: [a] -> [b] -> [Prod a b]
xs *** ys = [ (x,y) | x <- xs, y <- ys ]
(^^^) :: [a] -> [b] -> [Exp a b]
xs ^^^ [] = [ [] ]
xs ^^^ (y:ys) = [ (y,x):e | x <- xs, e <- xs^^^ys ]
The first two of these are already built-in to Haskell, in the form of append and list-comprehensions. The third is also quite useful, and I suggest it should be added to the standard List module. For example, if you want to form a truth table for the list of variables in names, your can do so using [True,False]^^^names to form all 2^n mappings of names to truth variables (where n is the length of names).
In case you doubt whether these actually correspond to sum, product, and exponentiation, here are Peano's definitions:
m+0 = m
m+(n+1) = (m+n)+1
m*0 = 0
m*(n+1) = (m*n)+m
m^0 = 1
m^(n+1) = (m^n)*m
And here are the above operations, rewritten to correspond to Peano's definitions:
(+++) :: [a] -> [b] -> [Sum a b]
[] +++ ys = map Right ys
(x:xs) +++ ys = Left x : (xs +++ ys)
(***) :: [a] -> [b] -> [Prod a b]
[] *** ys = []
(x:xs) *** ys = map f (ys +++ (xs *** ys))
where
f (Left y) = (x,y)
f (Right p) = p
(^^^) :: [a] -> [b] -> [Exp a b]
xs ^^^ [] = [ [] ]
xs ^^^ (y:ys) = map g (xs *** (xs ^^^ ys))
where
g (x,e) = (y,x):e
Subscribe to:
Post Comments (Atom)
7 comments:
Looks more like the definitions for cardinal arithmetic.
Neat! Minor quibble: I think you mean [True,False]^^^names instead of the other way around?
In the following equation:
xs ^^^ (y:ys) = [ (y,x):e | x <- xs, e <- xs^^^ys ], I think you're missing an x on the left hand side. (And likewise in its dual later on)
Thanks to Brent Yorgey for the correction (I edited my post to incorporate the fix).
Adam, the equation is fine as given. Variable x is bound by the generator, x <- xs.
It'd be interesting to make these work for infinite lists too. For products you need some kind of "diagonal trick" but I haven't yet thought about what's required for the exponentiation function.
We can't diagonalise ^^^.
Here's the proof. Exp a b represents a function b -> a, so let's implement this function:
> import Data.List (find)
> inport Data.Maybe (fromJust)
>
> lookup :: Exp a b -> b -> a
> lookup func b = snd $ fromJust $ find (\(b', _) -> b == b') func
funcs represents functions of type Integer -> Bool.
> funcs :: [Exp Bool Integer]
> funcs = [True, False]^^^[0...]
Now generate another instance of Exp Bool Integer from funcs as follows:
> awkward :: Exp Bool Integer
> awkward = map (\i -> (i, not $ lookup (funcs ! i) i)) [0..]
It's easy to see that:
lookup awkward 0 != lookup (funcs ! 0) 0
lookup awkward 1 != lookup (funcs ! 1) 1
lookup awkward 2 != lookup (funcs ! 2) 2
etc.
so awkward does not match amy element of funcs, so funcs cannot be a diagonalisation.
I'm actually surprised list exponentiation isn't already in there, it's quite natural from the automata/language theory side of the universe: a^^^b is just the language with alphabet a and all strings of length (length b)-- only paired with the values of b for mnemonic purposes.
Post a Comment