(Mathematical) Logic for Systems Biology (Invited Paper)

TL;DR

This paper advocates for using mathematical logic, specifically modal extensions of linear logic, as a unified framework for modeling, expressing properties, and verifying biological systems, with formal proofs demonstrated in Coq.

Contribution

It introduces two novel modal extensions of linear logic, HyLL and SELL, tailored for systems biology, and demonstrates their application through formal proofs in Coq.

Findings

Formal proofs of biological examples in Coq.

Introduction of HyLL and SELL logics for biological modeling.

Potential for automated reasoning in complex biological systems.

Abstract

We advocates here the use of (mathematical) logic for systems biology, as a unified framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The potential candidate logics should have a traditional proof theoretic pedigree (including a sequent calculus presentation enjoying cut-elimination and focusing), and should come with (certified) proof tools. Beyond providing a reliable framework, this allows the adequate encodings of our biological systems. We present two candidate logics (two modal extensions of linear logic, called HyLL and SELL), along with biological examples. The examples we have considered so far are very simple ones-coming with completely formal (interactive) proofs in Coq. Future works includes using automatic provers, which would extend existing automatic provers for linear logic. This should enable us to specify and study more realistic examples in systems biology, biomedicine (diagnosis and prognosis), and eventually neuroscience.

Equations

$$\mathtt{active}(a,b)\stackrel{\mathrm{def}}{=}\mathtt{pres}(a)-\circ (\mathtt{pres}(a)\otimes \mathtt{pres}(b)).$$

$$\frac{\Gamma ;\Delta ⊢A@u}{\Gamma ;\Delta ⊢(A\text{at}u)@w}\text{at}R\frac{\Gamma ;\Delta ,A@u⊢C@w}{\Gamma ;\Delta ,(A\text{at}u)@v⊢C@w}\text{at}L$$

$$\frac{\Gamma ;\Delta ⊢A[w/u]@w}{\Gamma ;\Delta ⊢\downarrow u.A@w}\downarrow R\frac{\Gamma ;\Delta ,A[v/u]@v⊢C@w}{\Gamma ;\Delta ,\downarrow u.A@v⊢C@w}\downarrow L$$

$$\square A\stackrel{\mathrm{def}}{=}\downarrow u.\forall w.(A\text{at}u.w)◊A\stackrel{\mathrm{def}}{=}\downarrow u.\exists w.(A\text{at}u.w){\delta }_{v}A\stackrel{\mathrm{def}}{=}\downarrow u.(A\text{at}u.v)$$

$$\begin{array}[]{lcl}F&::=&{\bf 0}\mid 1\mid\top\mid\perp\mid p(\vec{t})\mid F_{1}\otimes F_{2}\mid F_{1}\oplus F_{2}\mid F_{1}\mathrel{\hbox{\raise 5.84013pt\hbox{\tiny.}\raise 6.08014pt\hbox{\tiny.}\raise 6.32014pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.80016pt\hbox{\tiny.}\raise 6.80016pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.32014pt\hbox{\tiny.}\raise 6.08014pt\hbox{\tiny.}\raise 5.84013pt\hbox{\tiny.}\raise 5.52013pt\hbox{\tiny.}\raise 5.20012pt\hbox{\tiny.}\raise 4.88011pt\hbox{\tiny.}\raise 4.5601pt\hbox{\tiny.}\raise 4.2401pt\hbox{\tiny.}\raise 4.00009pt\hbox{\tiny.}\raise 3.76009pt\hbox{\tiny.}\raise 3.52008pt\hbox{\tiny.}\raise 3.28008pt\hbox{\tiny.}\raise 2.96007pt\hbox{\tiny.}\raise 2.64006pt\hbox{\tiny.}\raise 2.32005pt\hbox{\tiny.}\raise 2.08005pt\hbox{\tiny.}\raise 1.84004pt\hbox{\tiny.}\raise 1.52003pt\hbox{\tiny.}\raise 1.20003pt\hbox{\tiny.}\raise 0.96002pt\hbox{\tiny.}\raise 0.64001pt\hbox{\tiny.}\raise 0.32pt\hbox{\tiny.}\raise 0.08pt\hbox{\tiny.}\raise-0.16pt\hbox{\tiny.}\raise-0.32pt\hbox{\tiny.}\raise-0.40001pt\hbox{\tiny.}\raise-0.40001pt\hbox{\tiny.}\raise-0.32pt\hbox{\tiny.}\raise-0.16pt\hbox{\tiny.}\raise 0.08pt\hbox{\tiny.}\raise 0.40001pt\hbox{\tiny.}\raise 0.72002pt\hbox{\tiny.}\raise 1.04002pt\hbox{\tiny.}\raise 1.28003pt\hbox{\tiny.}\raise 1.52003pt\hbox{\tiny.}\raise 1.76004pt\hbox{\tiny.}\raise 2.00005pt\hbox{\tiny.}\raise 2.24005pt\hbox{\tiny.}\raise 2.40005pt\hbox{\tiny.}\raise 2.56006pt\hbox{\tiny.}\raise 2.72006pt\hbox{\tiny.}\raise 2.88007pt\hbox{\tiny.}\raise 3.12007pt\hbox{\tiny.}\raise 3.36008pt\hbox{\tiny.}\raise 3.60008pt\hbox{\tiny.}\raise 3.84009pt\hbox{\tiny.}\raise 4.0801pt\hbox{\tiny.}\raise 4.4001pt\hbox{\tiny.}\raise 4.72011pt\hbox{\tiny.}\raise 5.04012pt\hbox{\tiny.}\raise 5.36012pt\hbox{\tiny.}\raise 5.68013pt\hbox{\tiny.}\raise 5.92014pt\hbox{\tiny.}\raise 6.16014pt\hbox{\tiny.}\raise 6.40015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.64015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.64015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.40015pt\hbox{\tiny.}\raise 6.24014pt\hbox{\tiny.}\raise 6.00014pt\hbox{\tiny.}\raise 5.76013pt\hbox{\tiny.}\raise 5.52013pt\hbox{\tiny.}\raise 5.28012pt\hbox{\tiny.}\raise 5.04012pt\hbox{\tiny.}\raise 4.72011pt\hbox{\tiny.}\raise 4.4001pt\hbox{\tiny.}\raise 4.0801pt\hbox{\tiny.}\raise 3.76009pt\hbox{\tiny.}\raise 3.44008pt\hbox{\tiny.}\raise 3.12007pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\hskip 4.0pt}}F_{2}\mid F_{1}\mathbin{\&}F_{2}\mid\\ &&\exists x.F\mid\forall x.F\mid\hbox{$\mathop{!}^{a}$}F\mid\hbox{$\mathord{?}^{a}$}F\end{array}$$

$$⊢{?}^{a_1}{F}_1,\dots {?}^{a_n}{F}_n,{!}^{a}G⊢{?}^{a_1}{F}_1,\dots {?}^{a_n}{F}_n,G⊢\Gamma ,{?}^{a}G⊢\Gamma ,G$$

$$⊢\Gamma ,⋒l_x:a.G⊢\Gamma ,G[l_e/l_x]⊢\Gamma ,⋓l_x:a.G⊢\Gamma ,G[l/l_x]$$

$${\square }_{u}A\stackrel{\mathrm{def}}{=}\forall l:u.{!}^{l}A{◊}_{u}A\stackrel{\mathrm{def}}{=}\exists l:u.{!}^{l}A\square A\stackrel{\mathrm{def}}{=}\forall t:\infty .{!}^{t}A◊A\stackrel{\mathrm{def}}{=}\exists t:\infty .{!}^{t}A$$

$$\mathtt{active}(a,b)\stackrel{\mathrm{def}}{=}\mathtt{pres}(a)-\circ {\delta }_1(\mathtt{pres}(a)\otimes \mathtt{pres}(b)).$$

$$\mathtt{inhib}(a,b)\stackrel{\mathrm{def}}{=}{!}^{t}a-\circ {!}^{t+1}(a\otimes b^{\perp }).$$

$$\mathtt{C}(n,breast,f,[\text{EPCAM}])-\circ {\delta }_d\mathtt{C}(n,blood,1,[\text{EPCAM}])$$

Full text

• coming with completely formal (interactive) proofs in Coq. Future works includes using automatic provers, which would extend existing automatic provers for linear logic. This should enable us to specify and study more realistic examples in systems biology, biomedicine (diagnosis and prognosis), and eventually neuroscience.

1 Introduction

We consider here the question of reasoning about biological systems in (mathematical) logic. We show that two new logics, both modal extensions of linear logic [12] (LL), are particularly well-suited to this purpose. The first logic, called Hybrid Linear Logic (HyLL), has been developed by the author in joint work with K. Chaudhuri [8]. The second logic, an extension of Subexponential Linear Logic ($\textrm{SELL}^{\Cap}$), has been independently proposed by C. Olarte, E. Pimentel and V. Nigam [15]. Both HyLL and SELL provide a unified framework to encode biological systems, to express temporal properties of their dynamic behaviour, and to prove these properties. By constructing proofs in the logics, we directly witness reachability as logical entailment [13, 17]. This approach is in contrast to most current approaches to applying formal methods to systems biology, which generally encode biological systems either in a dedicated programming language [19, 10, 6], or in differential equations [5], express properties in a temporal logic, and then verify these properties against some form of traces (model-checking), eventually built using an external simulator.

In a joint work with E. De Maria and A. Felty, we presented some first applications of HyLL to systems biology [13]. In these first experiments, we focused on Boolean systems and in this case a time unit corresponds to a transition in the system. We believe that discrete modeling is crucial in systems biology because it allows taking into account some phenomena that have a very low chance of happening (and could thus be neglected by differential approaches), but which may have a strong impact on system behavior.

In a recent joint work with C. Olarte and E. Pimentel [9], we compared HyLL and SELL, providing two encodings. The first enoding is from HyLL’s logical rules into LL with the highest level of adequacy, hence showing that HyLL is as expressive as LL. We also proposed an encoding of HyLL into $\textrm{SELL}^{\Cap}$ , showing that $\textrm{SELL}^{\Cap}$ is more expressive than HyLL. However, the simplicity of HyLL might be of interest, both from the user point of view and as far as proof search is concerned (a priori easier and more efficient in HyLL than in SELL). In this joint work, we furthermore encoded temporal operators of Computational Tree Logic (CTL) into linear logic with fixed point operators.

We first recall here these two previous works. Then we briefly mention our current joint work with P. Lio, on formalizing the evolution of cancer cells, concluding with some future work.

This note is thus based on joint works with K. Chaudhuri (INRIA Saclay), A. Felty (Univ. of Ottawa), P. Lio (Cambridge Univ.), and C. Olarte and E. Pimentel (Universidade Federal do Rio Grande do Norte, Brazil).

2 Preliminaries

Although we assume that the reader is familiar with linear logic [12] (LL), we review some of its basic proof theory in the following sections. First, let us gently introduce linear logic by means of an example.

2.1 Linear Logic for Biology

Linear Logic (LL) [12] is particularly well suited for describing state transition systems. LL has been successfully used to model such diverse systems as: the $\pi$-calculus, concurrent ML, security protocols, multiset rewriting, and games.

In the area of biology, a rule of activation (e.g., a protein activates a gene or the transcription of another protein) can be modeled by the following LL axiom:

[TABLE]

The formula $\mathtt{active}(a,b)$ describes the fact that a state where $a$ is present ($\mathtt{pres}(a)$ is true) can evolve into a state where both $\mathtt{pres}(a)$ and $\mathtt{pres}(b)$ are true.

Propositions such as $\mathtt{pres}(a)$ are called resources, and a rule in the logic can be viewed as a rewrite rule from a set of resources into another set of resources, where a set of resources describes a state of the system. Thus, a particular state transition system can be modeled by a set of rules of the above shape. The rules of the logic then allow us to prove some desired properties of the system, such as, for example, the existence of a stable state. However, linear implication is timeless. Linear implication can be used to model one event occurring after another, but it cannot be precise about how many steps or how long the delay is without explicitly encoding time. In a domain where resources have lifetimes and state changes have temporal, probabilistic or stochastic constraints, then the logic will allow inferences that may not be realizable in the system being modeled. This was the motivation of the development of HyLL, which was designed to represent constrained transition systems.

2.2 Linear Logic and Focusing

Literals are either atomic formulas ($p$) or their negations ($p^{\bot}$). The connectives $\otimes$ and $\mathrel{\hbox{\raise 5.84013pt\hbox{\tiny.}\raise 6.08014pt\hbox{\tiny.}\raise 6.32014pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.80016pt\hbox{\tiny.}\raise 6.80016pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.32014pt\hbox{\tiny.}\raise 6.08014pt\hbox{\tiny.}\raise 5.84013pt\hbox{\tiny.}\raise 5.52013pt\hbox{\tiny.}\raise 5.20012pt\hbox{\tiny.}\raise 4.88011pt\hbox{\tiny.}\raise 4.5601pt\hbox{\tiny.}\raise 4.2401pt\hbox{\tiny.}\raise 4.00009pt\hbox{\tiny.}\raise 3.76009pt\hbox{\tiny.}\raise 3.52008pt\hbox{\tiny.}\raise 3.28008pt\hbox{\tiny.}\raise 2.96007pt\hbox{\tiny.}\raise 2.64006pt\hbox{\tiny.}\raise 2.32005pt\hbox{\tiny.}\raise 2.08005pt\hbox{\tiny.}\raise 1.84004pt\hbox{\tiny.}\raise 1.52003pt\hbox{\tiny.}\raise 1.20003pt\hbox{\tiny.}\raise 0.96002pt\hbox{\tiny.}\raise 0.64001pt\hbox{\tiny.}\raise 0.32pt\hbox{\tiny.}\raise 0.08pt\hbox{\tiny.}\raise-0.16pt\hbox{\tiny.}\raise-0.32pt\hbox{\tiny.}\raise-0.40001pt\hbox{\tiny.}\raise-0.40001pt\hbox{\tiny.}\raise-0.32pt\hbox{\tiny.}\raise-0.16pt\hbox{\tiny.}\raise 0.08pt\hbox{\tiny.}\raise 0.40001pt\hbox{\tiny.}\raise 0.72002pt\hbox{\tiny.}\raise 1.04002pt\hbox{\tiny.}\raise 1.28003pt\hbox{\tiny.}\raise 1.52003pt\hbox{\tiny.}\raise 1.76004pt\hbox{\tiny.}\raise 2.00005pt\hbox{\tiny.}\raise 2.24005pt\hbox{\tiny.}\raise 2.40005pt\hbox{\tiny.}\raise 2.56006pt\hbox{\tiny.}\raise 2.72006pt\hbox{\tiny.}\raise 2.88007pt\hbox{\tiny.}\raise 3.12007pt\hbox{\tiny.}\raise 3.36008pt\hbox{\tiny.}\raise 3.60008pt\hbox{\tiny.}\raise 3.84009pt\hbox{\tiny.}\raise 4.0801pt\hbox{\tiny.}\raise 4.4001pt\hbox{\tiny.}\raise 4.72011pt\hbox{\tiny.}\raise 5.04012pt\hbox{\tiny.}\raise 5.36012pt\hbox{\tiny.}\raise 5.68013pt\hbox{\tiny.}\raise 5.92014pt\hbox{\tiny.}\raise 6.16014pt\hbox{\tiny.}\raise 6.40015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.64015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.64015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.40015pt\hbox{\tiny.}\raise 6.24014pt\hbox{\tiny.}\raise 6.00014pt\hbox{\tiny.}\raise 5.76013pt\hbox{\tiny.}\raise 5.52013pt\hbox{\tiny.}\raise 5.28012pt\hbox{\tiny.}\raise 5.04012pt\hbox{\tiny.}\raise 4.72011pt\hbox{\tiny.}\raise 4.4001pt\hbox{\tiny.}\raise 4.0801pt\hbox{\tiny.}\raise 3.76009pt\hbox{\tiny.}\raise 3.44008pt\hbox{\tiny.}\raise 3.12007pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\hskip 4.0pt}}$ and their units $1$ and $\bot$ are multiplicative; the connectives $\oplus$ and $\mathbin{\&}$ and their units [math] and $\top$ are additive; $\forall$ and $\exists$ are (first-order) quantifiers; and $\mathop{!}$ and $\mathord{?}$ are the exponentials (called bang and question-mark, respectively).

First proposed by Andreoli [1] for linear logic, focused proof systems provide normal form proofs for cut-free proofs. The connectives of linear logic can be divided into two classes. The negative connectives have invertible introduction rules: these connectives are $\mathrel{\hbox{\raise 5.84013pt\hbox{\tiny.}\raise 6.08014pt\hbox{\tiny.}\raise 6.32014pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.80016pt\hbox{\tiny.}\raise 6.80016pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.32014pt\hbox{\tiny.}\raise 6.08014pt\hbox{\tiny.}\raise 5.84013pt\hbox{\tiny.}\raise 5.52013pt\hbox{\tiny.}\raise 5.20012pt\hbox{\tiny.}\raise 4.88011pt\hbox{\tiny.}\raise 4.5601pt\hbox{\tiny.}\raise 4.2401pt\hbox{\tiny.}\raise 4.00009pt\hbox{\tiny.}\raise 3.76009pt\hbox{\tiny.}\raise 3.52008pt\hbox{\tiny.}\raise 3.28008pt\hbox{\tiny.}\raise 2.96007pt\hbox{\tiny.}\raise 2.64006pt\hbox{\tiny.}\raise 2.32005pt\hbox{\tiny.}\raise 2.08005pt\hbox{\tiny.}\raise 1.84004pt\hbox{\tiny.}\raise 1.52003pt\hbox{\tiny.}\raise 1.20003pt\hbox{\tiny.}\raise 0.96002pt\hbox{\tiny.}\raise 0.64001pt\hbox{\tiny.}\raise 0.32pt\hbox{\tiny.}\raise 0.08pt\hbox{\tiny.}\raise-0.16pt\hbox{\tiny.}\raise-0.32pt\hbox{\tiny.}\raise-0.40001pt\hbox{\tiny.}\raise-0.40001pt\hbox{\tiny.}\raise-0.32pt\hbox{\tiny.}\raise-0.16pt\hbox{\tiny.}\raise 0.08pt\hbox{\tiny.}\raise 0.40001pt\hbox{\tiny.}\raise 0.72002pt\hbox{\tiny.}\raise 1.04002pt\hbox{\tiny.}\raise 1.28003pt\hbox{\tiny.}\raise 1.52003pt\hbox{\tiny.}\raise 1.76004pt\hbox{\tiny.}\raise 2.00005pt\hbox{\tiny.}\raise 2.24005pt\hbox{\tiny.}\raise 2.40005pt\hbox{\tiny.}\raise 2.56006pt\hbox{\tiny.}\raise 2.72006pt\hbox{\tiny.}\raise 2.88007pt\hbox{\tiny.}\raise 3.12007pt\hbox{\tiny.}\raise 3.36008pt\hbox{\tiny.}\raise 3.60008pt\hbox{\tiny.}\raise 3.84009pt\hbox{\tiny.}\raise 4.0801pt\hbox{\tiny.}\raise 4.4001pt\hbox{\tiny.}\raise 4.72011pt\hbox{\tiny.}\raise 5.04012pt\hbox{\tiny.}\raise 5.36012pt\hbox{\tiny.}\raise 5.68013pt\hbox{\tiny.}\raise 5.92014pt\hbox{\tiny.}\raise 6.16014pt\hbox{\tiny.}\raise 6.40015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.64015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.72015pt\hbox{\tiny.}\raise 6.64015pt\hbox{\tiny.}\raise 6.56015pt\hbox{\tiny.}\raise 6.40015pt\hbox{\tiny.}\raise 6.24014pt\hbox{\tiny.}\raise 6.00014pt\hbox{\tiny.}\raise 5.76013pt\hbox{\tiny.}\raise 5.52013pt\hbox{\tiny.}\raise 5.28012pt\hbox{\tiny.}\raise 5.04012pt\hbox{\tiny.}\raise 4.72011pt\hbox{\tiny.}\raise 4.4001pt\hbox{\tiny.}\raise 4.0801pt\hbox{\tiny.}\raise 3.76009pt\hbox{\tiny.}\raise 3.44008pt\hbox{\tiny.}\raise 3.12007pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\raise 2.80006pt\hbox{\tiny.}\hskip 4.0pt}}$, $\perp$, $\mathbin{\&}$, $\top$, $\forall$, and $\mathord{?}$. The positive connectives $\otimes$, $1$, $\oplus$, ${\bf 0}$, $\exists$, and $\mathop{!}$ are the de Morgan duals of the negative connectives. A formula is positive if it is a negated atom or its top-level logical connective is positive. Similarly, a formula is negative if it is an atom or its top-level logical connective is negative.

Focused proofs are organized into two phases. In the negative phase, all the invertible inference rules are eagerly applied. The positive phase begins by choosing a positive formula $F$ on which to focus. Positive rules are applied to $F$ until either $1$ or a negated atom is encountered (and the proof must end by applying the initial rules), the promotion rule ($\mathop{!}$) is applied, or a negative subformula is encountered and the proof switches to the negative phase.

This change of phases on proof search is particularly interesting when the focused formula is a bipole [1]. Focusing on a bipole will produce a single positive and a single negative phase. This two-phase decomposition enables us to adequately capture the application of object-level inference rules by the meta-level linear logic, as shown in [9].

2.3 Hybrid Linear Logic

Hybrid Linear Logic (HyLL) is a conservative extension of Intuitionistic first-order Linear Logic (ILL) [12] where the truth judgments are labelled by worlds representing constraints on states and state transitions. Instead of the ordinary judgment “$A$ is true”, for a proposition $A$, judgments of HyLL are of the form “$A$ is true at world $w$”, abbreviated as $A~{}@~{}w$. Particular choices of worlds produce particular instances of HyLL. Typical examples are “$A$ is true at time $t$”, or “$A$ is true with probability $p$”. HyLL was first proposed in [8] and it has been used as a logical framework for specifying biological systems [13].

Formally, worlds are defined as follows.

Definition 1 (HyLL worlds)

A constraint domain $\cal W$ is a monoid structure $\langle W,.,\iota\rangle$. The elements of $W$ are called worlds and its reachability relation $\preceq\ :W\times W$ is defined as $u\preceq w$ if there exists $v\in W$ such that $u.v=w$.

The identity world $\iota$ is $\preceq$-initial and is intended to represent the lack of any constraints. Thus, the ordinary first-order linear logic is embeddable into any instance of HyLL by setting all world labels to the identity. A typical, simple example of constraint domain is $\mathcal{T}=\langle{I\!\!N},+,0\rangle$, representing instants of time.

Atomic propositions $(p,q,\ldots)$ are applied to a sequence of terms $(s,t,\ldots)$, which are drawn from an untyped term language containing constants $(c,d,\ldots)$, term variables $(x,y,\ldots)$ and function symbols $(f,g,\ldots)$ applied to a list of terms $(\vec{t})$. Non-atomic propositions are constructed from the connectives of first-order intuitionistic linear logic and the two hybrid connectives satisfaction (at), which states that a proposition is true at a given world ($w,\iota,u.v,\ldots$), and localization ($\downarrow$), which binds a name for the (current) world the proposition is true at. The following grammar summarizes the syntax of HyLL.

[TABLE]

Note that world $u$ is bounded in the propositions $\downarrow u.~{}A$, $\forall u.~{}A$ and $\exists u.~{}A$. World variables cannot be used in terms, and neither can term variables occur in worlds. This restriction is important for the modular design of HyLL because it keeps purely logical truth separate from constraint truth. We note that $\downarrow$ and at commute freely with all non-hybrid connectives [8].

The sequent calculus [11] presentation of HyLL uses sequents of the form $\Gamma;\Delta\vdash C~{}@~{}w$ where $\Gamma$ (unbounded context) is a set and $\Delta$ (linear context) is a multiset of judgments of the form $A~{}@~{}w$. Note that in a judgment $A~{}@~{}w$ (as in a proposition $A~{}\texttt{at}~{}w$), $w$ can be any expression in $\cal W$, not only a variable.

The inference rules dealing with the new hybrid connectives are depicted below (the complete set of rules can be found in [8]).

[TABLE]

[TABLE]

Note that $(A~{}\texttt{at}~{}u)$ is a mobile proposition: it carries with it the world at which it is true. Weakening and contraction are admissible rules for the unbounded context.

The most important structural properties are the admissibility of the general identity (i.e. over any formulas, not only atomic propositions) and cut theorems. While the first provides a syntactic completeness theorem for the logic, the latter guarantees consistency (i.e. that there is no proof of $.;.\vdash\mathop{0}~{}@~{}w$).

Theorem 2.1 (Identity/Cut)

$\\ 1.~{}\Gamma;A~{}@~{}w\vdash A~{}@~{}w\\ 2.~{}{If}~{}\Gamma;\Delta\vdash A~{}@~{}u~{}{and}~{}\Gamma;\Delta^{\prime},A~{}@~{}u\vdash C~{}@~{}w,~{}{then}~{}\Gamma;\Delta,\Delta^{\prime}\vdash C~{}@~{}w\\ 3.~{}{If}~{}\Gamma;.\vdash A~{}@~{}u~{}{and}~{}\Gamma,A~{}@~{}u;\Delta\vdash C~{}@~{}w,~{}{then}~{}\Gamma;\Delta\vdash C~{}@~{}w.$**

Moreover, HyLL is conservative with respect to intuitionistic linear logic: as long as no hybrid connectives are used, the proofs in HyLL are identical to those in ILL. It is worth noting that HyLL is more expressive than S5, as it allows direct manipulation of the worlds using the hybrid connectives and HyLL’s $\delta$ connective (see Section 5) is not definable in S5. We also note that HyLL admits a complete focused [1] proof system. The interested reader can find proofs and further meta-theoretical theorems about HyLL in [8].

Modal Connectives.

We can define modal connectives in HyLL as follows:

Definition 2 (Modal connectives)

[TABLE]

$\Box A$ [resp. $\Diamond A$] represents all [resp. some] state(s) satisfying $A$ and reachable from now. The connective $\delta$ represents a form of delay.

2.4 Subexponentials in Linear Logic

Linear logic with subexponentials (SELL) shares with LL all its connectives except the exponentials: instead of having a single pair of exponentials $\mathop{!}$ and $\mathord{?}$, SELL may contain as many subexponentials [7, 18], written $\mathop{!}^{a}$ and $\mathord{?}^{a}$, as one needs. The grammar of formulas in SELL  is as follows:

[TABLE]

The proof system for SELL is specified by a subexponential signature $\Sigma=\langle I,\preceq,U\rangle$, where $I$ is a set of labels, $U\subseteq I$ is a set specifying which subexponentials allow weakening and contraction, and $\preceq$ is a pre-order among the elements of $I$. We shall use $a,b,\ldots$ to range over elements in $I$ and we will assume that $\preceq$ is upwardly closed with respect to $U$, i.e., if $a\in U$ and $a\preceq b$, then $b\in U$.

The system SELL is constructed by adding all the rules for the linear logic connectives except for the exponentials. The rules for subexponentials are dereliction and promotion of the subexponential labelled with $a\in I$

[TABLE]

Here, the rule $\mathop{!}^{a}$ has the side condition that $a\preceq{a_{i}}$ for all $\mathsl{i}$. That is, one can only introduce a $\mathop{!}^{a}$ on the right if all other formulas in the sequent are marked with indices that are greater or equal than $a$. Moreover, for all indices $a\in U$, we add the usual rules for weakening and contraction.

We can enhance the expressiveness of SELL with the subexponential quantifiers ${\Cap}$ and $\Cup$ ([15, 18]) given by the rules (omitting the subexponential signature)

[TABLE]

where $l_{e}$ is fresh. Intuitively, subexponential variables play a similar role as eigenvariables. The generic variable $l_{x}:a$ represents any subexponential, constant or variable in the ideal of $a$. Hence $l_{x}$ can be substituted by any subexponential $l$ of type $b$ (i.e., $l:b$) if $b\preceq a$. We call the resulting system $\textrm{SELL}^{\Cap}$.

As shown in [15, 18], $\textrm{SELL}^{\Cap}$ admits a cut-free and also a complete focused proof system.

Theorem 2.2

$\textrm{SELL}^{\Cap}$* admits cut-elimination for any subexponential signature.*

Modal connectives.

We can define modal connectives in SELL as follows:

[TABLE]

3 First experiments with HyLL

In a joint work with E. De Maria and A. Felty, we presented some first applications of HyLL to systems biology [13]. In these first experiments, we focused on Boolean systems and in this case a time unit corresponds to a transition in the system.

The activation rule seen in LL (Sec. 2.1) can be written in HyLL as

[TABLE]

We chosed a simple yet representative biological example concerning the DNA-damage repair mechanism based on proteins p53 and Mdm2, and present and proved several properties of this system. All these properties were reachability properties or the existence of an invariant. Most interesting proofs require induction or case analysis, that we borrowed from the meta-level (Coq). We fully formalized these proofs in the Coq Proof Assistant [3]. In Coq, we can both reason in HyLL and formalize meta-theoretic properties about it.

We discussed the merits and eventual drawbacks of this new approach compared to approaches using temporal logic and model checking. To better illustrate the correspondence with such approaches, which all use temporal logic to reason about (simulations of models of) the biological systems described, we also presented, informally but in some detail, the encoding of temporal logic operators in HyLL.

4 Relative Expressiveness Power of HyLL and SELL

We observe that, while linear logic has only seven logically distinct prefixes of bangs and question-marks, SELL allows for an unbounded number of such prefixes, e.g., $\mathop{!}^{i}$, or \mathop{!}^{i}$$\mathord{?}^{j}. Hence, by using different prefixes, we allow for the specification of richer systems where subexponentials are used to mark different modalities/states. For instance, subexponentials can be used to represent contexts of proof systems [16]; to specify systems with temporal, epistemic and spatial modalities [18] and to specify and verify biological systems [17]. An inhibition rule can be written in (classical) SELL as

[TABLE]

HyLL and Linear Logic.

One may wonder whether the use of worlds in HyLL increases also the expressiveness of LL. In a joint work with C. Olarte and E. Pimentel [9], we proved that this is not the case, by showing that HyLL rules can be directly encoded into LL by using the methods proposed in [14]. Moreover, the encoding of HyLL into LL is adequate in the sense that a focused step in LL corresponds exactly to the application of one inference rule in HyLL.

HyLL and SELL.

Linear logic allows for the specification of two kinds of context maintenance: both weakening and contraction are available (classical context) or neither is available (linear context). That is, when we encode (linear) judgments in HyLL belonging to different worlds, the resulting meta-level atomic formulas will be stored in the same (linear) LL context. The same happens with classical HyLL judgments and the classical LL context.

Although this is perfectly fine, encoding HyLL into $\textrm{SELL}^{\Cap}$  allows for a better understanding of worlds in HyLL. For that, we use subexponentials to represent worlds, having each world as a linear context. A HyLL judgment of the shape $F@w$ in the (left) linear context is encoded as the $\textrm{SELL}^{\Cap}$ formula \hbox{\mathord{?}^{w}}\lfloor F@w\rfloor. Hence, HyLL judgments that hold at world $w$ are stored at the $w$ linear context of $\textrm{SELL}^{\Cap}$. A judgment of the form $G@w$ in the classical HyLL context is encoded as the $\textrm{SELL}^{\Cap}$ formula \hbox{\mathord{?}^{\texttt{c}}}\hbox{\mathord{?}^{w}}\lfloor G@w\rfloor. Then, the encoding of $G@w$ is stored in the unbounded (classical) subexponential context c.

We showed that our encoding is indeed adequate. Moreover, as before, the adequacy of the encodings is on the level of derivations.

Information Confinement.

One of the features needed to specify spatial modalities is information confinement: a space/world can be inconsistent and this does not imply the inconsistency of the whole system. We showed in [9] that information confinement cannot be specified in HyLL. The authors in [15] exploit the combination of subexponentials of the form \mathop{!}^{w}$$\mathord{?}^{w} in order to specify information confinement in $\textrm{SELL}^{\Cap}$. More precisely, note that the sequents (in a 2-sided presentation of SELL) \hbox{\mathop{!}^{w}}\hbox{\mathord{?}^{w}}{\bf 0}\not\vdash{\bf 0} and \hbox{\mathop{!}^{w}}\hbox{\mathord{?}^{w}}{\bf 0}\not\vdash\hbox{\mathop{!}^{v}}\hbox{\mathord{?}^{v}}{\bf 0}, representing “inconsistency is local” and ‘ ‘inconsistency is not propagated” respectively hold in SELL.

5 Computation Tree Logic (CTL) in Linear Logic.

Hybrid linear logic is expressive enough to encode some forms of modal operators, thus allowing for the specification of properties of transition systems. As mentioned in [13], it is possible to encode CTL temporal operators into HyLL considering existential (E) and bounded universal (A) path quantifiers. We extended these encodings in [9], showing how to fully capture E and A CTL quantifiers in linear logic with fixed points. For that, we used the system $\mu$MALL [2] that extends MALL (multiplicative, additive linear logic) with fixed point operators. In [13], proofs of (encodings of) properties involving CTL quantifiers use induction borrowed from the (Coq) meta-level. In [9], we could directly use fixed points in linear logic.

6 Concluding Remarks and Future Work

Concerning related work, it is worth noticing that there are some other logical frameworks that are extensions of LL, for example, HLF[20]. Being a logic in the LF family, HLF is based on natural deduction, hence having a complex notion of ($\beta\eta$) normal forms. Thus adequacy (of encodings of systems) results are often much harder to prove in HLF than in (focused) HyLL/SELL. HLF seems to have been later abandonned in favour of Hybridized Intuitionistic Linear Logic (HILL) [4]

• a type theory based on a subpart of HyLL.

Both HyLL and SELL have been used for formalizing and analyzing biological systems [13, 17]. SELL proved to be a broader framework for handling such systems (in particular localities). However, the simplicity of HyLL may be of interest for specific purposes, such as building tools for diagnosis in biomedicine.

Formal proofs in HyLL were implemented in [13], in the Coq [3] proof assistant. It would be interesting to extend the implementations of HyLL given there to SELL. Such an interactive proof environment would enable both formal studies of encoded systems in SELL and formal meta-theoretical study of SELL itself.

We may pursue the goal of using HyLL/SELL for further applications. That might include neuroscience, a young and promising science where many hypotheses are provided and need to be verified. Indeed, logic is a general tool whose area of potential applications are not restricted per se. This is in contrast to most of the other approaches, which are valid only in a restricted area (typically inside or outside the cell).

In an ongoing joint work with P. Lio, we are formalizing the evolution of cancer cells, acquiring driver or passenger mutations. A rule describing an intravasating Circulating Tumour Cell, for example, might be:

[TABLE]

where $f$ is a fitness parameter, here in $\{0,1\}$. Our long term goal here is the design of a Logical Framework for disease diagnosis and therapy prognosis. This requires the development of automatic tools for proof search in our logics. These tools should benefit both from current research on proof search in linear logic and from current developments of automatic provers for SELL.