Complex Forming Processes

In order to strengthen the analogy between chemical reagents and compu-tational processes we now extend the language into one of complex forming process expressions. Save the omission of internal actions and conditionals, this language is identical to the π-calculus of Milner, Parrow, and Walker [MPW92, Mil99, SW01, Par01]. Suitable for the modelling of biochemical enti-ties and complexes it forms a powerful subset of the BioAmbients calculus.

Complex forming processes emerge when we allow names to be communicated when reactions occur. This is embodied in the local communication capabili-ties, a new set of primitives that subsumes the simple capabilities as a special case. The definition relies on a notion of variables, p, q, that we pick from a denumerable set,Var, and use as placeholders for the constants received during communication. As we shall see, the syntax admits both constants and vari-ables in many positions; hence it is common to refer to them simply asnames, x, y, and pick them from the denumerable set, Name, that is composed as the disjoint union of constants and variables, i.e.,Name=Const⊎ Var.

Definition 3.11 (Local communication capabilities) By alocal communi-cation capability we shall understand an element of the set defined by the fol-lowing syntax:

M ∈Cap ::= x!{y} Local output capability

| x?{p} Local input (co-)capability

Definition 3.12 (Variable binding) Inx?{p}.Pthe displayed occurrence of the variablepisbinding withscope P.

Definition 3.13 (Free and bound names) An occurrence of a namexin a process isbound if it is, or lies within the scope of, a binding occurrence of x.

If not bound,xisfree. A process with no free name isname closed.

Notation 3.14 (Name substitution) We shall write P[^m/x] for the substi-tution of the constant m for the namex in the process expression P, i.e., the process that is asP except that every free occurrence of the namexis replaced by the constantm.

Remark 3.15 Again, we postpone the operational definitions ofboundandfree

names until Chapter 5.

As was the case for the simple capabilities, the local communication capabilities only become operational when used for prefixing. Because of the involved name passing, however, reactions are no longer symmetric activities between processes;

rather they require one of the involved processes to act as sender and the other to act as recipient: The prefixn!{m}.P is a sender; it denotes a process that is capable of participating in the reaction identified byn, and if this capability is exercised the process shares its knowledge about the binding of m with the reaction partner and continues as P. In a complementary fashion the prefix n?{p}.Qis a recipient; it denotes a process that is capable of participating in the reaction identified byn, and if this capability is exercised the process learns about some name binding, e.g.,m, that is then substituted forpthroughoutQ, such that the process continues asQ[^m/p] rather thanQ.

Thus, the extension enables the passing of values from one entity to the other.

However, the main strength lies in the notion of scope extrusion that accom-panies this ability. For example, in a system (m)n!{m}.P n?{p}.Q P^′ a local communication reaction might occur such that in the resulting system (m) (P Q[^m/p]) P^′ the scope ofm has been extruded to include both P and Q[^m/p], i.e., P and Q[^m/p] now share the bond denoted by m, but it is not shared by anyone else.

This can be used to model the biological notion of complexes — especially the, often temporary, coordination compounds of molecular machineries that occur in conjunction with, e.g., the transcription of genes or the translation of RNA.

These compounds often form in an ad-hoc manner in order to perform some non-atomic piece of work, after which they disassemble again. The ad-hoc nature of such a compound calls for individual modelling of their constituting components.

The fixed cooperation structure of the compound, however, requires the model to enforce a temporary ’lock’ on the set of constituents throughout the lifetime of a complex. This is exactly what scope extrusion and recursion provides.

Now, when a communication reaction takes place, e.g., inn!{m}. P n?{p}. Q, then the result is defined in terms of a substitutionP Q[^m/p] of a constant for a variable. Ifmis bound inQ, i.e.,Qcontains a sub-expression (m)Q^′, thenm becomes spuriously bound by this binder ifQ^′ is of the form· · ·p· · ·.

This is called constant capture and, in order to avoid it, it is usual to demand static scope and define a notion of α-equivalence that allows bound constants to be freely changed.

Definition 3.16 (α-equivalence) Achange of bound constantsorα-renaming within a process P is the replacement of a subterm (n)Q ofP by (m)Q[^m/n] wherem /∈fn(Q). It is common to say thatP andQareα-equivalent,P ≡αQ, ifQcan be obtained fromP by a finite number of changes of bound constants.

Remark 3.17 Communication is defined in terms of a substitution,P[ⁿ/x], of a constant for a name, andα-equivalence is defined in terms of a substitution, P[^m/n], of a constant for a constant. In contrast we shall ensure in Chapter 5 that the need of substituting a variable for a variable or a process identifier for a process identifier shall never arise; hence we define α-equivalence neither for variables nor process identifiers.

Remark 3.18 (Canonical names) Many of the technical developments of the following sections and chapters will rely on the ability to statically track the names that occur in the processes of interest. Due to α-equivalence, however, the direct syntactical representation of names is not stable under the seman-tic relations; hence ordinary names are not suitable for carrying staseman-tic analysis information.

We solve this issue in the manner that is standard for Flow Logic based static analysis, e.g., [NNP04, HJNN99, BDNN01]. We associate each namexwith a canonical name ⌊x⌋ ∈Nameand demand thatα-renaming be disciplined, i.e., performed in such a way that canonical names are preserved, even when the syntactical representations change. When N is a set of names we shall write

⌊N⌋to denote the point-wise extension of⌊x⌋. Similarly we extend the operator to capabilities, i.e.,⌊M⌋isM where every name is canonicalised, and processes, i.e.,⌊P⌋isP where every name is canonicalised.

For any concrete process,P, we shall assume thatName, in contrast toName, is a finite set. And, like the ordinary names, this set is composed as the disjoint union of the canonical constants,⌊n⌋ ∈C, and the canonical variables,⌊p⌋ ∈V, i.e.,Name=C⊎V.

In practice we are going to takeName⊂ Name. In the case of variables, which are not subject toα-conversion, it then suffices to choose⌊p⌋=p. In the case of

P ∈Proc ::= (n)P Name restriction

| P ^µ Ambient boundary

| P P^′ Parallel composition

| P

i∈IM_i^ℓi.Pi Summation (guarded choice)

| recX. P Recursive process (definingX,recX. P)

| X Process identifier

Table 3.1: The syntax of BioAmbients processes, P.

constants, however, we shall assume that each distinct constant,n, occurring in the initial static program code gives rise to an equivalence class of constants rep-resented by the corresponding canonical constant,⌊n⌋. Disciplinedα-renaming then demands that the α-renaming process always picks the replacement name from the equivalence class of the replaced name and that the corresponding α-equivalence (Table 3.3) only holds when the bound names are indeed from the

same class.