-- | This file contains a semantic interpreter implemented in Haskell.
-- | It implements a denotational semantics of a language Ldna similar
-- | to a process algebra for DNA computing introduced by Cardelli.
-- |
-- | The denotational semantics of Ldna is described in the paper:
-- |
-- | "Continuation-Passing Semantics for Concurrency"
-- | Authors: Eneia Nicolae Todoran, Nikolaos Papaspyrou
-- | Under consideration for publication in Fundamenta Informaticae (FI)
-- |
-- | The function 'sem' implements the denotational semantics given
-- | in Section 6 of the paper.
-- | The interpreter can be tested by using function 'run'
-- | which takes as parameter an Ldna component.
-- |
-- | Examples p and p' are simple Ldna programs explained in the paper.
-- |
-- | Ldna programs can be tested as in the following example:
-- |
-- | Main> run p
-- | ...
-- | (Main> is the GHC prompt)
-- |
-- | Remark: In this implementation we avoided using various specific Haskell
-- | tools and library functions. Had we have done this, the implementation
-- | would have been shorter, but the connection with our FI submission
-- | would have been less obvious to a non Haskell-expert reader
-- = Syntax of Ldna
type X = String -- ^ Signals
type G = ([X], [X]) -- ^ Gates
data A = X X -- ^ Signal
| G G -- ^ Gate
data P = Zero -- ^ Inert component
| A A -- ^ Elementary components
| Star Int P -- ^ Finite population
| Par P P -- ^ Parallel composition
-- | Set of actions and semantics of interaction
type Asem = A
i :: A -> Asem
i a = a
-- | Interaction effect (/ observable)
data Interact = Obs G | Fail
interactf :: W -> Interact
interactf [] = Fail
interactf w =
case ([x | X x <- w], [g | G g <- w]) of
(xs', [(xs, ys)]) -> if xs' `eqms` xs then Obs (xs, ys) else Fail
_ -> Fail
-- | Final semantic domain
type R = [Q]
-- | Sequences of observables
data Q = Epsilon | Q G Q
deriving Eq
prefixr :: G -> R -> R
prefixr g p = [ Q g q | q <- p ]
-- | Semantic domain
type D = F -> R -- ^ Denotations
type F = (W, K) -> R -- ^ Synchronous continuations
data K = K0 | K D -- ^ Asynchronous continuations
-- | Interaction multisets
type W = [Asem]
-- | Denotational semantics
sem :: P -> K
sem Zero = K0
sem (A a) = K (sema a)
sem (Star n p) = star n (sem p)
sem (Par p1 p2) = sem p1 `park` sem p2
sema :: A -> D
sema a = \f -> f ([i a], K0)
star :: Int -> K -> K
star 0 k = K0
star n k = k `park` star (n-1) k
psi :: F -> F
psi f (w, K0) =
case interactf w of
Fail -> [Epsilon]
Obs (xs, []) -> [Q (xs, []) Epsilon]
Obs (xs, ys) -> prefixr (xs, ys) (bigpard [sema (X y) | y <- ys] f)
psi f (w, K d) =
case interactf w of
Fail -> [Epsilon]
Obs (xs, []) -> prefixr (xs, []) (d f0)
Obs (xs, ys) -> prefixr (xs, ys) ((d `pard` bigpard [sema (X y) | y <- ys]) f)
f0 :: F
f0 = fix psi
den :: P -> R
den p = case sem p of
K0 -> []
K d -> d f0
-- | Nondeterministic choice operator (oplus)
nedr :: R -> R -> R
nedr p1 p2 = [q | q <- p1 `union` p2, q /= Epsilon] `union`
[Epsilon | Epsilon <- p1 `intersect` p2]
bignedr :: [R] -> R
bignedr [] = [Epsilon]
bignedr (p : ps) = p `nedr` bignedr ps
-- | Semantic operators
omegaseq :: (D -> D -> D) -> (D -> D -> D)
omegaseq omega d1 d2 =
\f -> d1 (\(w1, k1) -> f (w1, lift omega k1 (K d2)))
omegalsyn :: (D -> D -> D) -> (D -> D -> D)
omegalsyn omega d1 d2 =
\f -> d1 (\(w1, k1) -> d2 (\(w2, k2) -> f (summs w1 w2, lift omega k1 k2)))
omegasyn :: (D -> D -> D) -> (D -> D -> D)
omegasyn omega d1 d2 =
\f -> bignedr [omegalsyn omega d1 d2 f, omegalsyn omega d2 d1 f]
omegapar :: (D -> D -> D) -> (D -> D -> D)
omegapar omega d1 d2 =
\f -> bignedr [lpard d1 d2 f, lpard d2 d1 f, synd d1 d2 f]
pard :: D -> D -> D
pard = fix omegapar
bigpard :: [D] -> D
bigpard [d] = d
bigpard (d : ds) = d `pard` bigpard ds
park :: K -> K -> K
park = lift pard
lpard :: D -> D -> D
lpard = omegaseq pard
lsynd :: D -> D -> D
lsynd = omegalsyn pard
synd :: D -> D -> D
synd = omegasyn pard
lift :: (D -> D -> D) -> (K -> K -> K)
lift omega K0 K0 = K0
lift omega K0 (K d) = K d
lift omega (K d) K0 = K d
lift omega (K d1) (K d2) = K (omega d1 d2)
-- = Auxiliary functions
-- | Fixed point operator
fix :: (a -> a) -> a
fix f = f (fix f)
-- | Multiset summation
summs :: [a] -> [a] -> [a]
summs w1 w2 = w1 ++ w2
-- | Equality test
eqms :: Eq a => [a] -> [a] -> Bool
eqms [] [] = True
eqms [] _ = False
eqms _ [] = False
eqms (x:xs) ys = if elem x ys then eqms xs (elimOnce x ys) else False
where elimOnce :: (Eq a) => a -> [a] -> [a]
elimOnce x [] = []
elimOnce x (y : ys) = if x==y then ys else y : elimOnce x ys
-- | Set union
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
-- | Set intersection
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
-- | Show instances
instance Show Q where
showsPrec p Epsilon = ("\n\n[]" ++)
showsPrec p (Q g q) = ("\n\n[" ++) . aux (Q g q) . ("]" ++)
where aux (Q g Epsilon) = showsPrec 0 g
aux (Q g q) = showsPrec 0 g . ("," ++) . aux q
-- = Test examples
p :: P
p = Par (Par (A (X "x"))
(Star 3 (A (G (["x", "x1"], ["x2", "x"])))))
(Star 3 (A (X "x1")))
p' :: P
p' = Par (Par (A (X "x1"))
(A (G (["x1"], ["x1'"]))))
(Par (A (X "x2"))
(A (G (["x2"], ["x2'"]))))
p0 :: P
p0 = Zero
p0' :: P
p0' = Star 3 Zero
p1 :: P
p1 = Par (Par (A (X "x"))
(A (G (["x1", "x2"], ["x3"]))))
(A (G (["x"], ["x1", "x2"])))
p2 :: P
p2 = Par (Star 2 (Par (A (X "x"))
(A (G (["x1", "x2"], ["x3"])))))
(Star 2 (A (G (["x"], ["x1", "x2"]))))
-- | Test support function
run :: P -> R
run p = den p
-- | Main program
main = do
print (run p)
print (run p')
print (run p0)
print (run p0')
print (run p1)
print (run p2)