From: Anders Date: Wed, 18 Mar 2015 10:57:06 +0000 (+0100) Subject: Add Connections X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=6922dabf06039c6aca04bcae02d233f17d413bc8;p=cubicaltt.git Add Connections --- diff --git a/Connections.hs b/Connections.hs new file mode 100644 index 0000000..536e4a0 --- /dev/null +++ b/Connections.hs @@ -0,0 +1,445 @@ +{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, + GeneralizedNewtypeDeriving #-} +module Connections where + +import Control.Applicative +import Data.List +import Data.Map (Map,(!)) +import Data.Set (Set) +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.Maybe +import Test.QuickCheck + +newtype Name = Name Integer + deriving (Arbitrary,Eq,Ord) + +instance Show Name where + show (Name i) = 'i' : show i + +swapName :: Name -> (Name,Name) -> Name +swapName k (i,j) | k == i = j + | k == j = i + | otherwise = k + + +-- | Directions +data Dir = Zero | One + deriving (Eq,Ord) + +instance Show Dir where + show Zero = "0" + show One = "1" + +instance Num Dir where + Zero + Zero = Zero + _ + _ = One + + Zero * _ = Zero + One * x = x + + abs = id + signum _ = One + + negate Zero = One + negate One = Zero + + fromInteger 0 = Zero + fromInteger 1 = One + fromInteger _ = error "fromInteger Dir" + +instance Arbitrary Dir where + arbitrary = do + b <- arbitrary + return $ if b then Zero else One + +-- | Face + +-- Faces of the form: [(i,0),(j,1),(k,0)] +type Face = Map Name Dir + +instance Arbitrary Face where + arbitrary = Map.fromList <$> arbitrary + +showFace :: Face -> String +showFace alpha = concat [ "(" ++ show i ++ "," ++ show d ++ ")" + | (i,d) <- Map.toList alpha ] + +swapFace :: Face -> (Name,Name) -> Face +swapFace alpha ij = Map.mapKeys (`swapName` ij) alpha + +-- i,j,k,l :: Name +-- i = Name 0 +-- j = Name 1 +-- k = Name 2 +-- l = Name 3 + +-- f1,f2 :: Face +-- f1 = Map.fromList [(i,0),(j,1),(k,0)] +-- f2 = Map.fromList [(i,0),(j,1),(l,1)] + +-- Check if two faces are compatible +compatible :: Face -> Face -> Bool +compatible xs ys = and (Map.elems (Map.intersectionWith (==) xs ys)) + +compatibles :: [Face] -> Bool +compatibles [] = True +compatibles (x:xs) = all (x `compatible`) xs && compatibles xs + +-- Partial composition operation +meet :: Face -> Face -> Face +meet = Map.unionWith f + where f d1 d2 = if d1 == d2 then d1 else error "meet: incompatible faces" + +meetMaybe :: Face -> Face -> Maybe Face +meetMaybe x y = if compatible x y then Just $ meet x y else Nothing + +meetCom :: Face -> Face -> Property +meetCom xs ys = compatible xs ys ==> xs `meet` ys == ys `meet` xs + +meetAssoc :: Face -> Face -> Face -> Property +meetAssoc xs ys zs = compatibles [xs,ys,zs] ==> + xs `meet` (ys `meet` zs) == (xs `meet` ys) `meet` zs + +meetId :: Face -> Bool +meetId xs = xs `meet` xs == xs + +meets :: [Face] -> [Face] -> [Face] +meets xs ys = nub [ meet x y | x <- xs, y <- ys, compatible x y ] + +-- instance Ord Face where + +leq :: Face -> Face -> Bool +alpha `leq` beta = meetMaybe alpha beta == Just alpha + +comparable :: Face -> Face -> Bool +comparable alpha beta = alpha `leq` beta || beta `leq` alpha + +incomparables :: [Face] -> Bool +incomparables [] = True +incomparables (x:xs) = all (not . (x `comparable`)) xs && incomparables xs + +(~>) :: Name -> Dir -> Face +i ~> d = Map.singleton i d + +eps :: Face +eps = Map.empty + +-- Compute the witness of A <= B, ie compute C s.t. B = CA +-- leqW :: Face -> Face -> Face +-- leqW = undefined + +-- data Faces = Faces (Set Face) + +-- instance Nominal Faces where +-- support (Faces f) = +-- act (Faces f) (i, phi) = Faces f + +-- | Formulas +data Formula = Dir Dir + | Atom Name + | NegAtom Name + | Formula :/\: Formula + | Formula :\/: Formula + deriving (Eq,Show) + +arbFormula :: [Name] -> Int -> Gen Formula +arbFormula names s = + frequency [ (1, Dir <$> arbitrary) + , (1, Atom <$> elements names) + , (1, NegAtom <$> elements names) + , (s, do op <- elements [andFormula,orFormula] + op <$> arbFormula names s' <*> arbFormula names s') + ] + where s' = s `div` 3 + +instance Arbitrary Formula where + arbitrary = do + n <- arbitrary :: Gen Integer + sized $ arbFormula (map Name [0..(abs n)]) + +class ToFormula a where + toFormula :: a -> Formula + +instance ToFormula Formula where + toFormula = id + +instance ToFormula Name where + toFormula = Atom + +instance ToFormula Dir where + toFormula = Dir + +-- TODO: FINISH! +-- instance Show a => Show (Formula a) where +-- show Zero = "0" +-- show One = "1" +-- show (NegAtom a) = "~" ++ show a +-- show (Atom a) = show a +-- show (a :/\: b) = show a ++ " /\ " ++ show b + +negFormula :: Formula -> Formula +negFormula (Dir b) = Dir (- b) +negFormula (Atom i) = NegAtom i +negFormula (NegAtom i) = Atom i +negFormula (phi :/\: psi) = orFormula (negFormula phi) (negFormula psi) +negFormula (phi :\/: psi) = andFormula (negFormula phi) (negFormula psi) + +andFormula :: Formula -> Formula -> Formula +andFormula (Dir Zero) _ = Dir Zero +andFormula _ (Dir Zero) = Dir Zero +andFormula (Dir One) phi = phi +andFormula phi (Dir One) = phi +andFormula phi psi = phi :/\: psi + +orFormula :: Formula -> Formula -> Formula +orFormula (Dir One) _ = Dir One +orFormula _ (Dir One) = Dir One +orFormula (Dir Zero) phi = phi +orFormula phi (Dir Zero) = phi +orFormula phi psi = phi :\/: psi + +evalFormula :: Formula -> Face -> Formula +evalFormula phi alpha = + Map.foldWithKey (\i d psi -> act psi (i,Dir d)) phi alpha + + -- (Dir b) alpha = Dir b +-- evalFormula (Atom i) alpha = case Map.lookup i alpha of +-- Just b -> Dir b +-- Nothing -> Atom i +-- evalFormula (Not phi) alpha = negFormula (evalFormula phi alpha) +-- evalFormula (phi :/\: psi) alpha = +-- andFormula (evalFormula phi alpha) (evalFormula psi alpha) +-- evalFormula (phi :\/: psi) alpha = +-- orFormula (evalFormula phi alpha) (evalFormula psi alpha) + +-- find a better name? +-- phi b = max {alpha : Face | phi alpha = b} +invFormula :: Formula -> Dir -> [Face] +invFormula (Dir b') b = [ eps | b == b' ] +invFormula (Atom i) b = [ Map.singleton i b ] +invFormula (NegAtom i) b = [ Map.singleton i (- b) ] +invFormula (phi :/\: psi) Zero = invFormula phi 0 `union` invFormula psi 0 +invFormula (phi :/\: psi) One = + meets (invFormula phi 1) (invFormula psi 1) +invFormula (phi :\/: psi) b = invFormula (negFormula phi :/\: negFormula psi) (- b) + +-- primeImplicants :: Formula -> Dir -> System () +-- primeImplicants phi Zero = primeImplicants (NegAtom phi) One +-- primeImplicants phi One = undefined + +propInvFormulaIncomp :: Formula -> Dir -> Bool +propInvFormulaIncomp phi b = incomparables (invFormula phi b) + +prop_invFormula :: Formula -> Dir -> Bool +prop_invFormula phi b = + all (\alpha -> phi `evalFormula` alpha == Dir b) (invFormula phi b) + +testInvFormula :: [Face] +testInvFormula = invFormula (Atom (Name 0) :/\: Atom (Name 1)) 1 + +-- | Nominal +gensym :: [Name] -> Name +gensym [] = Name 0 +gensym xs = Name (max+1) + where Name max = maximum xs + +gensyms :: [Name] -> [Name] +gensyms d = let x = gensym d in x : gensyms (x : d) + +class Nominal a where + support :: a -> [Name] +-- act u (i,phi) should have u # (phi - i) ?? + act :: a -> (Name,Formula) -> a + + swap :: a -> (Name,Name) -> a + -- swap u (i,j) = + -- where k = fresh (u,i,j) + +fresh :: Nominal a => a -> Name +fresh = gensym . support + +freshs :: Nominal a => a -> [Name] +freshs = gensyms . support + +unions :: Eq a => [[a]] -> [a] +unions = foldr union [] + +unionsMap :: Eq b => (a -> [b]) -> [a] -> [b] +unionsMap f = unions . map f + +instance Nominal () where + support () = [] + act () _ = () + swap () _ = () + +instance (Nominal a, Nominal b) => Nominal (a, b) where + support (a, b) = support a `union` support b + act (a,b) f = (act a f,act b f) + swap (a,b) n = (swap a n,swap b n) + +instance (Nominal a, Nominal b, Nominal c) => Nominal (a, b, c) where + support (a,b,c) = unions [support a, support b, support c] + act (a,b,c) f = (act a f,act b f,act c f) + swap (a,b,c) n = (swap a n,swap b n,swap c n) + +instance (Nominal a, Nominal b, Nominal c, Nominal d) => + Nominal (a, b, c, d) where + support (a,b,c,d) = unions [support a, support b, support c, support d] + act (a,b,c,d) f = (act a f,act b f,act c f,act d f) + swap (a,b,c,d) n = (swap a n,swap b n,swap c n,swap d n) + +instance (Nominal a, Nominal b, Nominal c, Nominal d, Nominal e) => + Nominal (a, b, c, d, e) where + support (a,b,c,d,e) = + unions [support a, support b, support c, support d, support e] + act (a,b,c,d,e) f = (act a f,act b f,act c f,act d f, act e f) + swap (a,b,c,d,e) n = + (swap a n,swap b n,swap c n,swap d n,swap e n) + +instance (Nominal a, Nominal b, Nominal c, Nominal d, Nominal e, Nominal h) => + Nominal (a, b, c, d, e, h) where + support (a,b,c,d,e,h) = + unions [support a, support b, support c, support d, support e, support h] + act (a,b,c,d,e,h) f = (act a f,act b f,act c f,act d f, act e f, act h f) + swap (a,b,c,d,e,h) n = + (swap a n,swap b n,swap c n,swap d n,swap e n,swap h n) + +instance Nominal a => Nominal [a] where + support xs = unions (map support xs) + act xs f = [ act x f | x <- xs ] + swap xs n = [ swap x n | x <- xs ] + +instance Nominal a => Nominal (Maybe a) where + support = maybe [] support + act v f = fmap (\u -> act u f) v + swap a n = fmap (`swap` n) a + +instance Nominal Formula where + support (Dir _) = [] + support (Atom i) = [i] + support (NegAtom i) = [i] + support (phi :/\: psi) = support phi `union` support psi + support (phi :\/: psi) = support phi `union` support psi + + act (Dir b) (i,phi) = Dir b + act (Atom j) (i,phi) | i == j = phi + | otherwise = Atom j + act (NegAtom j) (i,phi) | i == j = negFormula phi + | otherwise = NegAtom j + act (psi1 :/\: psi2) (i,phi) = act psi1 (i,phi) `andFormula` act psi2 (i,phi) + act (psi1 :\/: psi2) (i,phi) = act psi1 (i,phi) `orFormula` act psi2 (i,phi) + + swap (Dir b) (i,j) = Dir b + swap (Atom k) (i,j)| k == i = Atom j + | k == j = Atom i + | otherwise = Atom k + swap (NegAtom k) (i,j)| k == i = NegAtom j + | k == j = NegAtom i + | otherwise = NegAtom k + swap (psi1 :/\: psi2) (i,j) = swap psi1 (i,j) :/\: swap psi2 (i,j) + swap (psi1 :\/: psi2) (i,j) = swap psi1 (i,j) :\/: swap psi2 (i,j) + +face :: Nominal a => a -> Face -> a +face = Map.foldWithKey (\i d a -> act a (i,Dir d)) + +-- the faces should be incomparable +type System a = Map Face a + +showSystem :: Show a => System a -> String +showSystem ts = concat $ intersperse ", " [ showFace alpha ++ " |-> " ++ show u + | (alpha,u) <- Map.toList ts ] + +insertSystem :: Face -> a -> System a -> System a +insertSystem alpha v ts = + case find (comparable alpha) (Map.keys ts) of + Just beta | alpha `leq` beta -> ts + | otherwise -> Map.insert alpha v (Map.delete beta ts) + Nothing -> Map.insert alpha v ts + +insertsSystem :: [(Face, a)] -> System a -> System a +insertsSystem faces us = + foldr (\(alpha, ualpha) -> insertSystem alpha ualpha) us faces + +mkSystem :: [(Face, a)] -> System a +mkSystem = flip insertsSystem Map.empty + +unionSystem :: System a -> System a -> System a +unionSystem us vs = insertsSystem (Map.assocs us) vs + +-- could something like that work?? +-- transposeSystem :: System [a] -> [System a] +-- transposeSystem as = Map.tranverseWithKey (const . id) as + +-- TODO: add some checks +transposeSystemAndList :: System [a] -> [b] -> [(System a,b)] +transposeSystemAndList _ [] = [] +transposeSystemAndList tss (u:us) = + (Map.map head tss,u):transposeSystemAndList (Map.map tail tss) us + +-- transposeSystem :: System [a] -> [System a] +-- transposeSystem ts = +-- Map.map (\as -> head a) ts : transposeSystem (Map.map (\as -> tail as) ts) + +-- Quickcheck this: +-- (i = phi) * beta = (beta - i) * (i = phi beta) + +-- Now we ensure that the keys are incomparable +instance Nominal a => Nominal (System a) where + support s = unions (map Map.keys $ Map.keys s) + `union` support (Map.elems s) + + act s (i, phi) = addAssocs (Map.assocs s) + where + addAssocs [] = Map.empty + addAssocs ((alpha,u):alphaus) = + let s' = addAssocs alphaus + in case Map.lookup i alpha of + Just d -> let beta = Map.delete i alpha + in foldr (\delta s'' -> insertSystem (meet delta beta) + (face u (Map.delete i delta)) s'') + s' (invFormula (face phi beta) d) + Nothing -> insertSystem alpha (act u (i,face phi alpha)) s' + + swap s ij = Map.mapKeys (`swapFace` ij) (Map.map (`swap` ij) s) + +-- carve a using the same shape as the system b +border :: Nominal a => a -> System b -> System a +border v = Map.mapWithKey (const . face v) + +shape :: System a -> System () +shape ts = border () ts + +instance (Nominal a, Arbitrary a) => Arbitrary (System a) where + arbitrary = do + a <- arbitrary + border a <$> arbitraryShape (support a) + where + arbitraryShape :: [Name] -> Gen (System ()) + arbitraryShape supp = do + phi <- sized $ arbFormula supp + return $ Map.fromList [(face,()) | face <- invFormula phi 0] + +sym :: Nominal a => a -> Name -> a +sym a i = a `act` (i, NegAtom i) + +rename :: Nominal a => a -> (Name, Name) -> a +rename a (i, j) = a `act` (i, Atom j) + +connect :: Nominal a => a -> (Name, Name) -> a +connect a (i, j) = a `act` (i, Atom i :/\: Atom j) + +leqSystem :: Face -> System a -> Bool +alpha `leqSystem` us = + not $ Map.null $ Map.filterWithKey (\beta _ -> alpha `leq` beta) us + +-- assumes alpha <= shape us +proj :: (Nominal a, Show a) => System a -> Face -> a +proj us alpha | eps `Map.member` usalpha = usalpha ! eps + | otherwise = + error $ "proj: eps not in " ++ show usalpha ++ "\nwhich is the " + ++ show alpha ++ "\nface of " ++ show us + where usalpha = us `face` alpha + +-- actSystemCom :: Formula -> Name -> Formula -> Bool +-- actSystemCom psi i phi = border phi