--- This file contains a semantic interpreter implemented in Haskell.
--- The semantic interpreter implements a denotational (compositional) semantics
--- designed with continuations for a simple language Lmc embodying important features
--- encountered in membrane computing:
--- - the semantics of parallel composition is based on the concept of maximal parallelism
--- and computations are specified by means of multiset rewriting rules
--- - multisets of objects are encapsulated in hierarchical structures of
--- compartments delimited by membranes
--- - the language also provides primitives for parallel communication of objects across
--- membranes and a primitive for membrane creation.
---
--- The denotational semantics is described in the paper:
---
--- "Continuation-Passing Semantics for Membrane Systems"
--- Authors: Gabriel Ciobanu, Eneia Nicolae Todoran
--- Submitted to CMC 2016
---
--- The function 'sem' implements the denotational semantics of Lmc statements
--- The function 'den' implements the semantics of Lmc programs
---
--- This file contains a couple of Lmc test programs.
--- Example 'prg0' is given and explained in the paper
--- The semantic interpreter can be tested as follows:
---
--- Main> den prg0
--- ...
--- (Main> is the GHC prompt)
---------------- Syntax of Lmc ----------------
type O = String -- Objects
type W = [O] -- Multisets of objects
type Mname = String
data X = Obj O | Out O | In O -- Statements
| New Mname Y | Par X X deriving (Eq,Show)
data Y = ObjY O | ParY Y Y deriving (Eq,Show)
type R = [(W,X)] -- Rewriting rules
type MD = (Mname,R)
type MDs = [MD]
type Prg = (MDs,X) -- Lmc programs
-------------- Semantics ---------------
-- Labels
type L = Int
nu :: [L] -> L
nu [] = 0
nu ls = 1+ maximum ls
-- Membranes
data Mb = Mb Mname L W [Mb]
-- Final domain = powerdomain of observables
data Q = Q Mb Q | Epsilon deriving Eq
type P = [Q]
ned :: P -> P -> P
ned p1 p2 =
[ q | q <- p1 `union` p2, q /= Epsilon ] `union`
[ Epsilon | Epsilon <- p1 `intersect` p2 ]
bigned :: [P] -> P
bigned [] = [Epsilon]
bigned (p:ps) = p `ned` (bigned ps)
prefix :: Mb -> P -> P
prefix mu p = [ Q mu q | q <- p ]
-- Domain of actions
type A = Mb -> [Mb]
data T = T0 | Ta A | Tpref A T | Tpar T T -- Actions
semt :: T -> A
semt T0 = \mu -> [mu]
semt (Ta a) = a
semt (Tpref a T0) = a
semt (Tpref a t) = \mu -> bigunion [ semt t mu' | mu' <- a mu ]
semt (Tpar t1 T0) = (semt t1)
semt (Tpar T0 t2) = (semt t2)
semt (Tpar t1 t2) = (semt t1) `part` (semt t2)
part :: A -> A -> A -- (Mb -> [Mb]) -> (Mb -> [Mb]) -> (Mb -> [Mb])
part a1 a2 =
\mu -> ([ mu2 | mu1 <- a1 mu, mu2 <- a2 mu1 ] `union`
[ mu1 | mu2 <- a2 mu, mu1 <- a1 mu2 ])
-- Denotations and continuations
type D = K -> [L] -> Mb -> P -- Denotations
---type F = L -> Mb -> P -- Final semantic domain
type K = (T,T) -> [L] -> Mb -> P -- Continuations
-- Denotational mappings
sem :: X -> L -> D
sem (Obj o) l = \k -> k (Ta (\mu -> [add o l mu]),T0)
sem (In o) l = \k -> k (Ta (\mu -> inl o l mu),T0)
sem (Out o) l = \k -> k (Ta (\mu -> [out o l mu]),T0)
sem (New m y) l = \k ls ->
let lnew = nu ls
ls' = [lnew] `union` ls
in semy y lnew (\(t1,t2) -> k (T0,Tpref (\mu -> [newM m lnew l mu]) (Tpar t1 t2))) ls'
sem (Par x1 x2) l = (sem x1 l) `par` (sem x2 l)
semy :: Y -> L -> D
semy (ObjY o) l = \k -> k (Ta (\mu -> [add o l mu]),T0)
semy (ParY y1 y2) l = (semy y1 l) `par` (semy y2 l)
add :: O -> L -> Mb -> Mb
add o l (Mb m l' w mus) =
if (l'==l) then (Mb m l (o:w) mus)
else (Mb m l' w [ add o l mu | mu <- mus ])
inl :: O -> L -> Mb -> [Mb]
inl o l (Mb m lm w []) = if (l==lm) then [Mb m lm (o:w) []] else [Mb m lm w []]
inl o l (Mb m lm w mus) =
if (lm==l) then [ Mb m lm w (Mb mi li (o:wi) musi:mus') | (Mb mi li wi musi,mus') <- ms mus ]
else [ Mb m lm w mus' | mus' <- prod [ inl o l mu | mu <- mus ]]
ms :: [a ] -> [(a,[a])]
ms xs = aux xs []
where aux [] ys = []
aux (x : xs) ys = (x , xs ++ ys) : aux xs (x : ys)
out :: O -> L -> Mb -> Mb
out o l (Mb m lm w mus) =
if (lm==l0) then Mb m lm (o:w) mus -- cannot exit out of skin membrane
else aux o l (Mb m lm w mus)
where aux :: O -> L -> Mb -> Mb
aux o l (Mb m lm w mus) =
case [ lm | Mb _ lm _ _ <- mus, lm == l ] of
[] -> Mb m lm w [ aux o l mu | mu <- mus ]
_ -> Mb m lm (o:w) mus
par :: D -> D -> D
par d1 d2 = \k -> d1 (\(t1,t2) -> d2 (\(t1',t2') -> k (Tpar t1 t1',Tpar t2 t2')))
newM :: Mname -> L -> L -> Mb -> Mb
newM mnew lnew l (Mb m l' w mus) =
if (l' == l) then (Mb m l' w (Mb mnew lnew [] []:mus))
else (Mb m l' w [ newM mnew lnew l mu | mu <- mus])
-- Initial continuation definition as fixed point of a higher order mapping
fix :: (a -> a) -> a
fix f = f (fix f)
psi :: MDs -> K -> K
psi mds k (t1,t2) ls mu =
bigned [ prefix mu2 (if (haltMb mu2 mds) then [Epsilon] else ((d k) ls mu2'))
| mu1 <- semt t1 mu, mu2 <- semt t2 mu1, (d,mu2') <- (sched mu2 mds)]
bigpar :: [D] -> D
bigpar [d] = d
bigpar (d:ds) = d `par` (bigpar ds)
--- Scheduler mapping
sched :: Mb -> MDs -> [(D,Mb)]
sched (Mb m l w []) mds =
[ (bigpar ([ sem x l | (_,x) <- rs'] ++
[ sem (Obj o) l | o <- w' ]),Mb m l [] [])
| (rs',w') <- appRules w (rules mds m) ]
sched (Mb m l w mus) mds =
[ (bigpar ([ sem x l | (_,x) <- rs'] ++
[ sem (Obj o) l | o <- w' ] ++
[ d' | (d',_) <- dmus' ]),
Mb m l [] [ mu' | (_,mu') <- dmus' ])
| (rs',w') <- appRules w (rules mds m),
dmus' <- prod [ sched mu mds | mu <- mus ]]
prod :: [[a]] -> [[a]]
prod [xs] = [[x] | x <- xs ]
prod (xs:xss) = [ x : tup | x <- xs, tup <- prod xss ]
rules :: MDs -> Mname -> R
rules [(m',rs)] m = if (m'==m) then rs else []
rules ((m',rs):mds) m = if (m'==m) then rs else rules mds m
-- data Mb = Mb Mname L W [Mb]
appRules :: W -> R -> [(R,W)]
appRules [] r = [([],[])]
appRules w r =
case aux w r of
[] -> [([],w)]
rws -> [ (rule:r',w'')
| (rule,w') <- rws, (r',w'') <- appRules w' r ]
where aux :: W -> R -> [((W,X),W)]
aux w [] = []
aux w ((w',x'):r) =
if (subms w' w) then ((w',x'),difms w w') : aux w r
else aux w r
--- Predicates for halting configurations
haltMb :: Mb -> MDs -> Bool
haltMb (Mb m l w mus) mds =
(haltM m mds w) && (and [ haltMb mu mds | mu <- mus ])
haltM :: Mname -> MDs -> W -> Bool
haltM m mds w =
case appRules w (rules mds m) of
[([],w)] -> True
_ -> False
den :: Prg -> P
den (mds,x) =
let
m0 :: Mname
m0 = fst (head mds)
mu0 :: Mb
mu0 = Mb m0 l0 [] []
k0 :: K
k0 = fix (psi mds)
ls0 = [l0]
in sem x l0 k0 ls0 mu0
l0 :: L
l0 = nu [] -- Skin membrane label
prg0 :: Prg
prg0 = (ds0,Par (Obj "o1") (Obj "o4"))
ds0 :: MDs
ds0 = [("M0",[(["o1","o4"],Par (Obj "o2") (Obj "o4")),(["o2"],(Par (In "o5") (New "M1" (ParY (ObjY "o1") (ObjY "o5"))))),
(["o2"],Obj "o4"),(["o5"],In "o4"),(["o3"],In "o5")]),
("M1",[(["o1"],Par (Obj "o2") (Out "o3")),(["o2"],Obj "o3")])]
prg1 :: Prg
prg1 = (ds1,Par (Obj "o1") (Obj "o3"))
ds1 :: MDs
ds1 = [("M0",[(["o1","o3"],Par (Obj "o2") (Obj "o4")),(["o2"],
Par (New "M1" (ParY (ObjY "o1") (ObjY "o5"))) (New "M1" (ParY (ObjY "o1") (ObjY "o5")))),
(["o2"],In "o4"),(["o2"],Obj "o5")]),
("M1",[(["o1"],Obj "o2"),(["o2"],(Out "o3"))])]
--- Auxiliary operators
-- (subms xs ys) = xs is a submultiset o ys ?
subms :: Eq a => [a] -> [a] -> Bool
subms [] ys = True
subms (x : xs) ys =
if (elem x ys) then subms xs (remems x ys)
else False
-- (remems x xs) removes one occurence of an element (x) in a multiset (xs)
remems :: Eq a => a -> [a] -> [a]
remems _ [] = []
remems x (x' : xs) =
if x == x' then xs
else x' : remems x xs
-- (difms xs ys) computes multiset difference between xs and ys
difms :: Eq a => [a] -> [a] -> [a]
difms xs [] = xs
difms xs (x':xs') =
if (elem x' xs) then difms (remems x' xs) xs'
else difms xs xs'
eqms :: Eq a => [a] -> [a] -> Bool
eqms [] [] = True
eqms [] _ = False
eqms _ [] = False
eqms (x:xs) xs' =
if (x `elem` xs') then eqms xs (remems x xs') else False
union :: Eq a => [a] -> [a] -> [a]
union [] ys = ys
union (x : xs) ys =
if (x `elem` ys) then union xs ys else x : union xs ys
bigunion :: Eq a => [[a]] -> [a]
bigunion [] = []
bigunion (x : xs) = x `union` (bigunion xs)
intersect :: Eq a => [a] -> [a] -> [a]
intersect [] ys = []
intersect (x:xs) ys = if (x `elem` ys) then x : intersect xs ys else intersect xs ys
instance Show Mb where
show (Mb m l w []) =
"<" ++ (show m) ++ "," ++ (show l) ++ "|" ++ (show w) ++
";" ++ ">"
show (Mb m l w mus) =
"<" ++ (show m) ++ "," ++ (show l) ++ "|" ++ (show w) ++
";" ++ (showmus mus) ++ ">"
showmus :: [Mb] -> String
showmus [] = ""
showmus [mu] = (show mu)
showmus (mu:mus) = (show mu) ++ "," ++ (showmus mus)
instance Eq Mb where
(Mb m1 l1 w1 mus1) == (Mb m2 l2 w2 mus2) =
(m1 == m2) && (l1 == l2) && (eqms w1 w2) && (eqms mus1 mus2)
instance Show Q where
show Epsilon = "\n\n[]"
show q = "\n\n[" ++ (showQ q) ++ "]"
showQ :: Q -> String
showQ (Q mu Epsilon) = show mu
showQ (Q mu q) = (show mu) ++ " . " ++ (showQ q)