-- This file contains a semantic interpreter implemented in Haskell. -- It implements the operational semantics of a language Lsnpmr described in the paper: -- -- "A Semantic Investigation of Spiking Neural P Systems with Mute Rules" -- Authors: Eneia Nicolae Todoran and Gabriel Ciobanu -- Submitted to 28th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2026 (SYNASC 2026) -- -- The function 'osem' implements the operational semantics of Lsnpmr programs. -- -- The variable 'pi1' implements the Lsnpmr program presented in the paper in Example 1 and Example 2. -- The variable 'pi2' implements the Lsnpmr program presented in the paper in the Appendix (Section C). -- -- The semantic interpreter contained in this file is a direct implementation -- of the operational semantics presented in the paper. It is engineered -- to generate all execution traces (irrespective of their number or size), -- hence it can only be used to test (toy) Lsnpmr programs like pi1. -- -- (The Lsnpmr program pi2 also included below is both nondeterministic and nonterminating. -- The Lsnpmr program pi2 can only be tested using the semantic interpreters -- contained in the files Lsnpmr-osem-cps-fin.hs and Lsnpmr-dsem-cps-fin.hs -- which are based on finite execution traces) -- -- The Lsnpmr program 'pi1' can be tested as in the following examples (function 'main' calls 'osem pi1'): -- -- Main> main -- ... -- Main> osem pi1 -- ... -- (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 submission -- would have been less obvious to a non Haskell-expert reader --- Syntax of Lsnpmr type Oset = String -- Spikes (objects) type W = [Oset] -- Multisets of spikes type Nn = String -- Neuron names type Xi = [Nn] -- Sets of neuron names data XiInit = XiInit Xi deriving Eq data ES = Spike Oset | SelectiveSpike Xi Oset | InitSpike Xi -- Elementary statements data Stat = ES ES | Par Stat Stat -- Statements data Rule = Rfire (RE Oset) W Stat -- Spiking rule | Rminus (RE Oset) W -- Mute rule | Rplus (RE Oset) W -- Mute rule type Rs = [Rule] -- Lists of rules type ND = (Nn,Rs,Xi) -- Neuron declarations type Ndecl = [ND] -- Declarations type Prg = (Ndecl,Stat) -- Lsnpmr programs -- Regular expressions data RE a = LambdaRE | ARE a | Concat (RE a) (RE a) | Union (RE a) (RE a) | Plus (RE a) nns :: Ndecl -> Xi nns ndecl = [ nu | (nu,_,_) <- ndecl ] nbs :: Ndecl -> Nn -> Xi nbs [] nu = [] nbs ((nu',rho,alpha):ndecl) nu = if nu'==nu then alpha else nbs ndecl nu rs :: Ndecl -> Nn -> Rs rs [] nu = [] rs ((nu',rho,alpha):ndecl) nu = if nu'==nu then rho else rs ndecl nu data Sigma = Sigma [(Nn,W)] -- Neural states halt :: Ndecl -> Sigma -> Bool halt ndecl (Sigma sigma) = and [ hltN ndecl nu s | (nu,s) <- sigma ] hltN :: Ndecl -> Nn -> W -> Bool hltN ndecl nu w = case rs ndecl nu of [] -> True rho -> and [ not (ar varrho w) | varrho <- rho ] ar :: Rule -> W -> Bool ar (Rfire re wr x) w = and [elemRE w re,wr `subms` w] ar (Rplus re wr) w = elemRE w re ar (Rminus re wr) w = and [elemRE w re,wr `subms` w] type U = [Act] -- Multiset of actions data Act = At Oset Xi -- Actions | AtI Oset XiInit | AtInit XiInit deriving Eq opa :: ES -> Xi -> Act opa (Spike a) alpha = At a alpha opa (SelectiveSpike alpha1 a) alpha = AtI a (XiInit (alpha1 `intersect` alpha)) opa (InitSpike alpha1) alpha = AtInit (XiInit (alpha1 `intersect` alpha)) --- Final semantic domain and operators type P = [Q] data Q = Epsilon | Q Sigma Q deriving Eq prefix :: Sigma -> P -> P prefix b p = [ Q b q | q <- p ] data X = Xk Int | Xa Act | Xpar X X evx :: X -> U evx (Xk k) = error "evx: only defined for expressions without free variables" evx (Xa a) = [a] evx (Xpar x1 x2) = let u1 = evx x1 u2 = evx x2 in u1 `summs` u2 data F = Fs (Stat,Xi) | Fpar F F data Z = Ze | Z F -- | Resumptions, configurations type SeqF = [F] data T = Tx X | Lambda T type Res = (SeqF,T) data Conf = Conf F Res Sigma| E Sigma -- Transition relation tss :: Ndecl -> Conf -> [Sigma] tss ndecl (Conf (Fs (ES e,xi)) ([],t) sigma) = let Tx x = eval t (Xa (opa e xi)) u = evx x sigma1 = initsigma u sigma sigma2 = sndu u sigma1 sigmaobs = sigmaObs ndecl sigma2 in [sigmaobs] tss ndecl (Conf (Fs (ES e,xi)) (f:fs,t) sigma) = tss ndecl (Conf f (fs,eval t (Xa (opa e xi))) sigma) tss ndecl (Conf (Fs (Par s1 s2,xi)) (fs,t) sigma) = (tss ndecl (Conf (Fs (s1,xi)) (Fs (s2,xi):fs,Lambda (Lambda (eval t (Xpar (Xk 1) (Xk 0))))) sigma)) ++ (tss ndecl (Conf (Fs (s2,xi)) (Fs (s1,xi):fs,Lambda (Lambda (eval t (Xpar (Xk 1) (Xk 0))))) sigma)) tss ndecl (Conf (Fpar f1 f2) (fs,t) sigma) = (tss ndecl (Conf f1 (f2:fs,Lambda (Lambda (eval t (Xpar (Xk 1) (Xk 0))))) sigma)) ++ (tss ndecl (Conf f2 (f1:fs,Lambda (Lambda (eval t (Xpar (Xk 1) (Xk 0))))) sigma)) tss ndecl (E sigma) = case schedo ndecl sigma of [] -> [] scheds -> concat ([ tss ndecl (Conf f ([],Lambda (Tx (Xk 0))) sigma') | (f,sigma') <- scheds ]) -- The mapping '(sigmaObs ndecl sigma)' yields a list (an observable) of type 'Sigma' where -- neuron names occur in the same order as in the neural net definition 'ndecl' sigmaObs :: Ndecl -> Sigma -> Sigma sigmaObs ndecl (Sigma sigma) = Sigma [ (nu,w) | nu <- nns ndecl, (nu',w) <- sigma, nu'==nu ] initsigma :: U -> Sigma -> Sigma initsigma u (Sigma sigma) = Sigma (sigma ++ [ (nu,[]) | nu <- alphainit `diffs` alphasigma ]) where alphasigma = [ nu | (nu,w) <- sigma ] alphainit = bigunion [ alpha | (AtI a (XiInit alpha)) <- u ] `union` bigunion [ alpha | (AtInit (XiInit alpha)) <- u ] sndu :: U -> Sigma -> Sigma sndu [] sigma = sigma sndu ((At a alpha):u) sigma = sndf (a,alpha) (sndu u sigma) sndu ((AtI a (XiInit alpha)):u) sigma = sndf (a,alpha) (sndu u sigma) sndu ((AtInit (XiInit alpha)):u) sigma = sndu u sigma sndf :: (Oset,Xi) -> Sigma -> Sigma sndf (a,alpha) (Sigma sigma) = Sigma [ addn (a,alpha) nstate | nstate <- sigma ] addn :: (Oset,Xi) -> (Nn,W) -> (Nn,W) addn (a,alpha) (nu1,w) = if nu1 `elem` alpha then (nu1,[a] `summs` w) else (nu1,w) parz :: Z -> Z -> Z parz Ze d = d parz d Ze = d parz (Z d1) (Z d2) = Z (Fpar d1 d2) bigparz :: [Z] -> Z bigparz [] = Ze bigparz (k:ks) = k `parz` (bigparz ks) schedo :: Ndecl -> Sigma -> [(F,Sigma)] schedo ndecl (Sigma sigma) = if halt ndecl (Sigma sigma) then [] else [ (fo (bigparz [ Z f | (Z f,_) <- scheds ]),Sigma [ (nu,w) | (_,(nu,w)) <- scheds ]) | scheds <- prod [ schedon ndecl nu w | (nu,w) <- sigma ]] where prod :: [[a]] -> [[a]] prod [] = [[]] prod [xs] = [[x] | x <- xs ] prod (xs:xss) = [ x : tup | x <- xs, tup <- prod xss ] schedon :: Ndecl -> Nn -> W -> [(Z,(Nn,W))] schedon ndecl nu w = if hltN ndecl nu w then [(Ze,(nu,w))] else let rho = rs ndecl nu xi = nbs ndecl nu in [ (Z (Fs (s,xi)),(nu,w `diffms` wconsumed)) | Rfire re wconsumed s <- rho, elemRE w re, wconsumed `subms` w ] ++ [ (Ze,(nu,w `summs` wadd)) | Rplus re wadd <- rho, elemRE w re ] ++ [ (Ze,(nu,w `diffms` wconsumed)) | Rminus re wconsumed <- rho, elemRE w re, wconsumed `subms` w ] fo :: Z -> F fo Ze = Fs (ES (InitSpike []),[]) fo (Z f) = f --- Operational semantics of Lsnpmr programs psiN :: Ndecl -> (Conf -> P) -> (Conf -> P) psiN ndecl os conf = if terminates ndecl conf then [Epsilon] else let confs = tss ndecl conf in bigunion [ prefix sigma' (os (E sigma')) | sigma' <- confs ] terminates :: Ndecl -> Conf -> Bool terminates ndecl (E sigma) = halt ndecl sigma terminates ndecl (Conf _ _ _) = False osem :: Prg -> P osem (ndecl,s) = osn (Conf (Fs (s,xi0)) ([],Lambda (Tx (Xk 0))) sigma0) where osn = fix (psiN ndecl) sigma0 = Sigma [("nu0",[])] xi0 = xizero ndecl xizero :: Ndecl -> Xi xizero ((nu0,rho0,xi0):_) = xi0 -- Evaluation operation eval :: T -> X -> T eval (Lambda t) x' = shiftT (-1) (substT 0 (shiftX 1 x') t) substT :: Int -> X -> T -> T substT k x (Lambda t) = Lambda (substT (k+1) (shiftX 1 x) t) substT k x (Tx x1) = Tx (substX k x x1) where substX :: Int -> X -> X -> X substX k x (Xk k') = if k'==k then x else Xk k' substX k x (Xa a) = Xa a substX k x (Xpar x1 x2) = Xpar (substX k x x1) (substX k x x2) shiftT :: Int -> T -> T shiftT d t = shiftTaux d 0 t shiftTaux :: Int -> Int -> T -> T shiftTaux d l (Lambda t) = (Lambda (shiftTaux d (l+1) t)) shiftTaux d l (Tx x) = Tx (shiftXaux d l x) shiftX :: Int -> X -> X shiftX d x = shiftXaux d 0 x shiftXaux :: Int -> Int -> X -> X shiftXaux d l (Xk k) = if k 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 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 diffs :: Eq a => [a] -> [a] -> [a] diffs [] ys = [] diffs (x:xs) ys = if (x `elem` ys) then diffs xs ys else x : diffs xs ys subseteq :: Eq a => [a] -> [a] -> Bool subseteq [] ys = True subseteq (x:xs) ys = (x `elem` ys) && (subseteq xs ys) eqset :: Eq a => [a] -> [a] -> Bool eqset xs ys = and [subseteq xs ys,subseteq ys xs] --- Operators on multisets summs :: Eq a => [a] -> [a] -> [a] summs xs ys = xs ++ 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 :: Eq a => a -> [a] -> [a] remems _ [] = [] remems x (x' : xs) = if x == x' then xs else x' : remems x xs diffms :: Eq a => [a] -> [a] -> [a] diffms xs [] = xs diffms xs (x':xs') = if (elem x' xs) then diffms (remems x' xs) xs' else diffms 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 --- Operations with regular expressions --- 'elemRE' verifies if (any permutation of) a multiset is an element --- of a language associated with a regular expression elemRE :: Eq a => [a] -> (RE a) -> Bool elemRE w re = or [ elemre w' re | w' <- perm w ] where elemre :: Eq a => [a] -> (RE a) -> Bool elemre z LambdaRE = case z of { [] -> True; _ -> False } elemre z (ARE a) = case z of { [a'] -> (a' == a); _ -> False } elemre z (Union re1 re2) = or [ elemre z re1, elemre z re2 ] elemre z (Concat re1 re2) = or [ and [elemre z1 re1,elemre z2 re2] | (z1,z2) <- decompose z ] elemre z (Plus re) = or [ elemre z (ncopies re n) | n <- [1 .. length z] ] decompose :: [a] -> [([a],[a])] decompose [] = [([],[])] decompose (x:xs) = ([],x:xs):([x],xs):[ (x:x':z1',z2) | (x':z1',z2) <- decompose xs ] ncopies :: (RE a) -> Int -> (RE a) ncopies LambdaRE n = LambdaRE ncopies re n = if n<=1 then re else Concat re (ncopies re (n-1)) --- Permutations generator perm :: [a] -> [[a]] perm [] = [[]] perm xs = [ y:zs | (y,ys) <- sel xs, zs <- perm ys ] sel :: [a] -> [(a,[a])] sel [] = [] sel (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- sel xs ] instance Eq Sigma where (Sigma sigma1) == (Sigma sigma2) = sigma1 `eqset` sigma2 --- Show instances instance Show Sigma where show (Sigma sigma) = show sigma instance Show Q where show Epsilon = "\n[]" show q = "\n[" ++ (showQ q) ++ "]" showQ :: Q -> String showQ (Q ns Epsilon) = show ns showQ (Q obs q) = (show obs) ++ " .\n " ++ (showQ q) -- | Test Examples and Main Program pi1 :: Prg pi1 = ([("nu0",[],["nu1","nu2"]), ("nu1",[Rplus (ARE "a") ["a"], Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (Par (ES (Spike "a")) (ES (Spike "a")))],["nu2"]), ("nu2",[Rminus (ARE "a") ["a"],Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (ES (Spike "a"))],["nu0"])], Par (ES (SelectiveSpike ["nu1"] "a")) (Par (ES (SelectiveSpike ["nu2"] "a"))(ES (SelectiveSpike ["nu2"] "a")))) pi2 :: Prg pi2 = ([("nu0",[],["nu1","nu2"]), ("nu1",[Rplus (ARE "a") ["a"],Rfire (Concat (ARE "a") (ARE "a")) ["a"] (ES (Spike "a")), Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (Par (ES (Spike "a")) (ES (Spike "a")))],["nu2"]), ("nu2",[Rminus (ARE "a") ["a"],Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (ES (Spike "a"))],["nu0"])], Par (ES (SelectiveSpike ["nu1"] "a")) (Par (ES (SelectiveSpike ["nu2"] "a"))(ES (SelectiveSpike ["nu2"] "a")))) main = do print (osem pi1)