A program inspired by
What Sequential Games, the Tychonoff Theorem
and the Double-Negation Shift have in Common
by Martin Escardo and Paulo Oliva
Philip Wadler, 30 Aug 2010 (revised 31 Aug 2010)
A recent paper by Escardo and Oliva [1], to appear in MSFP 2010,
relates diverse aspects of computing, in the form of a literate
Haskell program. This note is inspired by theirs, and is also a
literate Haskell program. It improves on theirs in a few ways,
notably by using type classes to characterize valuation types, and by
using QuickCheck to describe and check relevant properties. This
note can be read stand-alone, but is best read in conjunction with
Escardo and Oliva's paper.
The starting point is finding optimal elements of sets. Let (J a)
represent a non-empty collection of values of type a. Let r be a
valuation type equipped with binary operation `sup` which selects the
larger of its two arguments.
class Sup r where
sup :: r -> r -> r
Using Haskell type classes, we write Sup r to indicate that type r
must support a binary operation `sup`. Escardo and Oliva restrict
attention to a few specific instances of r; an advantage of the
development here is that we use type classes to generalize to any r
with a suitable supremum operator.
Presume we are given a valuation function k :: a -> r which takes
elements of the set into valuations. We are interested in an
operation optimum, which picks the element with the largest valuation.
optimum :: Sup r => J a -> (a -> r) -> a
We require the collection to be non-empty so that there is always such
an element.
Given optimum, it is easy to define an operation supremum that finds
the largest valuation of any element in the set.
supremum :: Sup r => J a -> (a -> r) -> r
supremum x k = k (optimum x k)
The definition of supremum may seem roundabout: first compute the
element which under the evaluation function returns a dominant value,
and then apply the evaluation function. But this roundabout approach
is the key to ensuring that supremum is defined even on infinite sets.
Escardo and Oliva take this simple idea in a number of directions. If
r is Bool and `sup` is disjunction, then k is a predicate (a map from
elements to booleans), and supremum corresponds to the existential
quantifier (it returns true when there is an element in the set that
satisfies the predicate). Further, optimum corresponds to Hilbert's
epsilon operator, which selects an element of a set satisfying the
predicate if one exists, and returns an arbitrary element otherwise.
They observe it is possible to represent sets by choosing (J a)
to correspond to the type of the supremum operation.
newtype J a = J (forall r. Sup r => (a->r)->a)
Escardo and Oliva use a formalism that ties a set to a specific
valuation type r, defining J r a = (a->r)->a; an advantage of the
development here is that we define sets that work with any suitable
valuation type.
They observe that J has the structure of a monad, and hence that the
standard sequence operator over monads can then be used to convert a
value of type [J a] to a value of type J [a], that is, to convert a
list of sets to a set of lists. They further observe that,
remarkably, this construct works even when the list is an infinite
stream.
In particular, one can construct a set that represents all possible
infinite sequences of booleans (also known as the Cantor Set), and
find an optimum over this infinite set in finite time. Recall how
supremum was defined by applying the evaluator to the optimum. Over
cantor sets optimum will converge (but not arrive) on an optimum
infinite stream; but the evaluator k will only look at a finite number
of elements of the infinite stream, and so can yield a value. They
observe that this construct corresponds to the computational content
of Tychonoff's theorem in topology. As an application, they define
computable equality for certain classes of functionals.
They also define the related type
newtype K a = K (forall r. Sup r => (a->r)->r)
which is derived from J by by replacing the final a with an r. They
observe this also corresponds to a monad, known as the continuation
monad. It is well-known that viewed through the lens of
propositions-as-types that K corresponds to the double-negation
translation in logic. They further observe that viewed through this
same lens, the type J a is related to Peirce's law.
Preliminaries
~~~~~~~~~~~~~
Our program uses some extensions over Haskell. We use rank 2 types
in order to permit quantifying over r in the definitions of J and K.
We also use multi-parameter type classes to classify functions that
are representable by elements of the Cantor Set, and we import a few
standard library functions and the QuickCheck library.
> {-# LANGUAGE Rank2Types, MultiParamTypeClasses #-}
> import Monad(join)
> import Test.QuickCheck
> import Text.Show.Functions
Conventions
~~~~~~~~~~~
Let a, b range over arbitrary types, and values of such types. Let x,
y range over sets (or more generally monads), and phi range over sets
of sets (or more generally a monad of monads). Let r,s range over
types that support a sup operator, and values of such types.
Outcomes
~~~~~~~~
An outcome of a game may be to lose, win, or draw.
> data Outcome = Lose | Draw | Win deriving (Eq,Ord,Enum,Bounded,Show)
In what follows, running examples use Booleans, integers,
and outcomes.
Sup
~~~
We require a binary operator `sup` that finds the supremum of two
elements.
> class Eq r => Sup r where
> sup :: r -> r -> r
> instance Sup Bool where
> r `sup` s = r || s
> instance Sup Int where
> r `sup` s = r `max` s
> instance Sup Outcome where
> Win `sup` r = Win
> Draw `sup` r = Draw `max` r
> Lose `sup` r = r
Operator `sup` differs from `max` in that it is lazy in its
second argument where possible.
*Main> True `sup` undefined
True
*Main> True `max` undefined
*** Exception: Prelude.undefined
*Main> Win `sup` undefined
Win
*Main> Win `max` undefined
*** Exception: Prelude.undefined
However, `sup` is equivalent to `max` for all defined values.
> prop_max :: (Sup r, Ord r) => r -> r -> Bool
> prop_max r s = (r `sup` s) == (r `max` s)
> check_max =
> quickCheck (prop_max :: Bool -> Bool -> Bool) >>
> quickCheck (prop_max :: Int -> Int -> Bool) >>
> quickCheck (prop_max :: Outcome -> Outcome -> Bool)
We intend to select an optimum element from a set---an element whose
image under a given evaluation function is the supremum. Therefore,
one property we require of `sup` is that it returns one of its
arguments.
> prop_atomic :: Sup r => r -> r -> Bool
> prop_atomic r s = (r `sup` s == r) || (r `sup` s == s)
> check_atomic =
> quickCheck (prop_atomic :: Bool -> Bool -> Bool) >>
> quickCheck (prop_atomic :: Int -> Int -> Bool) >>
> quickCheck (prop_atomic :: Outcome -> Outcome -> Bool)
Observe that we do not have the following instance
instance (Sup r, Sup s) => Sup (r,s) where
(r,s) `sup` (t,u) = (r `sup` t, s `sup` u)
since it violates the above property. For instance, (1,2) `sup` (4,3)
is (2,4) which equals neither (1,2) nor (4,3). In particular, this
means that not every Boolean algebra belongs to Sup. It would be
interesting to classify algebraically the properties Sup must satisfy.
Partial order
~~~~~~~~~~~~~
From the `sup` operator we infer a partial order.
> dominates :: Sup r => r -> r -> Bool
> r `dominates` s = r == (r `sup` s)
Operator `dominates` differs from (>=) in that it is lazy in its
second argument where possible.
*Main> True `dominates` undefined
True
*Main> True >= undefined
*** Exception: Prelude.undefined
*Main> Win `dominates` undefined
True
*Main> Win >= undefined
*** Exception: Prelude.undefined
However, `dominates` is equivalent to (>=) for all defined values.
> prop_geq :: (Sup r, Ord r) => r -> r -> Bool
> prop_geq r s = (r `dominates` s) == (r >= s)
> check_geq =
> quickCheck (prop_geq :: Bool -> Bool -> Bool) >>
> quickCheck (prop_geq :: Int -> Int -> Bool) >>
> quickCheck (prop_geq :: Outcome -> Outcome -> Bool)
Negation
~~~~~~~~
Sometimes we want to compute the smallest value rather than the
largest. We do so using an involutive negation operator and
deMorgan duality.
> class Sup r => Neg r where
> neg :: r -> r
> instance Neg Bool where
> neg = not
> instance Neg Int where
> neg r = -r
> instance Neg Outcome where
> neg Win = Lose
> neg Draw = Draw
> neg Lose = Win
Negation is an involution.
> prop_involution :: Neg r => r -> Bool
> prop_involution r = neg (neg r) == r
> check_involution =
> quickCheck (prop_involution :: Bool -> Bool) >>
> quickCheck (prop_involution :: Int -> Bool) >>
> quickCheck (prop_involution :: Outcome -> Bool)
We define duality for binary operators.
> dual :: Neg r => (r -> r -> r) -> (r -> r -> r)
> dual op r s = neg (neg r `op` neg s)
The infimum is the dual of the supremum.
> inf :: Neg r => r -> r -> r
> inf = dual sup
DeMorgan's law is the special case of this where r is Bool, `sup` is
disjunction, `inf` is conjunction, and neg is complement.
> prop_conjunction :: Bool -> Bool -> Bool
> prop_conjunction r s = (r `inf` s) == (r && s)
> check_conjunction = quickCheck prop_conjunction
Just as `sup` is equivalent to `max` for defined values,
so is `inf` equivalent to `min`.
> prop_min :: (Neg r, Ord r) => r -> r -> Bool
> prop_min r s = (r `inf` s) == (r `min` s)
> check_min =
> quickCheck (prop_min :: Bool -> Bool -> Bool) >>
> quickCheck (prop_min :: Int -> Int -> Bool) >>
> quickCheck (prop_min :: Outcome -> Outcome -> Bool)
Negation is not necessarily a complement in the sense of Boolean
algebra. A complement should satisfy the property that
(a `sup` neg a) dominates every other value. This is satisfied
by Bool, but not by Int or Outcome. Again, it would be interesting to
classify algebraically the properties Neg must satisfy.
Optimum monad
~~~~~~~~~~~~~
Above, we motivated the definition of a type (J a), which can be
used to represent non-empty sets with elements of type a.
> newtype J a = J { unJ :: forall r. Sup r => (a -> r) -> a }
We require that a `sup` operation be available on the valuation
type r. It turns out that this is not required for the monad
structure, but it is required for the `union` operation that we
define below.
> instance Monad J where
> return a = J (\k -> a)
> x >>= f = J (\k -> unJ (f (unJ x (\a -> k (unJ (f a) k)))) k)
Escardo and Oliva define (>>=) in terms of fmap and join, called
functorJ and muJ. We can compute their definitions from ours; their
definition refers to the function 'overline' defined below. As
required, we have
fmap f
=
x >>= (return . f)
=
J (\k -> unJ (return (f (unJ x (\a -> k (unJ (return (f a)) k)))) k)
=
J (\k -> f (unJ x (\a -> k (f a))))
=
J (\k -> f (unJ x (k . f)))
and
join phi
=
phi >>= id
=
J (\k -> unJ (id (unJ phi (\x -> k (unJ (id x) k)))) k)
=
J (\k -> unJ (unJ phi (\x -> k (unJ x k))) k)
=
J (\k -> unJ (unJ phi (\x -> unK (overline x) k)) k)
Supremum monad
~~~~~~~~~~~~~~
We also motivated the definition of a type (K a), which
is identical to the continuation monad, save that again we
restrict attention to valuation types with a `sup` operation.
> newtype K a = K { unK :: forall r. Sup r => (a -> r) -> r }
This has a well-known monadic structure.
> instance Monad K where
> return a = K (\k -> k a)
> x >>= f = K (\k -> unK x (\a -> unK (f a) k))
Again, Escardo and Oliva define (>>=) using fmap and join, called
functorJ and muJ. We can compute their definitions from ours.
fmap f x
=
x >>= (return . f)
=
K (\k -> unK x (\a -> unK (return (f a)) k))
=
K (\k -> unK x (\a -> k (f a)))
=
K (\k -> unK x (k . f))
and
join phi
=
phi >>= id
=
K (\k -> unK phi (\x -> unK (id x) k))
=
K (\k -> unK phi (\x -> unK x k))
Monad morphism
~~~~~~~~~~~~~~
There is a monad morphism between the two monads.
> overline :: J a -> K a
> overline x = K (\k -> k (unJ x k))
Sets
~~~~
We extend the optimum monad with union, giving it a set structure. It
is in order to define union that we require Sup r in the definition of
J and K.
> union :: J a -> J a -> J a
> x `union` y = J (\k -> let a = unJ x k in
> let b = unJ y k in
> if k a `dominates` k b then a else b)
Singleton is the same as the return of the monad, and doubleton is the
union of two singletons.
> singleton :: a -> J a
> singleton = return
> doubleton :: a -> a -> J a
> a `doubleton` b = singleton a `union` singleton b
More generally, is straightforward to convert a non-empty list into a set.
This is the monad morphism from the list monad to J.
> set :: [a] -> J a
> set = foldr1 union . map return
The function 'set' is called 'argsup' in the paper (end of Section
2.2). Note that with our definition of `sup` for Outcome, that 'set'
behaves just like the version of 'argsup' optimized for evaluation
functions that yield -1, 0, or 1 given in the paper.
The J monad finds an optimum (an element of the set with the largest
value under the provided function), and from this we may define the
supremum (the largest value under the provided function).
> optimum :: Sup r => J a -> (a -> r) -> a
> optimum = unJ
> supremum :: Sup r => J a -> (a -> r) -> r
> supremum x k = k (optimum x k)
Pessimum and infimum are the duals of optimum and supremum.
> pessimum :: Neg r => J a -> (a -> r) -> a
> pessimum x k = optimum x (neg . k)
> infimum :: Neg r => J a -> (a -> r) -> r
> infimum x k = neg (supremum x (neg . k))
Existential and universal quantifiers are a special case of
supremum and infimum.
> forsome :: J a -> (a -> Bool) -> Bool
> forsome = supremum
> forevery :: J a -> (a -> Bool) -> Bool
> forevery = infimum
Set membership is a special case of the existential.
> member :: (Eq a) => a -> J a -> Bool
> a `member` x = forsome x (== a)
It is easy to define the set containing false and true, and the Cantor
Set containing every infinite sequence of booleans.
> bit :: J Bool
> bit = set [False,True]
> cantor :: J [Bool]
> cantor = sequence (repeat bit)
Some checks
~~~~~~~~~~~
We check that supremum and infimum behave as expected.
> prop_supremum :: Sup r => (a -> r) -> [a] -> Property
> prop_supremum k x = not (null x) ==>
> (supremum (set x) k == foldr1 sup (map k x))
> check_supremum =
> quickCheck (prop_supremum :: (Int -> Int) -> [Int] -> Property) >>
> quickCheck (prop_supremum :: (Int -> Outcome) -> [Int] -> Property) >>
> quickCheck (prop_supremum :: (Outcome -> Int) -> [Outcome] -> Property) >>
> quickCheck (prop_supremum :: (Outcome -> Outcome) -> [Outcome] -> Property)
> prop_infimum :: Neg r => (a -> r) -> [a] -> Property
> prop_infimum k xs = not (null xs) ==>
> (infimum (set xs) k == foldr1 inf (map k xs))
> check_infimum =
> quickCheck (prop_infimum :: (Int -> Int) -> [Int] -> Property) >>
> quickCheck (prop_infimum :: (Int -> Outcome) -> [Int] -> Property) >>
> quickCheck (prop_infimum :: (Outcome -> Int) -> [Outcome] -> Property) >>
> quickCheck (prop_infimum :: (Outcome -> Outcome) -> [Outcome] -> Property)
And, in particular, we check that forall, forsome, and member on sets
are equivalent to the standard operations on lists.
> prop_forsome :: (a -> Bool) -> [a] -> Property
> prop_forsome k x = not (null x) ==> (forsome (set x) k == any k x)
> check_forsome =
> quickCheck (prop_forsome :: (Int -> Bool) -> [Int] -> Property) >>
> quickCheck (prop_forsome :: (Outcome -> Bool) -> [Outcome] -> Property)
> prop_forevery :: (a -> Bool) -> [a] -> Property
> prop_forevery k x = not (null x) ==> (forevery (set x) k == all k x)
> check_forevery =
> quickCheck (prop_forevery :: (Int -> Bool) -> [Int] -> Property) >>
> quickCheck (prop_forevery :: (Outcome -> Bool) -> [Outcome] -> Property)
> prop_member :: (Eq a) => a -> [a] -> Property
> prop_member a x = not (null x) ==> ((a `member` set x) == (a `elem` x))
> check_member =
> quickCheck (prop_member :: Int -> [Int] -> Property) >>
> quickCheck (prop_member :: Outcome -> [Outcome] -> Property)
Naturals
~~~~~~~~
We introduce naturals, which we use as indexes to streams.
> newtype Nat = Nat Int deriving (Eq,Ord,Show)
> (!!!) :: [a] -> Nat -> a
> x !!! (Nat n) = x !! n
> instance Num Nat where
> Nat m + Nat n = Nat (m+n)
> Nat m * Nat n = Nat (m*n)
> Nat m - Nat n | m >= n = Nat (m-n)
> fromInteger n | n >= 0 = Nat (fromInteger n)
> abs = undefined
> signum = undefined
> instance Enum Nat where
> toEnum n | n >= 0 = Nat n
> fromEnum (Nat n) = n
Fan functional
~~~~~~~~~~~~~~
Given a function over streams of Booleans, the fan functional
determines the least position past which the arguments of the function
are not examined.
> fan :: Eq r => ([Bool] -> r) -> Nat
> fan f = least (\ (Nat n) ->
> forevery cantor (\x ->
> forevery cantor (\y ->
> (take n x == take n y) --> (f x == f y))))
> least :: (Nat -> Bool) -> Nat
> least p = head [ i | i <- [0..], p i ]
> (-->) :: Bool -> Bool -> Bool
> p --> q = not p || q
An alternative definition of the fan functional, from Ulrich
Berger's thesis (1990):
> fan2 :: Eq r => ([Bool] -> r) -> Nat
> fan2 f = if forevery cantor (\x -> f x == f (repeat False))
> then 0
> else 1 + max (fan2 (f.(False:))) (fan2 (f.(True:)))
Given a list of naturals, we can generate a function that examines its
argument at the specified positions, and use this to check fan. In
order for the test to complete in reasonable time, we restrict
ourselves to short lists of small naturals, using the Quick Check
function 'resize'.
> examineAt :: [Nat] -> [Bool] -> Bool
> examineAt ns x = and [ x !!! n | n <- ns ]
> prop_fan :: (([Bool] -> Bool) -> Nat) -> Gen [Nat] -> Property
> prop_fan fan gen = forAll gen (\ns ->
> fan (examineAt ns) == foldr max 0 [ n + 1 | n <- ns])
> check_fan = quickCheck (prop_fan fan (resize 4 arbitrary))
> check_fan2 = quickCheck (prop_fan fan2 (resize 4 arbitrary))
We can also check that the two functionals are equivalent.
> prop_equal_fan :: Gen [Nat] -> Property
> prop_equal_fan gen = forAll gen (\ns ->
> fan (examineAt ns) == fan2 (examineAt ns))
> check_equal_fan = quickCheck (prop_equal_fan (resize 4 arbitrary))
In this case, it would be better to generate functions directly rather
than generate a list and apply examineAt. However, doing so causes
QuickCheck to loop, because coarbitrary for lists examines too much of
its input.
Equality for functionals
~~~~~~~~~~~~~~~~~~~~~~~~
We call a function type a -> b representable if every function of
the type can be generated from a stream of Booleans. In particular,
the function type Int -> Bool is representable. We use 'interleave',
the standard mapping of integers to naturals.
> interleave :: Int -> Nat
> interleave i | i >= 0 = Nat (2*i)
> | i < 0 = Nat (2*(-i)-1)
> class Representable a b where
> decode :: [Bool] -> (a -> b)
> instance Representable Int Bool where
> decode x i = x !!! interleave i
> instance Representable Nat Bool where
> decode x i = x !!! i
Equality is decidable for any functional of type (a->b)->c where a->b
is representable and c has equality.
> equal :: (Representable a b, Eq c) => ((a->b)->c) -> ((a->b)->c) -> Bool
> equal f g = forevery cantor (\x -> f (decode x) == g (decode x))
We check that equality is reflexive.
> prop_reflexive :: (Representable a b, Eq c) => Gen ((a->b)->c) -> Property
> prop_reflexive gen =
> forAll gen (\f -> equal f f)
> check_reflexive =
> quickCheck (prop_reflexive (resize 5 arbitrary :: Gen ((Int->Bool)->Outcome)))
We check that two arbitrary functions are either equal (in which case
they should have the same value on arbitrary arguments) or unequal (in
which case we can search the cantor space for a counterexample on
which they are unequal). We use the QuickCheck function 'resize' to
restrict our attention to small cases, and 'label' to indicate how
many random tests fall under each case.
> prop_equal :: (Representable a b, Eq c) => Gen ((a->b)->c) -> Gen (a->b) -> Property
> prop_equal gen gen2 =
> forAll gen (\f ->
> forAll gen (\g ->
> if (equal f g) then
> forAll gen2 (\a ->
> label "equal" (f a == g a))
> else
> let a = decode (optimum cantor (\x -> f (decode x) /= g (decode x))) in
> label "unequal" (f a /= g a)))
> check_equal =
> quickCheck (prop_equal (resize 8 arbitrary :: Gen ((Int->Bool)->Outcome))
> (resize 8 arbitrary :: Gen (Int->Bool)))
Run all checks
~~~~~~~~~~~~~~
For convenience, here is a function that runs all checks.
> main =
> check_max >>
> check_atomic >>
> check_geq >>
> check_involution >>
> check_conjunction >>
> check_min >>
> check_supremum >>
> check_infimum >>
> check_forsome >>
> check_forevery >>
> check_member >>
> check_fan >>
> check_fan2 >>
> check_equal_fan >>
> check_reflexive >>
> check_equal
Efficiency
~~~~~~~~~~
An earlier version defined `union` in terms of `doubleton`, rather
than the other way around.
> doubleton2 :: a -> a -> J a
> a `doubleton2` b = J (\k -> if k a `dominates` k b then a else b)
> union2 :: J a -> J a -> J a
> x `union2` y = join (x `doubleton2` y)
> set2 :: [a] -> J a
> set2 = foldr1 union2 . map singleton
It is easy to check that this is equivalent, though less efficient.
x `union2` y
=
join (x `doubleton2` y)
=
J (\k -> unJ (unJ (x `doubleton` y) (\x -> k (unJ x k))) k)
=
J (\k -> unJ ((\k -> if k x `dominates` k y then x else y) (\x -> k (unJ x k))) k)
=
J (\k -> unJ (if k (unj x k) `dominates` k (unJ x k) then x else y) k)
=
J (\k -> if k (unj x k) `dominates` k (unJ x k) then unj x k else unj y k)
The loss of efficiency turns out to be exponential---while the
supremum of a list of length 24 can be computed too fast to notice
using set, using set2 it takes about half a minute. For a list
of length 25, it takes twice as long.
*Main> :set +s
*Main> supremum (set [0..23]) id :: Int
23
(0.00 secs, 525096 bytes)
*Main> supremum (set2 [0..23]) id :: Int
23
(30.10 secs, 3192968796 bytes)
*Main> supremum (set [0..24]) id :: Int
24
(0.00 secs, 525092 bytes)
*Main> supremum (set2 [0..24]) id :: Int
24
(60.19 secs, 6385879616 bytes)
Appendix: QuickCheck support
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To support testing with QuickCheck, we define instances
of Arbitrary and CoArbitrary for Outcome and Naturals.
> instance Arbitrary Outcome where
> arbitrary = oneof (map return [Lose, Draw, Win])
> instance CoArbitrary Outcome where
> coarbitrary o = variant (fromEnum o)
> instance Arbitrary Nat where
> arbitrary = sized (\ n -> do m <- choose (0,n)
> return (Nat m))
> instance CoArbitrary Nat where
> coarbitrary (Nat n) = variant n
Acknowledgements
~~~~~~~~~~~~~~~~
Thanks for their comments to Lennart Augustsson, Martin Escardo,
Kenneth MacKenzie, James McKenna, Paulo Oliva, and Kalani Thielen.
References
~~~~~~~~~~
[1] Martin Escardo and Paulo Oliva, What Sequential Games, the
Tychonoff Theorem and the Double-Negation Shift have in Common,
MSFP 2010.
(Additional reference, added 3 Dec 2010)
[2] Martin Escardo and Paulo Oliva, Sequential Games and optimal
strategies, Proceedings of the Royal Society A, published online 1
December 2010, doi: 10.1098/rspa.2010.0471.
http://rspa.royalsocietypublishing.org/content/early/2010/11/26/rspa.2010.0471