--- 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
--- It always produces execution traces of finite length
--- The interpreter can be tested by using function 'den' which takes 2 parameters:
--- a Ldna program, and a natural number, indicating the maximum length of the execution traces
---
--- The example Ldna programs 'ex1', 'ex2', 'ex3', 'ex4' are explained in the paper
--- and can be tested as in the following example:
---
--- Main> den ex1 5
--- ...
--- Main> den ex4 3
--- (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 G Q | Epsilon deriving Eq
type Den = F -> W -> Int -> P
data D = D0 | D Den
type F = D -> W -> Int -> P
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 :: G -> P -> P
prefix g p = [ Q g q | q <- p ]
try :: Bool -> (Int -> P) -> (Int -> P)
try True r = r
try False r = \n -> [Epsilon]
nedN :: (Int -> P) -> (Int -> P) -> (Int -> P)
nedN r1 r2 = \n -> (r1 n) `ned` (r2 n)
----- 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
-- Parallel composition
psi :: ((D,D) -> D) -> ((D,D) -> D)
psi op (D0,D0) = D0
psi op (D0,D d) = D d
psi op (D d,D0) = D d
psi op (D d1,D d2) =
D (\f w ->
try (mu w)
(d1 (\k1 w1 ->
try (lt w1 w) (f (op (k1,D d2)) w1) `nedN`
try (zlt w1 w) (d2 (\k2 -> f (op (k1,k2))) w1)) w) `nedN`
try (mu w)
(d2 (\k2 w2 ->
try (lt w2 w) (f (op (k2,D d1)) w2) `nedN`
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 n =
if (n <= 0) then [Epsilon]
else if (not (sigma w)) then [Epsilon]
else let Sync (xs,ys) xs' = w
in case bigPar (k : [ semX y | y <- ys ]) of
D0 -> [Q (xs,ys) Epsilon]
D d -> prefix (xs,ys) (d f Null (n-1))
f0 :: F
f0 = fix phi
-- Operator for unbounded populations
omega :: Den -> Den -> Den
omega d1 d2 f w =
try (mu w)
(d1 (\k1 w1 ->
try (lt w1 w) (f (par (k1,D d2)) w1) `nedN`
try (zlt w1 w) (omega d1 d2 (\k2 -> f (par (k1,k2))) w1)) w)
----- Denotational semantics
semX :: X -> D
semX x = D (\f w -> case w of
Null -> \n -> [Epsilon]
Sync g xs -> let w1 = Sync g (summs [x] xs) in try (mu w1) (f D0 w1))
semG :: G -> D
semG g = D (\f w -> case w of
Null -> f D0 (Sync g [])
_ -> \n -> [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 d -> D (fix (omega d))
sem (Par z1 z2) = par (sem z1,sem z2)
----- Test function
data ShowD = ShowD0 | ShowD P
instance Show ShowD where
show ShowD0 = "D0"
show (ShowD p) = show p
den :: Z -> Int -> ShowD
den z n = case sem z of
D0 -> ShowD0
D d -> ShowD (d f0 Null n)
----- 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)
ex4 :: Z
ex4 = Par (Star (X "x")) (Star (G (["x"],["y"])))
----- 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"))
z1 :: Z
z1 = Par (Par (X "x") (Star (G (["x","x1"],["x2","x"]))))
(Star (X "x1"))
z2 :: Z
z2 = Par (Par (X "y") (Star (G (["y","y1"],["y2","y"]))))
(Star (X "y1"))
exb :: Z
exb = Par z1 z2
exc :: Z
exc = Par exb (Star (G (["x2","y2"],["x","y"])))
exd :: Z
exd = Par exb (Star (Star (G (["x2","y2"],["x","y"]))))
----- Show instances
instance Show Q where
show Epsilon = "\n[]"
show q = "\n" ++ (showQ q) ++ ""
showQ :: Q -> String
showQ (Q g Epsilon) = show g
showQ (Q g q) = (show g) ++ "." ++ (showQ q)