posetFunctionality.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module PosetFunctionality where

import qualified Math.Combinatorics.Poset as PS
import qualified Math.Combinat.Partitions.Set as SetPart
import qualified Data.Set as Set

getSet :: PS.Poset t1 -> [t1]
getSet (PS.Poset (set,_)) = set

getPO :: PS.Poset t1 -> (t1 -> t1 -> Bool)
getPO (PS.Poset (_,po)) = po

-- biggerThanAll p z xs tells if z is greater than or equal to all x from xs
biggerThanAll:: PS.Poset t1 -> t1 -> [t1] -> Bool
biggerThanAll (PS.Poset (set,po)) z xs = and [z `po` x | x <- xs]

-- upperBounds p xs gives all the elements in poset p such that they are greater than or equal to everything in xs
upperBounds:: PS.Poset t1 -> [t1] -> [t1]
upperBounds (PS.Poset (set,po)) xs = [z | z <- set, biggerThanAll (PS.Poset (set,po)) z xs]

--given the list of upperBounds, an element z of this list may be not a good candidate for least upper bound
-- this happens when z is greater than or equal to an element of the list besides itself. That gives a length > 1
isTooBig:: PS.Poset t1 -> [t1] -> t1 -> Bool
isTooBig (PS.Poset (set,po)) zs z = (length $ [z1 | z1 <- zs , z `po` z1]) > 1

--make the list of upperBounds and then filter away the candidates that are too big
join:: PS.Poset t1 -> [t1] -> [t1]
join (PS.Poset (set,po)) xs = filter (\y -> not $ isTooBig (PS.Poset (set,po)) zs y) zs
                              where zs = upperBounds (PS.Poset (set,po)) xs

-- Test functionality of join by using the poset of divisors 24
example :: [Int] -> [Int]
example xs = join (PS.dual $ PS.posetD 24) xs

-- flip everything upside down
meet:: PS.Poset t1 -> [t1] -> [t1]
meet p xs = join (PS.dual p) xs

leftAdjointHelper p1@(PS.Poset (p1Set,p1po)) p2@(PS.Poset (p2Set,p2po)) g p = show [q | q <- p1Set , (g q) `p2po` p]

-- assume g is a right adjoint of something, find it's left adjoint
leftAdjoint:: PS.Poset t1 -> PS.Poset t2 -> (t1 -> t2) -> t2 -> [t1]
leftAdjoint p1@(PS.Poset (p1Set,p1po)) p2@(PS.Poset (p2Set,p2po)) g p = meet p1 qs
                                                                     where qs = [q | q <- p1Set , (g q) `p2po` p]

rightAdjointHelper p1@(PS.Poset (p1Set,p1po)) p2@(PS.Poset (p2Set,p2po)) f q = show [p | p <- p1Set , q `p2po` (f p)]

-- assume f is a left adjoint of something, find it's right adjoint
rightAdjoint:: PS.Poset t1 -> PS.Poset t2 -> (t1 -> t2) -> t2 -> [t1]
rightAdjoint p1@(PS.Poset (p1Set,p1po)) p2@(PS.Poset (p2Set,p2po)) f q = join p1 [p | p <- p1Set , q `p2po` (f p)]

-- Exercise 1.77
data SimpleExample = Zero | One | Two deriving (Show,Eq)
simpleExampleOrder Zero _ = True
simpleExampleOrder One One = True
simpleExampleOrder One Two = True
simpleExampleOrder Two Two = True
simpleExampleOrder _ _ = False
simpleExamplePoset = PS.dual ( PS.Poset ([Zero,One,Two],simpleExampleOrder) )
sampleF Zero = Zero
sampleF One = Zero
sampleF Two = Two

myPowerset :: (Ord a) => Set.Set a -> Set.Set (Set.Set a)
myPowerset s = Set.fromList $ map (Set.fromList) (powerList $ Set.toList s)
powerList :: [a] -> [[a]]
powerList [] = [[]]
powerList (x:xs) = powerList xs ++ map (x:) (powerList xs)

-- give the poset structure of such a poset
-- the implementation in Data.Set uses total order on X and Y
powerSetPoset :: Ord a => Set.Set a -> PS.Poset (Set.Set a)
powerSetPoset xs = PS.dual $ PS.Poset (Set.elems $ myPowerset xs,Set.isSubsetOf)

fUStar :: (Ord a1, Ord a2) => (a1 -> a2) -> Set.Set a1 -> Set.Set a2 -> Set.Set a1
fUStar f xSet ys = Set.fromList [x | x <- Set.toList xSet , Set.member (f x) ys]

--should only be one set in the output list, but can't guarantee that because left and right adjoint output lists
fLStar :: (Ord a1, Ord a2) => (a1 -> a2) -> Set.Set a1 -> Set.Set a2 -> Set.Set a1 -> [Set.Set a2]
fLStar f xSet ySet xs = rightAdjoint (powerSetPoset ySet) (powerSetPoset xSet) (\ys -> (fUStar f xSet ys)) xs

--should only be one set in the output list, but can't guarantee that because left and right adjoint output lists
fLShriek :: (Ord a1, Ord a2) => (a1 -> a2) -> Set.Set a1 -> Set.Set a2 -> Set.Set a1 -> [Set.Set a2]
fLShriek f xSet ySet xs = leftAdjoint (powerSetPoset ySet) (powerSetPoset xSet) (\ys -> (fUStar f xSet ys)) xs

--Exercise 1.95
exampleYSet = Set.fromList [1,2,3,4]
exampleXSet = Set.fromList [5,6]
exampleFunction 5 = 2
exampleFunction 6 = 2
exampleB1 = Set.fromList [1,2,3]
exampleB2 = Set.fromList [1,3]
exampleA1 = Set.fromList [6]
exampleA2 = Set.fromList [5,6]
parta1 = fUStar exampleFunction exampleXSet exampleB1
parta2 = fUStar exampleFunction exampleXSet exampleB2
partb1 = fLShriek exampleFunction exampleXSet exampleYSet exampleA1
partb2 = fLShriek exampleFunction exampleXSet exampleYSet exampleA2
partc1 = fLStar exampleFunction exampleXSet exampleYSet exampleA1
partc2 = fLStar exampleFunction exampleXSet exampleYSet exampleA2

--partition Logic
compareSetPartitions :: SetPart.SetPartition -> SetPart.SetPartition -> Bool
compareSetPartitions sp1 sp2 = and [isXSubset (Set.fromList x) sp1 | x <- SetPart.fromSetPartition sp2 ] where 
                               isXSubset x1 sp1' = or [ Set.isSubsetOf x1 (Set.fromList y) | y <- SetPart.fromSetPartition sp1' ]
partitionPoset :: Int -> PS.Poset SetPart.SetPartition
partitionPoset n = PS.Poset (SetPart.setPartitions n, compareSetPartitions)

--TODO: fUStar and fLShriek but this one has no fLStar
-- compiled but not tested

fUStarPartitionsHelper:: (Int -> Int) -> Int -> SetPart.SetPartition -> [[Int]]
fUStarPartitionsHelper f xSize spYs = [Set.toList $ fUStar f (Set.fromList [1..xSize]) (Set.fromList myS) | myS <- SetPart.fromSetPartition spYs]
clearEmpties :: [[Int]] -> [[Int]]
clearEmpties xs = [x | x <- xs, length x>0]

fUStarPartitions :: (Int -> Int) -> Int -> SetPart.SetPartition -> SetPart.SetPartition
fUStarPartitions f xSize spYs = SetPart.toSetPartition $ clearEmpties $ fUStarPartitionsHelper f xSize spYs

fLShriekPartitions :: (Int -> Int) -> Int -> Int -> SetPart.SetPartition -> [SetPart.SetPartition]
fLShriekPartitions f xSize ySize xPartition = leftAdjoint (partitionPoset xSize) (partitionPoset ySize) (\spYs -> (fUStarPartitions f xSize spYs)) xPartition

--free commutative monoidal preorder without any reactions

data Nat = Z | S Nat deriving (Show)

data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

data Vector a n where
  Nil  :: Vector a Z
  (:-) :: a -> Vector a n -> Vector a (S n)
infixr 5 :-

deriving instance Eq a => Eq (Vector a n)

toList :: Vector a n -> [a]
toList Nil = []
toList (x :- xs) = x : toList xs
instance Show a => Show (Vector a n) where
  showsPrec d = showsPrec d . toList

myReplicate :: SNat n -> a -> Vector a n
myReplicate SZ     _ = Nil
myReplicate (SS n) a = a :- myReplicate n a
--takes a natural number n and a list of integers and puts them into a vector of length n
-- default to 0 if the list is too short
fromList:: SNat n -> [Int] -> Vector Int n
fromList SZ _ = Nil
fromList (SS n) [] = myReplicate (SS n) (0)
fromList (SS n) (x:xs) = x :- (fromList n xs)

addVectors :: SNat n -> Vector Int n -> Vector Int n -> Vector Int n
addVectors n1 v1 v2 = fromList n1 $ zipWith (+) (toList v1) (toList v2)

-- takes an occupied natural number for the number of items like possible chemicals in a complex
-- and a maximum number to say there are at most maxAmount of any one of them
-- and produce the poset with no reactions only the product order
noReactionsSet :: SNat n -> Int -> [Vector Int n]
noReactionsSet SZ _ = [Nil]
noReactionsSet (SS x) maxAmount = [x1 :- y | x1 <- [0..maxAmount], y <- (noReactionsSet x maxAmount)]

-- reversed because can throw away from 4 to get to 3, so 4 <= 3 in reachability ordering
productOrder :: Ord a => Vector a n -> Vector a n -> Bool
productOrder Nil Nil = True
productOrder (x:-xs) (y:-ys) = (y<=x) && productOrder xs ys

noReactionsPoset :: SNat n -> Int -> PS.Poset (Vector Int n)
noReactionsPoset numItems maxAmount = PS.Poset (mySet,productOrder) where mySet=(noReactionsSet numItems maxAmount)

-- given the knowledge that x>=y in new partial order, all the ones that are automatic by
-- a=z+x >= b=z+y
-- mostly untested but it does compile
addReaction :: PS.Poset (Vector Int n) -> SNat n -> (Vector Int n,Vector Int n) -> PS.Poset (Vector Int n)
addReaction (PS.Poset (set,oldpo)) n1 (x,y) = PS.Poset (set,newpo)
                                          where newpo a b = ((a `oldpo` b) || (or [((a==addVectors n1 z x) && (b==addVectors n1 z y)) | z <- set]))

myThree = (SS $ SS $ SS $ SZ)
exampleNoReaction = noReactionsPoset myThree 4
exampleWithReaction = addReaction exampleNoReaction myThree ((2:-0:-0:-Nil),(0:-1:-0:-Nil))

--One Successful Test Case, now just mostly untested
testCase1=exampleWithReaction
testCase1Conf=(getPO testCase1) (3:-2:-1:-Nil) (1:-3:-1:-Nil)
-- evaluates to True as desired
testCase2=exampleNoReaction
testCase2Conf=(getPO testCase2) (3:-2:-1:-Nil) (1:-3:-1:-Nil)
-- evaluates to False as desired

-- test case, has not been checked yet
-- Bennett's laws
--vectors are ordered as (# qubits,# ebits,# cbits)
--there are at most 4 of any resource
bennettExample0 = noReactionsPoset myThree 4
--1 qubit to 1 ebit or cbit by measurement
bennettExample1 = addReaction bennettExample0 myThree ((1:-0:-0:-Nil),(0:-1:-0:-Nil))
bennettExample2 = addReaction bennettExample1 myThree ((1:-0:-0:-Nil),(0:-0:-1:-Nil))
-- superdense coding
bennettExample3 = addReaction bennettExample2 myThree ((1:-1:-0:-Nil),(0:-0:-2:-Nil))
-- teleportation
bennettExample = addReaction bennettExample3 myThree ((0:-1:-2:-Nil),(1:-0:-0:-Nil))

-- The ordinal sum of two posets, put everything in Y on top of everything in X
-- actually could write as a special case of collage where phi(a,b)=True
osum :: PS.Poset a -> PS.Poset b -> PS.Poset (Either a b)
osum (PS.Poset (setA,poA)) (PS.Poset (setB,poB)) = PS.Poset (set,po)
    where set = map Left setA ++ map Right setB
          po (Left a1) (Left a2) = poA a1 a2
          po (Right b1) (Right b2) = poB b1 b2
          po (Left _) (Right _) = True
          po _ _ = False

-- collage of the profunctor between two posets, does not check that phi is monotone
-- assumes you gave something sensible
collage :: PS.Poset a -> PS.Poset b -> (a -> b -> Bool) -> PS.Poset (Either a b)
collage (PS.Poset (setA,poA)) (PS.Poset (setB,poB)) phi = PS.Poset (set,po)
    where set = map Left setA ++ map Right setB
          po (Left a1) (Left a2) = poA a1 a2
          po (Right b1) (Right b2) = poB b1 b2
          po (Left a1) (Right b2) = phi a1 b2
          po _ _ = False

data FeasibilityRelation a b = FeasibilityRelation{source :: (PS.Poset a), target :: (PS.Poset b) , phi :: (a -> b -> Bool)}

collageF :: FeasibilityRelation a b -> PS.Poset (Either a b)
collageF feasibility1 = collage (source feasibility1) (target feasibility1) (phi feasibility1)

-- Example is untested, probably have some arrows flipped the wrong way around
-- didn't keep careful track of which is op and which is not.
data FeasibilityExXSetD = North | South | East | West deriving (Show,Read,Eq)
feasibilityExXSet :: [FeasibilityExXSetD]
feasibilityExXSet = [North,South,East,West]
feasibilityExXpo South _ = True
feasibilityExXpo West West = True
feasibilityExXpo West North = True
feasibilityExXpo East East = True
feasibilityExXpo East North = True
feasibilityExXpo North North = True
feasibilityExXpo _ _ = False
feasibilityExX = PS.Poset (feasibilityExXSet,feasibilityExXpo)
data FeasibilityExYSetD = A | B | C | D | E  deriving (Show,Read,Eq)
feasibilityExYSet :: [FeasibilityExYSetD]
feasibilityExYSet = [A,B,C,D,E]
feasibilityExYpo A _ = True
feasibilityExYpo B B = True
feasibilityExYpo B D = True
feasibilityExYpo C C = True
feasibilityExYpo D D = True
feasibilityExYpo E E = True
feasibilityExYpo _ _ = False
feasibilityExY = PS.Poset (feasibilityExYSet,feasibilityExYpo)
-- the direct connections, the ones drawn in blue arrows
feasibilityExPhiHelper :: FeasibilityExXSetD -> FeasibilityExYSetD -> Bool
feasibilityExPhiHelper South A = True
feasibilityExPhiHelper East B = True
feasibilityExPhiHelper North C = True
feasibilityExPhiHelper North E = True
feasibilityExPhiHelper _ _ = False
feasibilityExPhi :: FeasibilityExXSetD -> FeasibilityExYSetD -> Bool
feasibilityExPhi x1 y1 = or [(feasibilityExXpo x1 x2) && (feasibilityExYpo y2 y1) | y2 <- feasibilityExYSet, x2 <- feasibilityExXSet, (feasibilityExPhiHelper x2 y2)]
feasibilityEx :: PS.Poset (Either FeasibilityExXSetD FeasibilityExYSetD)
feasibilityEx = collage feasibilityExX feasibilityExY feasibilityExPhi
feasibilityEx2 = [((s1,s2),(getPO feasibilityEx) s1 s2) | s1 <- allEx, s2 <- allEx] where allEx = (getSet feasibilityEx)

composePhi :: (a -> b -> Bool) -> (b -> c -> Bool) -> [b] -> a -> c -> Bool
composePhi phi1 phi2 allYs aTest cTest = or [(phi1 aTest bTest) && (phi2 bTest cTest) | bTest <- allYs]

composeFeasibilityRelations :: FeasibilityRelation a b -> FeasibilityRelation b c -> FeasibilityRelation a c
composeFeasibilityRelations feasible1 feasible2 = FeasibilityRelation{source=(source feasible1),target=(target feasible2),
                                                                      phi=(composePhi (phi feasible1) (phi feasible2) (getSet (target feasible1)))}