Greg Meredith lgreg.meredith at biosimilarity.com
Tue Apr 24 23:27:18 EDT 2007

```Oleg, Simon,

Thanks for your help. If i understand it correctly, the code below gives a
reasonably clean first cut at a demonstration of process calculi as
polymorphically parametric in the type of name, allowing for an
instantiation of the type in which the quoted processes play the role of
name. This is much, much cleaner and easier to read than the OCaml version.

Best wishes,

--greg

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Core(
Nominal
,Name
,Locality
,Location
,CoreProcessSyntax
,CoreAgentSyntax
,MinimalProcessSyntax
,MinimalAgentSyntax
,ReflectiveProcessSyntax
--           ,make_process
)
where

-- What's in a name?

class Nominal n where
nominate :: i -> n i

-- newtype Name i = Nominate i deriving (Eq, Show)
newtype Name i = Name i deriving (Eq, Show)

instance Nominal Name where nominate i = Name i

-- Where are we?

class Locality a where
locate :: (Eq s, Nominal n) => s -> (n i) -> a s (n i)
name :: (Eq s, Nominal n) => a s (n i) -> (n i)

-- data Location s n = Locate s n deriving (Eq, Show)
data Location s n = Location s n deriving (Eq, Show)

instance Locality Location where
locate s n = Location s n
name (Location s n) = n

-- Constraints

class CoreProcessSyntax p a x | p -> a x where
zero :: p
sequence :: a -> x -> p
compose :: [p] -> p

class CoreAgentSyntax x p n | x -> p n where
bind  :: [n] -> p -> x
offer :: [n] -> p -> x

-- Freedom (as in freely generated)

data MinimalProcessSyntax l x =
Null
| Sequence l x
| Composition [MinimalProcessSyntax l x]

data MinimalAgentSyntax n p =
Thunk (() -> p)
| Abstraction ([n] -> p)
| Concretion [n] p

-- Responsibility : constraining freedom to enjoy order

instance CoreProcessSyntax (MinimalProcessSyntax l x) l x where
zero = Null
sequence l a = Sequence l a
compose [] = zero
compose ps = Composition ps

instance CoreAgentSyntax (MinimalAgentSyntax n p) p n where
bind [] proc = Thunk (\() -> proc)
--      -- TODO : lgm : need to substitute m for name in proc
bind (name:names) proc = Abstraction (\m -> comp \$ bind names proc)
where comp (Thunk fp) = fp ()
-- comp (Abstraction abs) = abs name
offer names proc = Concretion names proc

data ReflectiveProcessSyntax =
Reflect
(MinimalProcessSyntax
(Location [(Name ReflectiveProcessSyntax)] (Name
ReflectiveProcessSyntax))
(MinimalAgentSyntax (Name ReflectiveProcessSyntax)
ReflectiveProcessSyntax))

-- instance (CoreProcessSyntax p a x) =>
--     CoreProcessSyntax
--     (MinimalProcessSyntax
--      (Location
--       [(Name (MinimalProcessSyntax a x))]
--       (Name (MinimalProcessSyntax a x)))
--      (MinimalAgentSyntax
--       (Name (MinimalProcessSyntax a x))
--       (MinimalProcessSyntax a x)))
--     (Location
--       [(Name (MinimalProcessSyntax a x))]
--       (Name (MinimalProcessSyntax a x)))
--     (MinimalAgentSyntax
--       (Name (MinimalProcessSyntax a x))
--       (MinimalProcessSyntax a x))

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103

+1 206.650.3740

http://biosimilarity.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...