<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Type disciplines for systems biology</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Livio Bioglio</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>INSERM, UMR-S 1136, iPLESP</institution>
          ,
          <addr-line>Paris</addr-line>
          ,
          <country country="FR">France</country>
        </aff>
      </contrib-group>
      <fpage>11</fpage>
      <lpage>13</lpage>
      <abstract>
        <p>Systems Biology is a discipline that aims to study complex biological systems by means of computational models. Because of the complexity of biological behaviors, the formalisms used in this field are usually designed ad-hoc for the biological topic of interest, or they need to be tuned by a long set of evolution rules. Here we present a different approach: we define biological properties through a type discipline, leaving the formalisms as general as possible. We explore three different kinds of Type Systems: a static one, that limits the model that can be written by modelers; a dynamic one, that limits the evolution of the model at run-time; and an hybrid combination of the previous ones.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Dynamic type system</title>
      <p>
        In Biology and Chemistry there can be found several examples of repellency, such
as hydrophobicity (the physical property of a molecule that is repelled from a
mass of water), the behavior of anions and cations, or, at a different level of
abstraction, the behavior 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: for example, it is difficult to find a lonely atom of oxygen,
they always appear in the pair O2. 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.
We enrich the basic CLS with a type discipline which guarantees 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. We also propose a type inference
algorithm, based on the machinery of principal typing [
        <xref ref-type="bibr" rid="ref8">8</xref>
        ], and show its soundness and
completeness. The required/excluded elements properties modeled here assure,
through type inference, that only compatible elements are combined together in
the different environments of the biological system took in consideration. Thus
the type system intrinsically yields a notion of correct (well-behaving) system
according to the expressed requirements. The detailed Type Discipline can be
found in [
        <xref ref-type="bibr" rid="ref5">5</xref>
        ].
      </p>
      <p>
        There are cases in which the request/repellency model cannot reflect the
behavior of a biological system. An example is homeostasis, the property of a system
that regulates its internal environment and tends to maintain stable conditions
that are optimal for survival: when this equilibrium is disturbed, built-in
regulatory devices respond in order to restore the balance. Different living organisms
employ homeostatic mechanisms to maintain some conditions in specific ranges:
the human body, like in all the warm-blooded animals, maintain a near-constant
body temperature using mechanisms such as vasodilation and vasoconstriction;
microorganisms maintain the iron presence above a minimum level to maintain
life but up to a maximum level to avoid iron toxicity. For this reason, we
propose an extension of the previous Type Disciplines, where we assume that for
each element of our system we can fix the minimum and the maximum number
of other elements it requires. We enrich CLS with a type discipline and typed
reductions that guarantee the soundness of reduction rules with respect to the
properties of biological systems deriving from the minimum and the maximum
requested numbers of elements, and a type inference algorithm for inferring the
type of rewriting rules. Our contribution appeared in [
        <xref ref-type="bibr" rid="ref3">3</xref>
        ].
3
      </p>
    </sec>
    <sec id="sec-2">
      <title>Hybrid type system</title>
      <p>
        We present the variant of the Calculus of Looping Sequences with global and
local rewrite rules (CLSLR, for short). Global rules are the usual rules of CLS,
and they can be applied anywhere in a given term wherever their patterns match
the portion of the system under investigation, while local rules can only be
applied in the compartment in which they are defined. Terms written in CLSLR
are thus syntactically extended to contain explicit local rules within the term,
on different compartments. Local rules can be created, moved between different
compartments and deleted. Having a calculus in which we can model the dynamic
evolution of the rules describing the system allows to study emerging properties
of complex systems in a more natural and direct way. As it happens in nature,
where data and programs are encoded in the same kind of molecular structures,
we insert rewrite rules within the terms modeling the system under investigation.
On the other hand, some rule may represent general behaviors, common to the
whole system: global rules are used for avoiding the repetition of such rules in
each compartment. Since in this framework the focus is put on local rules, we
define a set of features that can be associated to each one. Features may define
general properties of rewrite rules or properties which are strictly related to the
model under investigation. We define a membrane type for the compartments of
our model and develop a type systems enforcing the property that a compartment
must contain only local rules with specific features. Our framework has been
presented in [
        <xref ref-type="bibr" rid="ref4">4</xref>
        ].
      </p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <given-names>R.</given-names>
            <surname>Barbuti</surname>
          </string-name>
          ,
          <string-name>
            <given-names>A.</given-names>
            <surname>Maggiolo-Schettini</surname>
          </string-name>
          ,
          <string-name>
            <given-names>P.</given-names>
            <surname>Milazzo</surname>
          </string-name>
          and
          <string-name>
            <given-names>A.</given-names>
            <surname>Troina</surname>
          </string-name>
          .
          <article-title>A Calculus of Looping Sequences for Modelling Microbiological Systems</article-title>
          .
          <source>Fundamenta Informaticae</source>
          ,
          <volume>72</volume>
          (
          <issue>1- 3</issue>
          ):
          <fpage>21</fpage>
          -
          <lpage>35</lpage>
          ,
          <year>2006</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <given-names>L.</given-names>
            <surname>Bioglio</surname>
          </string-name>
          .
          <article-title>A Minimal OO Calculus for Modelling Biological Systems. Computational Models for Cell Processes (CompMod) 2011</article-title>
          , EPTCS
          <volume>67</volume>
          :
          <fpage>50</fpage>
          -
          <lpage>64</lpage>
          ,
          <year>2011</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <given-names>L.</given-names>
            <surname>Bioglio</surname>
          </string-name>
          .
          <article-title>Enumerated Type Semantics for the Calculus of Looping Sequences</article-title>
          .
          <source>RAIRO - Theoretical Informatics and Applications</source>
          ,
          <volume>45</volume>
          (
          <issue>01</issue>
          ):
          <fpage>35</fpage>
          -
          <lpage>58</lpage>
          ,
          <year>2011</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <given-names>L.</given-names>
            <surname>Bioglio</surname>
          </string-name>
          ,
          <string-name>
            <given-names>M.</given-names>
            <surname>Dezani-Ciancaglini</surname>
          </string-name>
          ,
          <string-name>
            <given-names>P.</given-names>
            <surname>Giannini</surname>
          </string-name>
          and
          <string-name>
            <given-names>A.</given-names>
            <surname>Troina</surname>
          </string-name>
          .
          <article-title>A Calculus of Looping Sequences with Local Rules</article-title>
          .
          <source>7th Workshop on Developments in Computational Models (DCM'11)</source>
          , EPTCS
          <volume>88</volume>
          :
          <fpage>43</fpage>
          -
          <lpage>58</lpage>
          ,
          <year>2011</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <given-names>L.</given-names>
            <surname>Bioglio</surname>
          </string-name>
          ,
          <string-name>
            <given-names>M.</given-names>
            <surname>Dezani-Ciancaglini</surname>
          </string-name>
          ,
          <string-name>
            <given-names>P.</given-names>
            <surname>Giannini</surname>
          </string-name>
          and
          <string-name>
            <given-names>A.</given-names>
            <surname>Troina</surname>
          </string-name>
          .
          <article-title>Type Directed Semantics for the Calculus of Looping Sequences</article-title>
          .
          <source>International Journal of Software and Informatics</source>
          , to appear.
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <given-names>A.</given-names>
            <surname>Igarashi</surname>
          </string-name>
          ,
          <string-name>
            <given-names>B.</given-names>
            <surname>Pierce</surname>
          </string-name>
          and
          <string-name>
            <given-names>P.</given-names>
            <surname>Wadler</surname>
          </string-name>
          .
          <article-title>Featherweight Java: a Minimal Core Calculus for Java and GJ</article-title>
          .
          <source>ACM Transactions on Programming Languages and System</source>
          ,
          <volume>23</volume>
          :
          <fpage>396</fpage>
          -
          <lpage>450</lpage>
          ,
          <year>2001</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          7. G. Pa˘un.
          <source>Membrane Computing. An Introduction</source>
          . Springer,
          <year>2002</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          8.
          <string-name>
            <given-names>J. B.</given-names>
            <surname>Wells</surname>
          </string-name>
          .
          <article-title>The Essence of Principal Typings</article-title>
          .
          <source>International Colloquium on Automata, Languages and Programming (ICALP'02)</source>
          , LNCS
          <volume>2380</volume>
          :
          <fpage>913</fpage>
          -
          <lpage>925</lpage>
          ,
          <year>2002</year>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>