--- This file contains a semantic interpreter implemented in Haskell.
--- It implements a denotational semantics of a process algebra language for DNA computing
---
--- The denotational semantics is described in the paper:
---
--- "Experiments with continuation semantics for DNA computing"
--- Submitted to IEEE ICCP 2013
---
--- The function 'sem' implements the denotational semantics
--- The interpreter can be tested by using function 'den'
---
--- The example Ldna programs 'ex1', 'ex2', 'ex3' are explained in the paper
--- and can be tested as follows:
---
--- Main> den ex1
--- ...
--- Main> den ex3
--- ...
--- (Main> is the GHC prompt)
----- Syntax of Ldna
type X = String
type G = ([X],[X])
data Z = Zero | X X | G G | Par Z Z | Star Z | ParK Z Int
----- Semantic domains
type P = [Q]
data Q = Q M Q | Epsilon deriving Eq
type Den = F -> W -> P
data D = D0 | D M Den
type F = K -> W -> P
type K = D
data A = Ax X | Ag G | Astar [A] deriving Eq
type M = [A]
data W = Null | Sync G [X]
----- General fixed point operator
fix :: (a -> a) -> a
fix f = f (fix f)
----- Operations on sets
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
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
----- Operations on multisets
summs :: Eq a => [a] -> [a] -> [a]
summs w1 w2 = w1 ++ w2
subms :: Eq a => [a] -> [a] -> Bool
subms [] [] = True
subms [] _ = True
subms _ [] = False
subms (a:as) as' =
if (a `elem` as') then subms as (remove a as') else False
eqms :: Eq a => [a] -> [a] -> Bool
eqms [] [] = True
eqms [] _ = False
eqms _ [] = False
eqms (a:as) as' =
if (a `elem` as') then eqms as (remove a as') else False
remove :: Eq a => a -> [a] -> [a]
remove a [] = []
remove a (a':as) = if (a == a') then as else a' : remove a as
----- Operations on final domain P
ned :: P -> P -> P
ned p1 p2 =
[ q | q <- p1 `union` p2, q /= Epsilon ] `union`
[ Epsilon | Epsilon <- p1 `intersect` p2 ]
prefix :: M -> P -> P
prefix m p = [ Q m q | q <- p ]
try :: Bool -> P -> P
try True g = g
try False g = [Epsilon]
----- Auxiliary operators on W
lt :: W -> W -> Bool
lt (Sync g1 xs1) Null = (mu (Sync g1 xs1))
lt (Sync g1 xs1) (Sync g2 xs2) = (mu (Sync g1 xs1)) &&
(g2 == g1) && (not (eqms xs2 xs1)) && (subms xs2 xs1)
lt _ _ = False
zlt :: W -> W -> Bool
zlt w1 w = (lt w1 w) && (not (sigma w1))
mu :: W -> Bool
mu Null = True
mu (Sync (xs,ys) xs') = subms xs' xs
sigma :: W -> Bool
sigma Null = False
sigma (Sync (xs,ys) xs') = eqms xs' xs
----- Semantic operators
psi :: ((D,D) -> D) -> ((D,D) -> D)
psi op (D0,D0) = D0
psi op (D0,D m2 d2) = D m2 d2
psi op (D m1 d1,D0) = D m1 d1
psi op (D m1 d1,D m2 d2) =
D (summs m1 m2)
(\f w ->
try (mu w)
(d1 (\k1 w1 ->
try (lt w1 w) (f (op (k1,D m2 d2)) w1) `ned`
try (zlt w1 w) (d2 (\k2 -> f (op (k1,k2))) w1)) w) `ned`
try (mu w)
(d2 (\k2 w2 ->
try (lt w2 w) (f (op (k2,D m1 d1)) w2) `ned`
try (zlt w2 w) (d1 (\k1 -> f (op (k2,k1))) w2)) w)
)
par = fix psi
bigPar :: [D] -> D
bigPar [] = D0
bigPar (d : k) = par (d,bigPar k)
-- Initial continuation
phi :: F -> F
phi f k w =
if (not (sigma w)) then [Epsilon]
else let Sync (xs,ys) xs' = w
in (case bigPar (k : [ semX y | y <- ys ]) of
D0 -> [Q [] Epsilon]
D m d -> prefix m (d f Null))
f0 :: F
f0 = fix phi
-- Operator for unbounded populations
omega :: M -> Den -> Den -> Den
omega m2 d1 d2 f w =
try (mu w)
(d1 (\k1 w1 ->
try (lt w1 w) (f (par (k1,D m2 d2)) w1) `ned`
try (zlt w1 w) (omega m2 d1 d2 (\k2 -> f (par (k1,k2))) w1)) w)
----- Denotational semantics
semX :: X -> D
semX x = D [Ax x] (\f w -> case w of
Null -> [Epsilon]
Sync g xs -> let w1 = Sync g (summs [x] xs) in try (mu w1) (f D0 w1))
semG :: G -> D
semG g = D [Ag g] (\f w -> case w of
Null -> f D0 (Sync g [])
_ -> [Epsilon])
sem :: Z -> D
sem Zero = D0
sem (X x) = semX x
sem (G g) = semG g
sem (ParK z n) = bigPar (replicate n (sem z))
sem (Star z) = case sem z of
D0 -> D0
D m d -> D [Astar m] (fix (omega [Astar m] d))
sem (Par z1 z2) = par (sem z1,sem z2)
----- Test function
data ShowD = ShowD0 | ShowD P deriving Eq
instance Show ShowD where
show ShowD0 = "D0"
show (ShowD p) = show p
den :: Z -> ShowD
den z = case sem z of
D0 -> ShowD0
D _ d -> ShowD (d f0 Null)
----- Test programs
ex1,ex2 :: Z
ex1 = Par (Par (X "x1") (G (["x1"],["y1"]))) (Par (X "x2") (G (["x2"],["y2"])))
ex2 = Par (X "x") (Par (G (["x1","x2"],["x3"])) (G (["x"],["x1","x2"])))
ex3 :: Z
ex3 = Par (Par (X "y") (Star (G (["y","x1"],["x2","y"])))) (ParK (X "x1") 3)
----- Further test programs
exa :: Z
exa = Par (Par (X "x") (Par (G (["x","x1"],["x2","x"]))
(G (["x","x1"],["x2","x"]))))
(Par (X "x1") (X "x1"))
----- Show instances
instance Show Q where
show Epsilon = "\n[]"
show q = "\n\n" ++ (showQ q) ++ ""
showQ :: Q -> String
showQ (Q m Epsilon) = show m
showQ (Q m q) = (show m) ++ " . " ++ (showQ q)
instance Show A where
show (Ax x) = x
show (Ag g) = show g
show (Astar m) = "(" ++ (show m) ++ ")*"