A Type System for Required/Excluded Elements in CLS∗
Mariangiola Dezani-Ciancaglini

Paola Giannini

Dipartimento di Informatica, Università di Torino

Dipartimento di Informatica, Università del Piemonte Orientale

dezani@di.unito.it

giannini@mfn.unipmn.it

Angelo Troina
Dipartimento di Informatica, Università di Torino
troina@di.unito.it

The calculus of looping sequences is a formalism for describing the evolution of biological systems
by means of term rewriting rules. We enrich this calculus with a type discipline to guarantee the
soundness of reduction rules with respect to some biological properties deriving from the requirement
of certain elements, and the repellency of others. As an example, we model a toy system where the
repellency of a certain element is captured by our type system and forbids another element to exit a
compartment.

1

Introduction

While the approach of biologists to describe biological systems by mathematical means, allows them to
reason on the behaviour of the described systems and to perform quantitative simulations, such modelling
starts becoming more difficult both in specification and in analysis when the complexity of the described
systems increases. This has become one of the main motivations for the application of Computer Science
formalisms to the description of biological systems [15]. Other motivations can be found in the fact
that the use of formal means of Computer Science permits the application of analysis methods that are
practically unknown to biologists, such as static analysis and model checking.
Many formalisms have either been applied to or have been inspired from biological systems. The
most notable are automata-based models [1, 11], rewrite systems [9, 13], and process calculi [15, 16,
14, 8]. Models based on automata have the great advantage of allowing the direct use of many verification tools such as model checkers. On the other side, models based on rewrite systems usually allow
describing biological systems with a notation that can be easily understood by biologists. However,
automata-like models and rewrite systems present, in general, problems from the point of view of compositionality. Compositionality allows studying the behaviour of a system componentwise, and is in
general ensured by process calculi, included those commonly used to describe biological systems.
In [5, 6, 12], Milazzo et al. developed a new formalism, called Calculus of Looping Sequences (CLS
for short), for describing biological systems and their evolution. CLS is based on term rewriting with
some features, such as a commutative parallel composition operator, and some semantic means, such as
bisimulations [6, 7], which are common in process calculi. This permits to combine the simplicity of
notation of rewrite systems with the advantage of a form of compositionality.
In chemistry, hydrophobicity is the physical property of a molecule (known as a hydrophobe) that is
repelled from a mass of water. Hydrophobic molecules tend to be non–polar and thus prefer other neutral
molecules and non–polar solvents. Hydrophobic molecules in water often cluster together forming micelles. From the other perspective, water on hydrophobic surfaces will exhibit a high contact angle (thus
∗ This

work was partly funded by the project BioBIT of the Regione Piemonte.

S. Barry Cooper & Vincent Danos (eds.): Fifth Workshop on
Developments in Computational Models—Computational Models From Nature
EPTCS 9, 2009, pp. 38–48, doi:10.4204/EPTCS.9.5

M. Dezani-Ciancaglini, P. Giannini and A. Troina

39

causing, for example, the familiar dew drops on a hydrophobic leaf surface). Examples of hydrophobic molecules include the alkanes, oils, fats, and greasy substances in general. Hydrophobic materials
are used for oil removal from water, the management of oil spills, and chemical separation processes to
remove non-polar from polar compounds. Hydrophobicity is just an example of repellency in Biochemistry. Other well known examples may be found on the behaviour of anions and cations, or at a different
level of abstraction, in the behaviour of the rh antigen for the different blood types.
As a counterpart, there may be elements, in nature, which always require the presence of other
elements (it is difficult to find a lonely atom of oxygen, they always appear in the pair O2 ).
In this paper we bring these aspects at their maximum limit, and, by abstracting away all the phenomena which give rise/arise to/from repellency (and its counterpart), we assume that for each kind of
element of our reality we are able to fix a set of elements which are required by the element for its
existence and a set of elements whose presence is forbidden by the element.
Thus, we enrich CLS with a type discipline which allows to guarantee the soundness of reduction
rules with respect to some relevant properties of biological systems deriving from the required and excluded kinds of elements. The key technical tool we use is to associate to each reduction rule the minimal
set of conditions an instantiation must satisfy in order to assure that applying this rule to a “correct” system we get a “correct” system as well.
To the best of our knowledge [3, 2] are the only papers which study type disciplines for CLS. We generalise the proposal in [2] by focusing on the type disciplines for Present/Required/Excluded elements.

2

The Calculus of Looping Sequences

In this section we recall the Calculus of Looping Sequences (CLS). CLS is essentially based on term
rewriting, hence a CLS model consists of a term and a set of rewrite rules. The term is intended to
represent the structure of the modelled system, and the rewrite rules to represent the events that may
cause the system to evolve.
We start with defining the syntax of terms. We assume a possibly infinite alphabet E of symbols
ranged over by a, b, c, . . ..
Definition 2.1 (Terms) Terms T and sequences S of CLS are given by the following grammar:
T
S

::=
::=

S
ε

(S)L ⌋ T
a
S·S

T |T

where a is a generic element of E , and ε represents the empty sequence. We denote with T the infinite
set of terms, and with S the infinite set of sequences.
In CLS we have a sequencing operator · , a looping operator ( )L , a parallel composition operator
| and a containment operator ⌋ . Sequencing can be used to concatenate elements of the alphabet E .
The empty sequence ε denotes the concatenation of zero symbols. A term can be either a sequence or a
looping sequence (that is the application of the looping operator to a sequence) containing another term,
or the parallel composition of two terms. By definition, looping and containment are always applied
together, hence we can consider them as a single binary operator ( )L ⌋ which applies to one sequence
and one term.
The biological interpretation of the operators is the following: the main entities which occur in
cells are DNA and RNA strands, proteins, membranes, and other macro–molecules. DNA strands (and

A Type System for Required/Excluded Elements in CLS

40

a

c

(i)

a

(ii)

b

Figure 1:
(i) represents (a · b · c)L ;
L
(a · b · c) ⌋ ((d · e)L | f · g).

c
d

e

b

a

f

c

g

(iii)
d

e
b

(ii) represents (a · b · c)L ⌋ (d · e)L ;

(iii) represents

similarly RNA strands) are sequences of nucleic acids, but they can be seen also at a higher level of abstraction as sequences of genes. Proteins are sequence of amino acids which usually have a very complex
three–dimensional structure. In a protein there are usually (relatively) few subsequences, called domains,
which actually are able to interact with other entities by means of chemical reactions. CLS sequences
can model DNA/RNA strands and proteins by describing each gene or each domain with a symbol of
the alphabet. Membranes are closed surfaces, often interspersed with proteins, which may contain something. A closed surface can be modelled by a looping sequence. The elements (or the subsequences) of
the looping sequence may represent the proteins on the membrane, and by the containment operator it
is possible to specify the content of the membrane. Other macro–molecules can be modelled as single
alphabet symbols, or as short sequences. Finally, juxtaposition of entities can be described by the parallel
composition of their representations.
Brackets can be used to indicate the order of application of the operators, and we assume ( )L ⌋ to
have precedence over | . In Figure 1 we show some examples of CLS terms and their visual representation, using (S)L as a short-cut for (S)L ⌋ ε .
In CLS we may have syntactically different terms representing the same structure. We introduce a
structural congruence relation to identify such terms.
Definition 2.2 (Structural Congruence) The structural congruence relations ≡S and ≡T are the least
congruence relations on sequences and on terms, respectively, satisfying the following rules:
S1 · (S2 · S3 ) ≡S (S1 · S2 ) · S3
S · ε ≡S ε · S ≡S S
S1 ≡S S2 implies S1 ≡T S2 and (S1 )L ⌋ T ≡T (S2 )L ⌋ T
T1 | T2 ≡T T2 | T1
T1 | (T2 | T3 ) ≡T (T1 | T2 ) | T3
T | ε ≡T T
(S1 · S2 )L ⌋ T ≡T (S2 · S1 )L ⌋ T
(ε )L ⌋ ε ≡T ε
Rules of the structural congruence state the associativity of · and | , the commutativity of the latter
and the neutral role of ε . Moreover, axiom (S1 · S2 )L ⌋ T ≡T (S2 · S1 )L ⌋ T says that looping sequences can
rotate. In the following, for simplicity, we will use ≡ in place of ≡T .
Rewrite rules will be defined essentially as pairs of terms, with the first term describing the portion
of the system in which the event modelled by the rule may occur, and the second term describing how
that portion of the system changes when the event occurs. In the terms of a rewrite rule we allow the
use of variables. As a consequence, a rule will be applicable to all terms which can be obtained by
properly instantiating its variables. Variables can be of three kinds: two of these are associated with
the two different syntactic categories of terms and sequences, and one is associated with single alphabet
elements. We assume a set of term variables T V ranged over by X ,Y, Z, . . ., a set of sequence variables
S V ranged over by xe, ye,e
z, . . ., and a set of element variables X ranged over by x, y, z, . . .. All these sets

M. Dezani-Ciancaglini, P. Giannini and A. Troina

41

are possibly infinite and pairwise disjoint. We denote by V the set of all variables, V = T V ∪ S V ∪ X ,
and with ρ a generic variable of V . Hence, a pattern is a term that may include variables.
Definition 2.3 (Patterns) Patterns P and sequence patterns SP of CLS are given by the following grammar:
P
::= SP
(SP)L ⌋ P
P|P
X
a
SP · SP
xe
x
SP
::= ε

where a is a generic element of E , and X , xe and x are generic elements of T V , S V and X , respectively.
We denote with P the infinite set of patterns.

We assume the structural congruence relation to be trivially extended to patterns. An instantiation is
a partial function σ : V → T . An instantiation must preserve the kind of variables, thus for X ∈ T V , xe ∈
x) ∈ S and σ (x) ∈ E , respectively. Given P ∈ P, with Pσ we
S V and x ∈ X we have σ (X ) ∈ T , σ (e
denote the term obtained by replacing each occurrence of each variable ρ ∈ V appearing in P with the
corresponding term σ (ρ ). With Σ we denote the set of all the possible instantiations and, given P ∈ P,
with Var(P) we denote the set of variables appearing in P. Now we define rewrite rules.
Definition 2.4 (Rewrite Rules) A rewrite rule is a pair of patterns (P1 , P2 ), denoted with P1 7→ P2 , where
P1 , P2 ∈ P, P1 6≡ ε and such that Var(P2 ) ⊆ Var(P1 ).
A rewrite rule P1 7→ P2 states that a term P1 σ , obtained by instantiating variables in P1 by some
instantiation function σ , can be transformed into the term P2 σ . We define the semantics of CLS as a
transition system, in which states correspond to terms, and transitions correspond to rule applications.
We define the semantics of CLS by resorting to the notion of contexts.
Definition 2.5 (Contexts) Contexts C are defined as:
C|T

C ::= 

T |C

(S)L ⌋C

where T ∈ T and S ∈ S . The context  is called the empty context. We denote with C the infinite set
of contexts.
By definition, every context contains a single hole . Let us assume C,C′ ∈ C . With C[T ] we denote
the term obtained by replacing  with T in C; with C[C′ ] we denote context composition, whose result
is the context obtained by replacing  with C′ in C. The structural equivalence is extended to contexts in
the natural way (i.e. by considering  as a new and unique symbol of the alphabet E ).
Rewrite rules can be applied to terms only if they occur in a legal context. Note that the general
form of rewrite rules does not permit to have sequences as contexts. A rewrite rule introducing a parallel
composition on the right hand side (as a 7→ b | c) applied to an element of a sequence (e.g., m·a·m) would
result into a syntactically incorrect term (in this case m · (b | c) · m). To modify a sequence, a pattern
representing the whole sequence must appear in the rule. For example, rule a·e
x 7→ a | xe can be applied
to any sequence starting with element a, and, hence, the term a·b can be rewritten as a | b, and the term
a·b·c can be rewritten as a | b·c.
The semantics of CLS is defined as follows.
Definition 2.6 (Semantics) Given a finite set of rewrite rules R, the semantics of CLS is the least relation closed with respect to ≡ and satisfying the following rule:
P1 7→ P2 ∈ R

P1 σ 6≡ ε

σ ∈Σ C∈C

C[P1 σ ] −
→ C[P2 σ ]

A Type System for Required/Excluded Elements in CLS

42

As usual we denote with −
→∗ the reflexive and transitive closure of −
→.
Given a set of rewrite rules R, the behaviour of a term T is the tree of terms to which T may reduce.
Thus, a model in CLS is given by a term describing the initial state of the system and by a set of rewrite
rules describing all the events that may occur.

3

A Type Discipline for Required and Excluded Elements

We classify elements in E with basic types. Intuitively, given a molecule represented by an element in
E , we associate to it a type t which specifies the kind of the molecule. We assume a fixed typing Γ for
the elements in E .
For each basic type t we assume to have a pair of sets of basic types (Rt , Et ), where t 6∈ Rt ∪ Et and
Rt ∩ Et = 0,
/ saying that the presence of elements of basic type t requires the presence of elements whose
basic type is in Rt and forbids the presence of elements whose basic type is in Et . We consider only local
properties: elements influence each other if they are either in the same compartment or they contain each
other.
The type system derives the set of types of patterns (and therefore also terms), checking that the
constraints imposed by the required and excluded sets are satisfied. Types are pairs (P, R): where P is the
set of basic types of present elements (at the top level of a pattern), R is the set of basic types of required
elements (that should still be added to the pattern to represent a correct system). The set of excluded
S
elements is implicitly given by EP = t∈P Et .
Types are well formed, and pair of types are compatible, if their constraints on required and excluded
elements are not contradictory; compatible types can be combined.
Definition 3.1 (Auxiliary definitions)
• Well formed types (P, R) and

(P′ , R′ )

• A type (P, R) is well formed if P ∩ EP = P ∩ R = R ∩ EP = 0.
/
are compatible (written (P, R) ⊲⊳ (P′ , R′ )) if

– EP ∩ P′ = EP ∩ R′ = 0,
/ and
/
– EP′ ∩ P = EP′ ∩ R = 0.
• Given two compatible types (P, R) and (P′ , R′ ) we define their conjunction (P, R) ⊔ (P′ , R′ ) by
(P, R) ⊔ (P′ , R′ ) = (P ∪ P′ , (R ∪ R′ ) \ (P ∪ P′ )).
Basis are defined by:
∆ ::= 0/

∆, x : ({t}, Rt )

∆, η : (P, R)

where η denotes a sequence or term variable. A basis ∆ is well formed if all types in the basis are well
formed.
We check the safety of terms, sequences and more generally patterns using the typing rules of Figure
2. It is easy to verify that, if we start from well-formed basis, then in a derivation we produce only wellformed basis and well-formed types. Note that terms and sequences are typable from the empty context.
All the rules are trivial except for the last one which types looping sequences. In this rule we can put a
pattern P inside a looping sequence SP only if all the types required from P are provided by SP. This
is because if P gets inside a compartment (represented by the looping sequence) it cannot interact any
more with the environment.
Given a context we define the possible types of terms that may fill the hole in the context.
Definition 3.2 (Typed Holes) Given a context C, and a well-formed type (P, R), the type (P, R) is OK for
the context C if X : (P, R) ⊢ C[X ] : (P′ , 0)
/ for some P′ .

M. Dezani-Ciancaglini, P. Giannini and A. Troina

∆, ρ : (P, R) ⊢ ρ : (P, R)

∆ ⊢ ε : (0,
/ 0)
/

∆ ⊢ SP : (P, R)

43
a:t∈Γ
∆ ⊢ a : ({t}, Rt )

∆ ⊢ SP′ : (P′ , R′ ) (P, R) ⊲⊳ (P′ , R′ )

∆ ⊢ SP·SP′ : (P, R) ⊔ (P′ , R′ )
∆ ⊢ P : (P, R)

∆ ⊢ P′ : (P′ , R′ ) (P, R) ⊲⊳ (P′ , R′ )

∆ ⊢ P | P′ : (P, R) ⊔ (P′ , R′ )
∆ ⊢ SP : (P, R) ∆ ⊢ P : (P′ , R′ ) (P, R) ⊲⊳ (P′ , R′ ) and R′ ⊆ P
∆ ⊢ (SP)L ⌋ P : (P, R \ P′ )
Figure 2: Typing Rules
The above notion guarantees that filling a context with a term we obtain a correct system (whose type
is well formed and whose requirements are completely satisfied). It is to this kind of terms that we are
interested in applying reduction rules.
Note that there may be more than one type (P, R) such that (P, R) is OK for the context C.
We can classify reduction rules according to the types we can derive for the right hand sides of the
rules.
Definition 3.3 (∆-(P, R)-Reduction Rules) A rule P1 7→ P2 is a ∆-(P, R)-reduction rule if ∆ ⊢ P2 : (P, R).
An instantiation σ agrees with a basis ∆ (notation σ ∈ Σ∆ ) if ρ : (P, R) ∈ ∆ implies ⊢ σ (ρ ) : (P, R).
We can safely apply a rule to a typed term only if the instances of the pattern on the right hand side
of the rule has a type that is OK for the context. More formally:
Definition 3.4 (Typed Semantics) Given a finite set of rewrite rules R, the typed semantics of CLS is
the least relation closed with respect to ≡ and satisfying the following rule:
P1 7→ P2 ∈ R is a ∆-(P, R)-reduction rule
P1 σ 6≡ ε
C∈C
(P, R) is OK for C
σ ∈ Σ∆
C[P1 σ ] =⇒ C[P2 σ ]
As expected, reduction preserves typing, in the sense that the obtained term is still typable, but the new
type can have a different set of present elements, while the set of required elements is always empty.
This choice makes possible typing creation and degradation of elements.
Theorem 3.5 If ⊢ T : (P, 0)
/ and T =⇒ T ′ , then ⊢ T ′ : (P′ , 0)
/ for some P′ .
We can infer the OK relation between types and contexts and which rules are ∆-(P, R)-reduction rules by
using the machinery of principal typing [17]. In this way we can decide the applicability of the reduction
rules for the typed semantics. This is the content of the remaining part of this section.
We convene that for each variable x ∈ X there is an e-type variable ϕx ranging over basic types,
and for each variable η ∈ T V ∪ S V there are two variables φη , ψη (called p-type variable and r-type
variable) ranging over sets of basic types. Moreover we convene that Φ ranges over formal unions and
differences of sets of basic types, e-type variables and p-type variables, and Ψ ranges over formal unions
and differences of sets of basic types and r-type variables.

A Type System for Required/Excluded Elements in CLS

44

⊢ ε : 0;
/ (0,
/ 0);
/ 0/

a:t∈Γ

⊢ x : {x : (ϕx , Ψ)}; (ϕx , Ψ); {Ψ = Rϕx }

⊢ a : 0;
/ (t, Rt ); 0/

⊢ η : {η : (φη , ψη )}; (φη , ψη ); 0/
⊢ SP : Θ; (Φ, Ψ); Ξ

⊢ SP′ : Θ′ ; (Φ′ , Ψ′ ); Ξ′

⊢ SP·SP′ : Θ ∪ Θ′ ; (Φ, Ψ) ⊔ (Φ′ , Ψ′ ); Ξ ∪ Ξ′ ∪ {(Φ, Ψ) ⊲⊳ (Φ′ , Ψ′ )}
⊢ P : Θ; (Φ, Ψ); Ξ

⊢ P′ : Θ′ ; (Φ′ , Ψ′ ); Ξ′

⊢ P | P′ : Θ ∪ Θ′ ; (Φ, Ψ) ⊔ (Φ′ , Ψ′ ); Ξ ∪ Ξ′ ∪ {(Φ, Ψ) ⊲⊳ (Φ′ , Ψ′ )}
⊢ SP : Θ; (Φ, Ψ); Ξ

⊢ P : Θ′ ; (Φ′ , Ψ′ ); Ξ′

⊢ (SP)L ⌋ P : Θ ∪ Θ′ ; (Φ, Ψ \ Φ′ ); Ξ ∪ Ξ′ ∪ {(Φ, Ψ) ⊲⊳ (Φ′ , Ψ′ ), Ψ′ ⊆ Φ}
Figure 3: Inference Rules for Principal Typing
A basis scheme Θ is a mapping from atomic variables to their e-type variables, and from sequence and
term variables to pairs of their p-type variables and r-type variables:
Θ, x : ϕx

Θ ::= 0/

Θ, η : (φη , ψη ).

The rules for inferring principal typing use judgements of the shape:
⊢ P : Θ; (Φ, Ψ); Ξ
where Θ is the principal basis in which P is well formed, (Φ, Ψ) is the principal type of P, and Ξ is the
set of constraints that should be satisfied. Figure 3 gives these inference rules.
Soundness and completeness of our inference rules can be stated as usual. A type mapping maps etype variables to basic types, p-type variables and r-type variables to sets of basic types. A type mapping
m satisfies a set of constraints Ξ if all constraints in m(Ξ) are satisfied.
Theorem 3.6 (Soundness of Type Inference) If
satisfies Ξ, then m(Θ) ⊢ P : (m(Φ), m(Ψ)).

⊢ P : Θ; (Φ, Ψ); Ξ and m is a type mapping which

Theorem 3.7 (Completeness of Type Inference) If ∆ ⊢ P : (P, R), then ⊢ P : Θ; (Φ, Ψ); Ξ for some Θ,
(Φ, Ψ), Ξ and there is a type mapping m that satisfies Ξ and such that ∆ ⊇ m(Θ), P = m(Φ), R = m(Ψ).
We put now our inference rules at work in order to decide applicability of typed reduction rules. We first
characterize by means of principal typing the OK relation and the classification of reduction rules.
Notably for deciding the OK relation it is not necessary to consider the whole context, but only
the part of the context which influences the typing of the hole. The key observation is that the typing
of a term inside two nested looping sequences does not depend on the typing of the terms outside the
outermost looping sequence. We call core of the context this part. More formally:
Definition 3.8 The core of the context C (notation core(C)) is defined by:
• core(C) = C
• core(C) = C2

if
if

C ≡  | T1

or

C ≡ (S1 )L ⌋ ( | T1 ) | T2 ;

C = C1 [C2 ] where C2 ≡ (S2 )L ⌋ ((S1 )L ⌋ ( | T1 ) | T2 ).

M. Dezani-Ciancaglini, P. Giannini and A. Troina

45

Remark that core is always unambiguously defined, since every context can be split in a unique way into
one of the three shapes of the previous definition.
Lemma 3.9 (OK Relation) Let the context C be such that ⊢ C[T ] : (P0 , 0)
/ for some T, P0 . A type (P, R)
is OK for C if and only if the type mapping m defined by
1. m(φX ) = P,
2. m(ψX ) = R,
satisfies the set of constraints
Ξ ∪ {Ψ = 0/ | if φX or ψX occurs in Ψ},
where ⊢ core(C)[X ] : {X : (φX , ψX )}; (Φ, Ψ); Ξ.
It is easy to check that if core(C) ≡ (S2 )L ⌋ ((S1 )L ⌋ ( | T1 ) | T2 ), and ⊢ T1 : (P1 , R1 ), ⊢ S1 : (P′1 , R′1 ), ⊢ T2 :
(P2 , R2 ), ⊢ S2 : (P′2 , R′2 ), then we have to verify the following six constraints:
• (φX , ψX ) ⊲⊳ (P1 , R1 )
• (P′1 , R′1 ) ⊲⊳ ((φX , ψX ) ⊔ (P1 , R1 ))
• ((ψX ∪ R1 ) \ (φX ∪ P1 )) ⊆ P′1
• (P′1 , R′1 \ (φX ∪ P1 )) ⊲⊳ (P2 , R2 )
• (P′2 , R′2 ) ⊲⊳ ((P′1 , R′1 \ (φX ∪ P1 )) ⊔ (P2 , R2 ))
• (((R′1 \ (φX ∪ P1 )) ∪ R2 ) \ (P′1 ∪ P2 )) ⊆ P′2 .
The set of constraints is smaller when the core context has one of the simpler shapes.
Lemma 3.10 (Classification of Reduction Rules) A rule P1 7→ P2 is a ∆-(P, R)-reduction rule if and
only if the type mapping m defined by
1. m(ϕx ) = t if ∆(x) = ({t}, Rt ),
2. m(φη ) = P′ if ∆(η ) = (P′ , R′ ),
3. m(ψη ) = R′ if ∆(η ) = (P′ , R′ ),
satisfies the set of constraints Ξ ∪ {Φ = P, Ψ = R}, where ⊢ P2 : Θ; (Φ, Ψ); Ξ.
The previous two lemmas imply the following theorem which gives the desired result.
Theorem 3.11 (Applicability of Reduction Rules) Let
⊢ P2 : Θ; (Φ, Ψ); Ξ

and

⊢ core(C)[X ] : {X : (φX , ψX )}; (Φ′ , Ψ′ ); Ξ′ .

Then the rule P1 7→ P2 can be applied to the term C[P1 σ ] such that ⊢ C[P1 σ ] : (P, 0)
/ for some P if and
only if the type mapping m defined by
1. m(ϕx ) = t if σ (x) : t ∈ Γ,
2. m(φη ) = P′ if ⊢ σ (η ) : (P′ , R′ ),
3. m(ψη ) = R′ if ⊢ σ (η ) : (P′ , R′ ),
satisfies the set of constraints Ξ ∪ Ξ′ ∪ {Φ = φX , Ψ = ψX } ∪ {Ψ′ = 0/ | if φX or ψX occurs in Ψ′ }.
Note that - after fixing the reduction rules - the sets of constraints for typing the r.h.s. of these rules can
be evaluated once for all. Instead, the sets of constraints for typing the core contexts need to be evaluated
at every application of a reduction rule. Luckily these sets of constraints includes at most six constraints.
The mapping m is immediate from the derivation of a type for P1 σ . Finally, the checking that m satisfies
a set of constraints requires only some substitutions.

A Type System for Required/Excluded Elements in CLS

46

4

Examples

We start showing the properties of our type system by modelling an example of two molecules repelling
each other. As we have seen, one might model repellency in our framework via the set Et .
Namely, if molecule a, of basic type t, is a repellent for molecule b, of basic type t′ (and viceversa),
we will have that Et = {t′ } and Et′ = {t}. Note that this does not mean that a and b cannot be present
in the same term, actually they should just be contained in two different compartments. In fact, the term
T = a | (m)L ⌋ b
/ is typed by the pair ({t, t′′ }, 0)
/ by the
with m of basic type t′′ , where Et′′ = 0/ and Rt = Rt′ = Rt′′ = 0,
′
′′
following derivation, where Γ = {a : t, b : t , m : t }:

a:t∈Γ
⊢ a : ({t}, 0)
/

m : t′′ ∈ Γ

b : t′ ∈ Γ

⊢ m : ({t′′ }, 0)
/

⊢ b : ({t′ }, 0)
/

({t′′ }, 0)
/ ⊲⊳ ({t′ }, 0)
/

⊢ (m)L ⌋ b : ({t′′ }, 0)
/

({t′′ }, 0)
/ ⊲⊳ ({t}, 0)
/

⊢ a | (m)L ⌋ b : ({t, t′′ }, 0)
/
As we can see the term is well typed, since a and b are in two different compartments. The element m
could also be replaced by any sequence which does not repel elements of types t, t′ and whose (well
formed) type is (P, R) where (P, R) ⊲⊳ ({t′ }, 0)
/ and (P, R) ⊲⊳ ({t}, 0),
/ that is P ∩ {t, t′ } = 0/ and R ∩
′
{t, t } = 0.
/ Moreover, if the term is at top level, then R should be 0.
/
Consider now the rule
R1 : (e
x)L ⌋ (X | b) 7→ b | (e
x)L ⌋ X
which moves the element b outside the compartment. Such a rule could not be applied in T cause it
/ is not well formed.
will result in the term a | b | (m)L ⌋ ε , which is not well typed since ({t, t′ , t′′ }, 0)
Indeed, following Definition 3.4, P1 = (e
x)L ⌋ (X | b), P2 = b | (e
x)L ⌋ X , σ (e
x) = m, σ (X ) = ε and C = a | .
Moreover, while C[P1 σ ] is well typed, the same does not hold for C[P2 σ ].
This does not mean the rule R1 can never be applied. In fact, if we consider the term
T ′ = a | (m)L ⌋ b | (m)L ⌋ ε
and we add the rule
R2 : a | (e
x)L ⌋ X 7→ (e
x)L ⌋ (a | X )
we still have that rule R1 cannot be applied to T ′ (same reasons as before). Moreover, if we consider
the context C = (m)L ⌋ ε | , P1 = a | (e
x)L ⌋ X , and P2 = (e
x)L ⌋ (a | X ), that is we try to move a in the
x) = m and σ (X ) = b, and therefore P2 σ
compartment containing b, we cannot apply the rule R2 , since σ (e
is not well typed. However, we can apply rule R2 to T ′ if we consider C = (m)L ⌋ b | , P1 = a | (e
x)L ⌋ X ,
L
x) = m and
and P2 = (e
x) ⌋ (a | X ), that is moving a in the compartment that does not contain b, since σ (e
L
′
′′
′′
σ (X ) = ε , and we have that T ≡ C[P1 σ ] has type ({t, t }, 0)
/ and T = C[P2 σ ] = (m) ⌋ a | (m)L ⌋ b has
′′
type ({t }, 0)
/ - both C[P1 σ ] and C[P2 σ ] are well typed. Now, we can apply rule R1 to T ′′ , bringing b
outside the compartment. The context of the rule application will be C = (m)L ⌋ a |  and the patterns
P1 = (e
x)L ⌋ (X | b), P2 = b | (e
x)L ⌋ X where σ (e
x) = m and σ (X ) = ε . Both C[P1 σ ] and C[P2 σ ] are well
typed and the resulting term will be
T ′′′ = b | (m)L ⌋ a | (m)L ⌋ ε .

M. Dezani-Ciancaglini, P. Giannini and A. Troina

47

We now show an application for the set of required elements in our typing system. The idea is to
model the absorption of a given compound c by a cell. The absorption is promoted by a receptor r which
should be present in the surface of the cell. We can model the effect of the absorption by using a different
symbol (thus a different type) for the compound when it enters the cell, namely c′ . The basic types of
c, r and c′ are, respectively, t, t′ and t′′ . We also assume that Et = Et′ = Et′′ = Rt = Rt′ = 0.
/ The
requirement for t′′ (modelling the type of the compound inside a cell) should be, instead, the presence of
the receptor on the membrane surface. We can model this condition with the set Rt′′ = {t′ }. Thus, with
these basic types, we can model the rule for the absorption of the protein as:
R : c | (e
x)L ⌋ X 7→ (e
x)L ⌋ (X | c′ )
without imposing explicitly the presence of the receptors on the patterns of the rule.
Actually, our type system guarantees that such a rule cannot be applied to the term c | (m)L ⌋ ε , while
it is applicable to the term c | (m · r)L ⌋ ε .
In a sense, the role of the promoter (the receptor) is modelled intrinsically on the type of the compound brought inside the cell; its properties become transparent for the rewrite rules and controlled by
the type system.

5

Conclusions

This paper is a first step toward the application of typing to the safety of system transformations which
model biological phenomena. We focused on disciplines deriving by the requirement/exclusion of certain
elements, and used the type system to describe how repellency could be modelled. We would like
to underline that in nature it is not easy to find elements which completely exclude or require other
elements. Our abstraction, however allows us to deal with a simple qualitative model, and to observe
some basic properties of biological systems. A more detailed analysis, could also deal with quantities.
In this case, typing is useful in modelling quantitative aspects of CLS semantics on the line of [4]. In
particular, in [10], we show how types can be used to model repellency also by quantitative means, that
is slowing down undesired interactions.
As a future work, we plan to investigate type disciplines assuring different properties for CLS and
to apply this approach to other calculi for describing evolution of biological systems, in particular to P
systems.
An interesting application of this model may also abstract from biological phenomena. In a sense,
the composition of a context C with a term T which satisfies C may represent the agreement on a contract
between C and T . Namely, if C satisfies (P, R) and T has type (P, R), then T offers to C, via the elements
in P, everything that is required by C, viceversa, C has to satisfy T ’s request R; modelling, in a sense, the
fact that C and T mutually agree with each other.
Finally, modelling biological phenomena in CLS, especially for biologists, could be made more
intuitive with the use of a graphical interface, that would check most of the syntactical details, so that the
modeller could focus on the conceptual aspects of the formalization.

Acknowledgements. We thank the referees for their helpful comments. The final version of the paper
improved due to their suggestions.

48

A Type System for Required/Excluded Elements in CLS

References
[1] Alur, R., Belta, C., Ivancic, F., Kumar, V., Mintz, M., Pappas, G.J., Rubin, H. and Schug, J. (2001) Hybrid
modelling and simulation of biomolecular networks. Proc. of Hybrid Systems: Computation and Control,
LNCS 2034, Springer, 19-32.
[2] Aman, B., Dezani-Ciancaglini, M. and Troina, A. (2008) Type disciplines for analysing biologically relevant properties. Proc. of Second International Meeting on Membrane Computing and Biologically Inspired
Process Calculi (MeCBIC’08), ENTCS 227, Elsevier, 97-111.
[3] Barbuti, R., Maggiolo-Schettini, A. and Milazzo, P. (2007) Extending the calculus of looping sequences
to model protein interaction at the domain level. Proc. of International Symposium on Bioinformatics
Research and Applications (ISBRA’07), LNBI 4463, Springer, 638-649.
[4] Barbuti, R., Maggiolo-Schettini, A., Milazzo, P., Tiberi, P. and Troina, A. (2008) Stochastic calculus of
looping sequences for the modelling and simulation of cellular pathways.Transactions on Computational
Systems Biology, vol. IX, 86-113.
[5] Barbuti, R., Maggiolo-Schettini, A., Milazzo, P. and Troina, A. (2006) A calculus of looping sequences
for modelling microbiological systems. Fundamenta Informaticae, 72, 21-35.
[6] Barbuti, R., Maggiolo-Schettini, A., Milazzo, P. and Troina, A. (2006) Bisimulation congruences in the
calculus of looping sequences. Proc. of International Colloquium on Theoretical Aspects of Computing
(ICTAC’06), LNCS 4281, Springer, 93-107.
[7] Barbuti, R., Maggiolo-Schettini, A., Milazzo, P., and Troina, A. (2008) Bisimulations in calculi modelling
membranes. Formal Aspects of Computing, 20(4-5), 351-377.
[8] Cardelli, L. (2005) Brane calculi. Interactions of biological membranes. Proc. of Comput. Methods in
Systems Biology (CMSB’04), LNCS 3082, Springer, 257-280.
[9] Danos, V. and Laneve, C. (2004) Formal molecular biology. Theoretical Computer Science, 325, 69-110.
[10] Dezani-Ciancaglini, M., Giannini, P. and Troina, A. (2009) A Type System for a Stochastic CLS. Proc.
of Third International Meeting on Membrane Computing and Biologically Inspired Process Calculi
(MeCBIC’09), EPTCS, to appear.
[11] Matsuno, H., Doi, A., Nagasaki, M. and Miyano, S. (2000) Hybrid Petri net representation of gene regulatory network. Proc. of Pacific Symposium on Biocomputing, World Scientific Press, 341-352.
[12] Milazzo, P. (2007) Qualitative and quantitative formal modelling of biological systems. Ph.D. Thesis,
University of Pisa.
[13] Pǎun, G. (2002) Membrane computing. An introduction. Springer, 2002.
[14] Regev, A., Panina, E. M., Silverman, W., Cardelli, L. and Shapiro, E. (2004) BioAmbients: an abstraction
for biological compartments. Theoretical Computer Science, 325, 141-167.
[15] Regev, A. and Shapiro, E. (2002) Cells as computation. Nature, 419, 343.
[16] Regev, A. and Shapiro, E. (2004) The π -calculus as an abstraction for biomolecular systems. Modelling
in Molecular Biology, Natural Computing Series, Springer, 219-266.
[17] Wells, J. (2002). The essence of principal typings. Proc. of 29th International Colloquium on Automata,
Languages and Programming (ICALP’02), LNCS 2380, Springer, 913-925.

