rap-rech.epsi

                                    Logo-INRIA-couleur.epsi

THÈME 1 INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE

Proof of the subject reduction property for a π-calculus in COQ

Loïc Henry-Gréard

N° ????

Novembre 1998

                          Logo-INRIA-Sophia-couleur.epsi

Unité de recherche INRIA Sophia Antipolis 2004, route des Lucioles, B.P. 93, 06902 Sophia Antipolis Cedex (France)

Téléphone : 04 92 38 77 77 - International : +33 4 92 38 77 77 — Fax : 04 92 38 77 65 - International : +33 4 92 38 77 65

Proof of the subject reduction property for a π-calculus in COQ

Loïc Henry-Gréard

Thème 1 — Réseaux et systèmes Projet MEIJE

Rapport de recherche n° ???? — Novembre 1998 — 18 pages

Abstract: This paper presents a method for coding π-calculus in the COQ proof assistant, in order to use this environment to formalize properties of the pi-calculus. This method consists in making a syntactic discrimination between free names (then called parameters) and bound names (then called variables) of the processes, so that implicit renamings of bound names are avoided in the substitution operation. This technique has been used by J.McKinna and R.Pollack in an extensive study of PTS [5]. We use this coding here to prove subject reduction property for a type system of a monadic π-calculus.

Key-words: π-calculus, COQ, subject reduction

Preuve de la préservation des types pour un π-calcul codé en COQ

Résumé : Ce rapport présente une formalisation du π-calcul dans le système d’aide à la preuve COQ, point de depart vers des preuves de propriétés du π-calcul. La méthode employée pour coder les noms consiste en la séparation syntaxique des noms libres (paramètres) et des noms liés (variables), en vue d’éviter les renommages implicites dans les substitutions, technique proposée et intensivement utilisee par J. McKinna et R. Pollack [5] pour la formalisation des PTS. La preuve effectuée ici est celle de la propriété de conservation des types (subject reduction) d’un π-calcul monadique typé.

Mots-clés : π-calcul, COQ, préservation des types

π-calculus in COQ 3

1 Introduction

1.1 A typed monadic π-calculus

The π-calculus has been introduced in 1989 by Robin Milner, Joachim Parrow and David Walker [8], as an extension of the CCS process algebra, and extends CCS’s process synchronization expressivity with mobility of names, in order to have a complete formalization of concurrent processes. A precise description of π-calculus fundations can be found in [8]. A natural extension of the monadic πcalculus consists in considering name tuples as the values that can be passed between processes , instead of just names : the polyadic π-calculus. This version of π-calculus, described by R.Milner in [7], allows the introduction of a first notion of discipline on the use of names, since a reduction can be incorrect because of an arity mismatch. An other constraint on the use of names is introduced by D. Sangiorgi [9] [10] and concerns the directionality of names, that is, their ability to be used as emitters, receivers or both (or none). This name usage discipline is implemented by associating types to names, and by defining a predicate that states that the name that appears in a given process complies with the capacity they are given by an environment.

The proofs presented here as an application of the coding of the π-calculus is in this context the subject reduction property, which states that this correction predicate is preserved by the various kinds of reductions in a labelled transition semantics.

1.2 Coding name abstraction

The main difficulty in coding process algebras is in representing the binding of names in terms. In the π-calculus (of which the syntax is described below), name binding exists in two varieties:

Receivers: In the process p(x).Q, the name x is bound in the continuation process Q, waiting to be substituted by an other name before Q can be executed itself (Q is said to be “guarded” by p(x)). This abstraction is similar to λ-calculus abstraction (except for the guarding role of the input).

Scope restriction: In the process (νx : t)Q, the name x is only bound by a scope constraint. Its occurences in Q are not to be substituted, and the binder can be extruded, that is extended to processes that would come to receive x. This construction is what gives to the π-calculus all its expressivity. In fact, if the calculus is restricted to finite terms, that is, terms without the bang (!) operator, the scope restriction can be statically replaced by renamings of restricted names by fresh names, preserving the semantics:

a(x).P | (νx : t)(ā[x].Q | (νx : t′)R_{x})

being replaced by:

a(x).P | a[b].Q | R_{c}

The name restriction is needed to express that !(νx : t)ā[x] always sends a fresh name to processes that listen to channel a.

The coding of these abstractions must meet several criterias: to allow a simple definition of the substitution operation avoiding variables captures, and thus implicit renamings, allow a natural coding of the semantics relation, and avoid to have to consider α-conversion in proofs, that is to allow the manipulation of terms that will represent their whole α-equivalence class.

A direct coding of names by a set with decidable equality, a solution used by T. Melham using HOL [6], implies a difficult definition of the substitution operation, even just for substituting names for names. (νx)P {y/z} is simply defined for x = z and for x ≠ z, y ≠ x, but implies a renaming for x ≠ z, y = x.

In D. Hirschkoff [2], the coding uses de Bruijn indices, that is, replace bound names by pointers to their binder, coded by the number of binders one has to cross to find a given name’s binder. This method allows to be sure to manipulate processes modulo α-equivalence, since two α-equivalent terms are not syntactically discernable in this coding, but formalizing the semantics relation becomes complicated, because manipulation of these indices do not match our intuitive representation of terms.

The method used here is a transposition to the π-calculus syntax and semantics to the one used in [5] to PTS. The idea is to distinguish by two different constructors, the free and bound names in a process.

1.3 COQ

COQ ([4]) is a proof assistant based on the Calculus of Inductive Constructions (CIC). It allows interactive manipulation of CIC terms representing proofs of assertions, and to the building of such terms by mean of tactics that reflect intuitive mathematical reasoning. COQ is also able to extract algorithm from constructive proofs of their specification. This feature will not be used here.

Outline of the paper. The proofs of the subject reduction property is very simple, after many technical lemmas are defined, giving COQ’s user the basic tools to manipulate terms as one would naturally do on a paper and pencil proof. Part of these lemmas are given in section 4, as well as some steps of the proof of subject reducton property, for each kind of transition.

Before that, the reference semantics for the π-calculus (section 2.2), and the encoding method for this semantic (section 2.3) will be presented. A formal argument for the compliance of the coding with respect to the reference semantics will also be given. The type system will be introduced in section 3.

2 Semantics

This section presents the typed, monadic π-calculus, beginning by reference semantics, as used for informal reasoning, before the coding used in COQ for mechanized reasoning.

2.1 Syntax of a typed, monadic π-calculus

2.1.1 Reference syntax

The formalization work has been done for a classical monadic π-calculus, extended with an explicit type declaration for restricted names:

P ::= n̄m.P | n(m).P | (νn : t)P | (P | Q) | !P | P + Q | [n = m]P | 0

where P, Q,… represent processes, n, m,… an infinite set of names, supposed enumerable. t, t′, … represent types, associated with names. The various constructors that are introduced in this monadic version of π-calculus are those of [8]. The INPUT operator n(m).P expresses an agent that is waiting on a chanel named n, a piece of data that will be subsituted for m in its continuation P. The OUTPUT operator n̄m.P allows to transmit as data the name m on the chanel named n. The (νn : t)P, RESTRICTION operator, restricts the visibility of the name n to its body P. !P denotes an process with infinite behavior (cf. [7]). We call P r_{I} the set of processes syntactically defined this way.

2.1.2 Syntax in the COQ proof assistant

The system used here is an alternative to the use of de Bruijn indices [2]. The names are coded by a different constructor depending on the fact that they are in a bound position or in a free position in the process. Free names are called parameters, while bound names are called variables. We note P r_{P} the set of terms of the π-calculus syntactically defined this way. The concrete type for P r_{P} in COQ is called proc.

In the rest of the report, COQ expressions are translated in more commonly used mathematical notations. For exemple, a set of inference rules that caracterize a predicate will denode an inductively defined predicate in COQ. Parts of COQ code will be typed with a typewriter-like

font.

Parameters are noted p, q, r, variables x, y, z, names n, m and processes P, Q, R. According to notations in [5], parameters and variables set are respectively noted PP and VV. The definition of names in COQ follows:

Inductive name : Set :=
  pname : PP -> name |
  vname : VV -> name.

A predicate:

fresh: PP -> proc -> Prop

is also defined, noted p ∉ P(P), which states that a given parameter p does not appear in a given process P. Similarly, x ∉ V(P) denotes the fact that the variable x does not appear in process P.

Decidability of the equality for the sets PP and VV is given by two axioms PP_decidable and VV_decidable, and the facts that one can always find fresh parameters satisifying a number of conditions (PP is an infinite set), by axioms in the file exists.v.

The definition of processes in COQ follows:

Inductive proc : Set :=
  nil : proc |
  inp : name -> VV -> proc -> proc |
  out : name -> name -> proc -> proc |
  par : proc -> proc -> proc |
  res : VV -> type -> proc -> proc |
  ban : proc -> proc |
  sum : proc -> proc -> proc |
  mat : name -> name -> proc -> proc.

For example, the process (νx : t)(p̄x | x(y)) will be represented by the term:

(res x t (par (out (pname p) (vname x) nil)
              (inp (vname x) y nil)))

given of course that x and y are declared to have types VV and p to have type PP.

The main technical justification for this distinction between variables and parameters is that there is no need for renamings when a parameter is substituted for another in a process. A parameter cannot be captured, because binder can only point to variables, which have a different constructor.

We’ll see however that translating the reference semantics leads to substituting variables for names, which in principle entails captures (for example in (p(x).q̄r){x/q}). This difficulty is linked to the OPEN/CLOSE system of the semantics, that creates an abstraction when the scope of a name is extruded. It does not appear in [5].

2.2 Reference Semantics

The terms are considered modulo α-equivalence, the binding operators being INPUT and RE-STRICTION. The transition relation is considered as a relation between P r_{I}/ ≃_{α} and P r_{I}/ ≃_{α}, parameterized by names.

The formalization is based on a structural operational semantics described in fig. 1, that defines a labeled transitions system. The symmetric couterparts of rules PARl, SUMl, COMl and CLOSEl have not been represented. The choice of a labeled transitions systems allows us to take into consideration not only internal reductions, but also the interaction of processes with their environment. We will have different subject reduction properties for each kind of transition in order to reflect the relationship between conditions on the typing environment and conditions on the context in which the process is running.

6 Henry-Gréard

INPUT  \overline{x(y).X ⟶^{xz} X\{z/y\}}
OUTPUT  \overline{x̄y.X ⟶^{x̄y} X}
COMl  \frac{P ⟶^{xy} P′ Q ⟶^{x̄y} Q′}{P |Q ⟶^{τ} P′|Q′}
OPEN \frac{P ⟶^{x̄y} P′}{(νy : t)P ⟶^{x̄(y:t)} P′} x ≠ y
CLOSEl \frac{P ⟶^{xy} P′ Q ⟶^{x̄(y:t)} Q′}{P |Q ⟶^{τ} (νy : t)(P′|Q′)} y ∉ fv(P)
RES \frac{P ⟶^{μ} P′}{(νx : t)P ⟶^{μ} (νx : t)P′}  x ∉ n(μ)
PARl \frac{P ⟶^{μ} P′}{P |Q ⟶^{μ} P′|Q} bn(μ) ∩ fn(Q) = ∅
BANG  \frac{!P |P ⟶^{μ} P′}{!P ⟶^{μ} P′}
PLUSl  \frac{P ⟶^{μ} P′}{P + Q ⟶^{μ} P′}
MATCH  \frac{P ⟶^{μ} P′}{[x = x]P ⟶^{μ} P′}

Figure 1: Semantics for a monadic π-calculus

INRIA

The actions characterizing the transitions are the same than in [8]:

μ ::= xy | x̄y | x̄(y : t) | τ

that is, respectively, input, output, bound output and the silent action. The bound output action represents the emission of a name that is new to its receiver, and thus the action must carry the type of the exported name, as well as the name that extends its scope by scope extrusion.

The side conditions of the inference rules deal with the scope extrusion problem. The x ≠ y condition on the OPEN rule denotes that a process cannot emit on a private channel, which makes for example the process (νx : t)x̄[y], equivalent to 0 in terms of behavior (bisimilarity). The condition on the CLOSE rules indicates that a process that receives an exported name receives a name that is new to it. This condition is intended to avoid a capture and can lead to a renaming. The side condition for the rule RES states that a name restricted to a process being “invisible for the outside”, it cannot emit, nor receive, nor use this name as a communication channel. The side condition for the rule PAR avoids capture of a name in Q : a bound output action acts as a binder of the exported name on the resulting process. The PAR rule corresponds to a structural augmentation of the resulting process, where the names in Q can be binded.

2.3 Parameterized semantics

We build the labeled transitions relation in COQ from the reference semantics described above. The actions are the same, the names appearing in the actions are parameters:

Inductive act : Set :=
  aout : PP -> PP -> act |
  ainp : PP -> PP -> act |
  about : PP -> PP -> type -> act |
  tau : act.

We keep, as in [5], as an invariant the property closed of fully parameterized processes on both sides of the reduction arrow. This predicate checks that the process does not contain any variable in place of free names (as for example x in p(y).P_{y} |x̄q). These processes represent the “well-formed” processes.

We build an inductive property in COQ, each constructor being described by an inference rule that is a variant of an rule of the reference semantics.

sem : proc -> act -> proc -> Prop

scope extrusion The OPEN rule replaces the variable whose binder has disappeared by a fresh parameter. When the scope restriction is created again (CLOSE rule), these parameters are replaced by the bound variable, checking that no capture is possible, that is, that the variable is “new” (side condition). Because of this side condition, we cannot have the property

⟶^{μ} ∘ ≃_{α}=⟶^{μ}

any more, because for example:

(νx : t)p̄[x] | p(y).ȳ[q] | (νx : t)P ⟶^{τ} (νy : t)(0 | ȳ[q] | (νx : t)P)
≃_{α} (νx : t)(0 | x̄[q] | (νx : t)P)

while we cannot obtain:

(νx : t)p̄[x] | p(y).ȳ[q] | (νx : t)P ⟶^{τ} (νx : t)(0 | x̄[q] | (νx : t)P)

restrictions The semantics of the π-calculus express by the RES rule the same thing than the ξ rule of the λ-calculus, that [5] deals with. It is based on a coding of abstraction by the set of possible subsitutions of the bound variable, explicit in [1]. We must note that this rule is 8 Henry-Gréard

INPUT  \overline{p(x).P ⟶^{pq} P \{q/x\}}
OUTPUT  \overline{p̄q.P ⟶^{p̄q} P}
COMl  \frac{P ⟶^{pq} P′ Q ⟶^{p̄q} Q′}{P |Q ⟶^{τ} P′|Q′}
OPEN  \frac{P \{q/x\} ⟶^{p̄q} P′}{(νx : t)P ⟶^{p̄(q:t)} P′}  \begin{matrix}q ∉ P(P) \\ p ≠ q \end{matrix}
CLOSEl \frac{P ⟶^{pq} P′  Q ⟶^{p̄(r:t)} Q′}{P |Q ⟶^{τ} (νx : t)(P′\{x/q\}|Q′\{x/r\})}  \begin{matrix}q ∉ P(P) \\ x ∉ V(P′) ∪ V(Q′) \end{matrix}
RES  \frac{∀q P \{q/x\} ⟶^{μ} P′\{q/y\}}{(νx : t)P ⟶^{μ}(νy : t)P′}
PARl \frac{P ⟶^{μ} P′}{P |Q ⟶^{μ} P′|Q} \begin{matrix}μ = p̄(q : t) ⇒ \\ q ∉ P(Q) \end{matrix}
BANG  \frac{!P |P ⟶^{μ} P′}{!P ⟶^{μ} P′}
PLUSl  \frac{P ⟶^{μ} P′}{P + Q ⟶^{μ} P′}
MATCH  \frac{P ⟶^{μ} P′}{[p = p]P ⟶^{μ} P′}

Figure 2: parameterized monadic π-calculus

INRIA

the same than the PR̃1-BIND from [5], and that a transition relation, that is extensionally equivalent, can be obtained with a weaker induction principle by using the inference rule with a side condition instead of quantifying in the rule’s premise:

\frac{P \{p/x\} ⟶^{μ} P′\{p/y\}}{(νx : t)P ⟶^{μ} (νy : t)P′} p ∉ P(P) ∧ p ∉ P(μ)

The formalization for the proof of this equivalence, done in [5] by induction on the length of the terms, has not been done in this study.

2.4 Adequacy of the encoding

The encoding of the π-calculus in COQ is justified by formalizing the correspondance between the reference semantics of the calculus and our inductive predicate. The goal of this formalization is to justify the choice of the side-conditions and quantifications on parameters that have been added in the inference rules. We denote by NN the set of names used in the informal notation (figure 1). The PP, VV and NN sets are supposed to be enumerable, and we choose b_{P} : NN → PP a bijection from the set of names to the set of parameters. Let b_{I} = b_{P}^{−1}.

We can now build a one-one mapping between the α-equivalence classes of the processes described by the usual syntax (P r_{I}) and the processes described by the parameterized syntax (P r_{P}). Let T_{P} : P r_{I} → P r_{P} be this correspondance. The μ actions involved in the semantics relation of figure 1 can also be translated in the parameterized actions of figure 2. This translation is noted b_{P} (μ).

To establish the translation function T_{P}, we first define a series (x_{n})_{n∈N} of pairwise distinct elements of VV.

Then we define:

T_{P} (n(m).Q, N) = b_{P} (n)(x_{N}).(T_{P} (Q, N + 1){x_{N}/b_{P} (m)})
T_{P} (n̄m.Q, N) = \overline{b_{P} (n)}b_{P} (m).T_{P} (Q, N)
T_{P} ((νn : t)Q, N) = (νx_{N} : t)T_{P} (Q, N + 1){x_{N}/b_{p}(n)}
T_{P} (P | Q, N) = T_{P} (P, N) | T_{P} (Q, N)
.
.
.

Lemma 2.4.1 For every process P ∈ P r_{I}, and for every integer N and M, we have the following:

T_{P} (P, M) ≃_{α} T_{P} (P, N)

In order to define the inverse function of T_{P}, T_{I} : P r_{P} → P r_{I}, we take a series (p_{N})_{N∈M} of pairwise distinct elements of PP. As the terms are syntactically defined, the set P ars(P) = {N ∈ N | p_{N} ∈ fn(P)} is always finite. We note N_{0}^{P} = max P ars(P) + 1, and (n_{N} the series of (b_{I}(p_{N})). We define the function T_{I} as follows:

T_{I} (p(x).Q, N) = b_{I}(p)(n_{N}).T_{I}(Q{p_{N}/x}, N + 1)
T_{I} (p̄q.Q, N) = \overline{b_{I}(p)}b_{I}(q).T_{I}(Q, N)
T_{I} ((νx : t)Q, N) = (νn_{N} : t)T_{I}(Q{p_{N}/x}, N + 1)
T_{I} (P | Q, N) = T_{I}(P, N) | T_{I}(Q, N)
.
.
.

Property 2.4.1 If P, P′ are two processes of P r_{I}, and μ is an action, and if we have the P ⟶^{μ} P′

transition in the usual semantics, then we can build a transition Q ⟶^{b_{P} (μ)} Q′ in the parameterized semantics such that Q ≃_{α} T_{P} (P, 0) and Q′ ≃_{α} T_{P} (P′, 0).

The proof is done by induction on the derivation of the transition in the semantics of figure 1. For the INPUT rule we have:

n(m).Q ⟶^{nk} Q{k/m}

Where T_{P} (n(m).Q, 0) = b_{P} (n)(x_{0}).(T_{P} (Q, 1){x_{0}/b_{P} (m)}), which, according to the semantics coded in COQ, reduces to:

b_{P} (n)(x_{0}).(T_{P} (Q, 1){x_{0}/b_{P} (m)}) ⟶^{b_{P} (n)b_{P} (k)} T_{P} (Q, 1){x_{0}/b_{P} (m)}{b_{P} (k)/x_{0}}.

Since x_{0} does not appear in T_{P} (Q, 1), we have the right term of this derivation syntactically equal to T_{P} (Q, 1){b_{P} (k)/b_{P} (m)}, so with lemma 2.4.1, this term is also α-equivalent to the expected translation.

For the RES rule : if P ⟶^{μ} P′, then by the induction hypothesis, there exists Q and Q′ ∈ P r_{P}

such that Q ⟶^{b_{P} (μ)} Q′. Let m be the name whose scope is to be restricted to P, and p = b_{P} (m),

we have from the hypotheses p ∉ P(b_{P} (μ)), so Q{q/p} ⟶^{b_{P} (μ)} Q′{q/p} for every parameter q. But Q{q/p} = Q{x_{N}/p}{q/x_{N}} for every integer N big enough to avoid captures. The same reasoning

applies to Q′. We can then apply the RES rule of figure 2: \frac{∀q Q\{x_{N}/p\}\{q/x_{N}\} ⟶^{b_{P} (μ)} Q\{x_{N}/p\}\{q/x_{N}\}}{(νx_{N} : t)Q\{x_{N}/p\} ⟶^{b_{P} (μ)} (νx_{N} : t)Q′\{x_{N}/p\}}

However we have T ((νm : t)P, N) = (νx_{N} : t)T (P, N + 1){x_{N}/p}, so as Q ≃_{α} T (P, N + 1), we

have processes in the same α-class than their expected translations.

For the OPEN rule, we have from the hypotheses : \frac{P ⟶^{n̄m} P′}{(νm : t)P ⟶^{n̄(m:t)} P′} n ≠ m. Let

p = b_{P} (n), and q = b_{P} (m). From the induction hypothesis, we also have Q ⟶^{p̄q} Q′ with Q and Q′ α-convertible with the translations of P and P′. The hypothesis p ≠ q holds because b_{P} is a bijection. Taking N big enough to avoid captures, we have Q{x_{N}/q}{q/x_{N}} ⟶^{p̄q} Q′. The condition q ∉ P(Q{x_{N}/q}) being always respected, we can apply the transition rule and obtain

that (νx_{N} : t)Q{x_{N}/q} ⟶^{p̄(q:t)} Q′, which allows us to conclude. For the CLOSE rule: if we have:

\frac{P ⟶^{nm} P′ Q ⟶^{n̄(m)} Q′}{P | Q ⟶^{τ} (νm : t)(P′ | Q′)}

We note p = b_{P} (n) and q = b_{P} (m). By the induction hypothesis R_{P} ⟶^{pq} R_{P′} and R_{Q} ⟶^{p̄(q)} R_{Q′}. The hypothesis q ∉ P(Q_{P}) holds because m ∉ fv(P). Let N be big enough for the hypothesis x_{N} ∉ V(R_{P′}) ∪ V(R_{Q′}) to hold. We have, according to the CLOSE rule:

R_{P} | R_{Q} ⟶^{τ} (νx_{N} : t)(R_{P′}{x_{N}/q} | R_{Q′}{x_{N}/q}).

We can then verify that both members of the transition are α-equivalent to the expected translations.

Property 2.4.2 Whenever we have a transition P ⟶^{μ} P′ of the parameterized semantics, there exist Q and Q′ processes in P r_{I} such that

Q ⟶^{b_{I}(μ)} Q′)

is a valid transition according to the rules of figure 1 and Q ≃_{α} T_{I}(P, N_{0}^{P}) and Q′ ≃_{α} T_{I}(P′, N_{0}^{P′}).

The proof is again done by induction, with for example the rule INPUT: Let n = b_{I}(p), k = b_{I}(q) and N = max N_{0}^{p(x).P} N_{0}^{P {q/x}}. We have:

T_{I}(p(x).P, N) = n(n_{N}).T_{I}(P {p_{N}/x}, N + 1)

Which reduces according to the rules of figure 2 to:

n(n_{N}).T_{I}(P {p_{N}/x}, N + 1) ⟶^{n̄k} T_{I}(P {p_{N}/x}, N + 1){k/n_{N}}.

But T_{I}(P {p_{N}/x}, N + 1){k/n_{N}} = T_{I}(P {p_{N}/x}{q/p_{N}}, N + 1), and also p_{N} ∉ P(P), so we get:

T_{I}(p(x).P, N) ⟶^{n̄k} T_{I}(P {q/x}, N + 1)

For the RES rule: \frac{∀q P \{q/x\} ⟶^{μ} P′\{q/y\}}{(νx : t)P ⟶^{μ} (νy : t)P′} By the induction hypothesis, for every param-

eter q, we have:

T_{I}(P {q/x}, N) ⟶^{b_{I}(μ)} T_{I}(P′{q/y}, N),

so as p_{N} ∉ P(P), for a q_{0} such that q_{0} ∉ n(μ) we have:

T_{I}(P {p_{N}/x}{q_{0}/p_{N}}, N) ⟶^{b_{I}(μ)} T_{I}(P′{p_{N}/y}{q_{0}/p_{N}}, N).

If n = b_{I}(q_{0}), then the hypothesis n ∉ n(b_{I}(μ)) holds, so we have:

(νn : t)T_{I}(P {p_{N}/x}, N){n/n_{N}} ⟶^{b_{I}(μ)} (νn : t)T_{I}(P′{p_{N}/y}, N){n/n_{N}}.

The left and right members of this relation are α-equivalent to the expected translations.

3 The type system

This section presents the specifications of the type system. The type system can be implemented in several ways, allowing or not to build for every process a suitable typing environment.

3.1 Types

The type system used in our monadic π-calculus carries for every name two informations:

• A directionnality information noted ⟨t⟩, and called the capacity of t. This information expresses the capacity of the name to be used as a channel for a communication. The R (Read), W (Write), B (Both) and N (Nil) capacitie form a small lattice with a subtyping relation noted ≤_{c}:

[figure: N; R; W; B]

The names that have a R capacity can be used as receivers, like p in p(x).P, those of capacity W can be emitters, as p in p̄[q].P, those of capacity B can be both, and finaly those of capacity N cannot be receivers nor emitters, but can still appear in a term, like q in p̄[q].P.

• An information about the type of the names that can transit by a given channel This type is denoted [t]. For our monadic π-calculus, [t] represents itself a type since the only objects that can be transmitted are names. If we extend the calculus to polyadic π-calculus for example, [t] will be a set of types denoting the constraints on the set of names simultaneously transmitted by a channel (including an arity information).

Given a certain types set (data of type Set in COQ), and functions ⟨_⟩ and [_], we define axioms on the subtyping relation, based on the covariance of the receiving types, and countervariance of the emitting types (fig. 4). We then suppose that the subtyping relation is transitive.

Note that whatever the representation of the types IS, these cannot form an inf-semi lattice, since for example two types t_{1} and t_{2} such that ⟨t_{1}⟩ = ⟨t_{2}⟩ = B and [t_{1}] ≠ [t_{2}] do not have a minimum (it is impossible to find a type that is at the same time a subtype of one and of the other).

12 Henry-Gréard

TypNil  \overline{Γ ⊢ 0}
TypInp ∀q ∉ P(P) ; ⟨Γ(p)⟩ ≤_{c} I Γ ⊕ (q ↦ [Γ(p)]) ⊢ P {q/x} ; Γ ⊢ p(x).P
TypOut  \frac{⟨Γ(p)⟩ ≤_{c} O Γ(q) ≤ [Γ(p)] Γ ⊢ P}{Γ ⊢ p̄[q].P}
TypRes ∀q ∉ P(P) ; Γ ⊕ (q ↦ t) ⊢ P {q/x} ; Γ ⊢ (νx : t)P
TypPar  \frac{Γ ⊢ P Γ ⊢ Q}{Γ ⊢ P |Q}
TypBan  \frac{Γ ⊢ P}{Γ ⊢!P}
TypPlus  \frac{Γ ⊢ P Γ ⊢ Q}{Γ ⊢ P + Q}
TypMatch  \frac{⟨Γ(p)⟩ = ⟨Γ(q)⟩ = B Γ ⊢ P}{Γ ⊢ [p = q]P}

Figure 3: Typing rules for a monadic π-calculus

INRIA

STRefl  \overline{t ≤ t}

STNil  \frac{⟨t′⟩ = N}{t ≤ t′}

STRead  \frac{⟨t_{1}⟩ ≤_{c} R ⟨t_{2}⟩ = R [t_{1}] ≤ [t_{2}]}{t_{1} ≤ t_{2}}

STWrite \frac{⟨t_{1}⟩ ≤_{c} W ⟨t_{2}⟩ = W [t_{2}] ≤ [t_{1}]}{t_{1} ≤ t_{2}}

Figure 4: Subtyping rules for the names of π-calculus

3.2 Environments

The processes will be typed (fig 3) or not in a environment that gives to each of their free names (that is of their parameters), a type expressing what they can transmit, as well as the direction in which they can transmit it. This predicate is noted Γ ⊢ P ([10]). These environments, noted Γ, Δ, are total functions form the set of parameters to the set of types.

Example: In Γ such that ⟨Γ(p)⟩ = B, ⟨Γ(q)⟩ = N, ⟨Γ(r)⟩ = N, the processes p̄[q] and p(x).x̄[r] are correctly typed individually, but in the first case, it takes ⟨[Γ(p)]⟩ = N because of contravariance for typing emitting names, and in the second case ⟨[Γ(p)]⟩ ≤_{c} W because of the typing rule. Thus, the process p̄[q] | p(x).x̄[r] cannot be correctly typed in an environment that forbids emitting to q. For detailed arguments about the correction of the directionnality information in typing, with respect to an “incorrect” usage of channels in processes, see [9].

We note ⊕ (binary operator, left associativity), the operation such that Γ ⊕ (p ↦ t) is the function from parameters to types, that associates t to p and Γ(q) to every q ≠ p.

4 Proof for type preservation

The proof for the subject reduction properties are done very simply by an induction on the derivation of the labeled transitions, after we have defined a number of technical results, the most significant of which are given in the next subsection. Of course these results are themselves proven using a number of other lemmas. Thus, proving the subject reduction property for our formalization in COQ has been an opportunity to define many technical lemmas corresponding to intuitive facts a paper and pencil proof would not investigate, that provide a “toolbox” for future proofs.

4.1 Lemmas on substitutions

These lemmas, and those of the next section, are purely technical results and their proof in COQ is often trivial, by induction on the structure of the processes in most cases, the proof being then simplified by defining a similar lemma on the set of names, to factorize the verification of the property on process that include free names (output, input and match).

Lemma 4.1.1 (subs par after subs var)

∀P, p, q, x q ∉ P(P) ⟹ P {q/x}{p/q} = P {p/x}.

Lemma 4.1.2 (subs var after subs par)

∀P, p, q, x x ∉ V(P) ⟹ P {x/p}{q/x} = P {q/p}.

4.2 Lemmas on parameters

Lemma 4.2.1 (fresh after subs)

∀P, p, q, x p ∉ P(P) ∧ p ≠ q ⟹ p ∉ P(P {q/x}).

Lemma 4.2.2 (fresh before subs)

∀P, p, q, x p ∉ P(P {q/x}) ⟹ p ∉ P(P).

Lemma 4.2.3 (listening on known name)

∀P, P′, p, q P ⟶^{pq} P′ ⟹ p ∈ P(P).

Similar properties are of couse true for output and bound output acions.

Lemma 4.2.4 (fresh after trans)

∀P, μ, P′ P ⟶^{μ} P′ ⟹ ∀p p ∉ P(P) ∧ p ∉ P(μ) ⟹ p ∉ P(P′).

4.3 Subtyping lemmas

These lemmas allows us to manipulate subtyping on environments, that is, the extension of the subtyping relation on parameters, to environments that are total functions of parameters to types:

Γ ≤_{e} Δ ⇔ ∀p Γ(p) ≤ Δ(p).

Lemma 4.3.1 (subtyping extension)

∀Γ, Δ, p, t_{1}, t_{2} Δ ≤_{e} Γ ∧ t_{1} ≤ t_{2} ⟹ Δ ⊕ (p ↦ t_{1}) ≤_{e} Γ ⊕ (p ↦ t_{2}).

Lemma 4.3.2 (subtyping)

∀Γ, P Γ ⊢ P ⟹ ∀Δ Δ ≤_{e} Γ ⟹ Δ ⊢ P.

4.4 Swapping parameters

We introduce the “swap parameters” operator on processes, environments, names and parameters : swap_proc, swap_env, swap_name and swap_par. This operation is in all cases notes X{p ↔ q} where X is a process, an environment, a name or a parameter. This operation consists in substituting to every occurenceof p, an occurence of q, and to every occurences of q, an occurence of p. In the case of environments, Γ{p ↔ q} represents the function that associates Γ(q) to p, Γ(p) to q, and associates Γ(r) to every r different of p and q .

A number of properties are proved for this operator, including:

Lemma 4.4.1 (typing after swap)

∀Γ, P Γ ⊢ P ⟹ ∀p, q Γ{p ↔ q} ⊢ P {p ↔ q}.

4.5 Typing Lemmas

Lemma 4.5.1 (addenv unused name)

∀Γ, P Γ ⊢ P ⟹ ∀t, q ∉ P(P) Γ ⊕ (q ↦ t) ⊢ P.

Lemma 4.5.2 (redundant addenv)

∀Γ, P Γ ⊢ P ⟹ ∀Δ, p, t p ∉ P(P) ∧ Γ =_{e} Δ ⊕ (p ↦ t) ⟹ Δ ⊢ P.

Lemma 4.5.3 (type with other subs)

∀Γ, P, p, q, x, t p ∉ P(P) ∧ q ∉ P(P) ∧ Γ ⊕ (p ↦ t) ⊢ P {p/x} ⟹ Γ ⊕ (q ↦ t) ⊢ P {q/x}.

Proof The proof of this lemma uses parameter swapping in terms. We consider the non-trivial case where p ≠ q. From

Γ ⊕ (p ↦ t) ⊢ P {p/x}

we deduce (4.4.1)

(Γ ⊕ (p ↦ t)){p ↔ q} ⊢ P {p/x}{p ↔ q}.

As we have

(Γ ⊕ (p ↦ t)){p ↔ q} =_{e} Γ ⊕ (q ↦ t) ⊕ (p ↦ Γ(q))

We get the conclusion since p does not appear in P {q/x}.

Lemma 4.5.4 (subs typing)

∀Γ, P Γ ⊢ P ⟹ ∀p, q Γ(p) ≤ Γ(q) ⟹ Γ ⊢ P {p/q}

4.6 INPUT transitions

The property proved for INPUT transitions is the following:

P ⟶^{pq} P′ ⟹ Γ ⊢ P ⟹ Γ(q) ≤ [Γ(p)] ⟹ Γ ⊢ P′.

The proof is done by induction on the transition relation. In each case, the typing predicate is inverted according to the syntax of the processes involved in a given transition rule.

4.6.1 The INPUT rule

We have Γ ⊢ p(x).Q, so for every s ∉ P(Q),

Γ ⊕ (s ↦ [Γ(p)]) ⊢ Q{s/x}.

We also deduce from the hypothesis:

Γ ⊕ (s ↦ [Γ(p)])(q) ≤ Γ ⊕ (s ↦ [Γ(p)])(s).

(To simplify the proof in COQ, we also make the assumption that s is different from q).

Thus we can substitute the paramater q for the parameter s in the typing relation (lemma 4.5.4):

Γ ⊕ (s ↦ [Γ(p)]) ⊢ Q{s/x}{q/s}.

We know that s does not appear in the typed term, so we can omit to add it to the environment (lemma 4.5.2):

Γ ⊢ Q{s/x}{q/s}.

The fact that Q{q/x} = Q{s/x}{q/s} allows us to conclude (lemma 4.1.1).

4.6.2 The RES rule

The proof is the same for the RES rule whatever the transition kind is, so we will only describe it for the INPUT case.

If Γ ⊢ (νx : t)P, we want to obtain for any r ∉ P(P′),

Γ ⊕ (r ↦ t) ⊢ P′{r/y}.

Let s ∉ P(P), with s different from p, q and r. s ∉ P(P {r/x}) (lemme 4.2.1) ⟹ s ∉ P(P′{r/y})

(lemme 4.2.4), ⟹ s ∉ P(P′) (lemme 4.2.2). So we can apply the lemma 4.5.3 and conclude if we have:

Γ ⊕ (s ↦ t) ⊢ P′{s/y}

The induction hypothesis is:

∀r Δ ⊢ P {r/x} ⟹ Δ(q) ≤ [Δ(p)] ⟹ Δ ⊢ P′{r/y}.

We replace in this proposition, Δ by Γ ⊕ (s ↦ t) and r by s. The first condition is true because Γ ⊢ (νx : t)P, the second condition is true because s ≠ p and s ≠ q.

4.7 OUTPUT transitions

The result for OUTPUT transitions has two parts:

• A type preservation result:

P ⟶^{p̄q} P′ ⟹ Γ ⊢ P ⟹ Γ ⊢ P′,

• A constraint on the environment that stems from the initial typing correction:

P ⟶^{p̄q} P′ ⟹ Γ ⊢ P ⟹ Γ(q) ≤ [Γ(p)].

4.8 Bound OUTPUT transitions

We proove as for OUTPUT the following properties:

• A type preservation property:

P ⟶^{p̄(q:t)} P′ ⟹ Γ ⊢ P ⟹ Γ ⊕ (q ↦ t) ⊢ P′,

• a bout transition exports a type that is compatible with the typing environment:

P ⟶^{p̄(q:t)} P′ ⟹ Γ ⊢ P ⟹ t ≤ [Γ(p)].

4.8.1 The case of the OPEN rule

From the hypothesis:

\frac{P \{q/x\} ⟶^{p̄q} P′}{(νx : t)P ⟶^{p̄(q:t)} P′} for q ∉ P(P) and p ≠ q. and also Γ ⊢ (νx : t)P.

Type preservation. The type preservation property directly follows from the similar property for OUTPUT transitions: Γ ⊢ (νx : t)P, so for all r that does not appear in P, Γ ⊕ (r ↦ t) ⊢ P {r/x} (from the TypRes typing rule), so in particular for q. Thus by applying the subject reduction property for OUTPUT transitions to the P {q/x} ⟶^{p̄q} P′ transition we obtain:

Γ ⊕ (q ↦ t) ⊢ P′.

Exporting a correct type. We also use the similar property for OUTPUT:

(Γ ⊕ (q ↦ t)) (q) ≤ [(Γ ⊕ (q ↦ t)) (p)]

As we have p ≠ q, we can conclude that:

t ≤ [Γ(p)].

4.8.2 PAR rule

We need our side condition on the inference rule: taking for example the PARl rule: \frac{P ⟶^{p̄(q:t)} P′}{P |Q ⟶^{p̄(q:t)} P′|Q}

with the supplementary condition: q ∉ P(Q). The expected result is Γ ⊕ (q ↦ t) ⊢ P′ | Q.

• Γ ⊕ (q ↦ t) ⊢ P′ is given directly by the induction hypothesis.

• Γ ⊕ (q ↦ t) ⊢ Q follows from the fact that q ∉ P(Q), as well as from the hypothesis Γ ⊢ Q: we modify in a typing environment the type of a name that is not used in the typed process (lemma 4.5.1).

4.9 Internal transitions

We prove the following property:

P ⟶^{τ} P′ ⟹ Γ ⊢ P ⟹ Γ ⊢ P′.

4.9.1 COM rule

Let’s consider the COMl rule. The derivation of the transition ends with:

\frac{P ⟶^{pq} P′ Q ⟶^{p̄q} Q′}{P |Q ⟶^{τ} P′|Q′}

So we have Γ ⊢ P | Q, and we want to obtain Γ ⊢ P′ | Q′.

To proove Γ ⊢ P′ from Γ ⊢ P, we use the subject reduction property for the INPUT transitions. To validate the side condition Γ(q) ≤ [Γ(p)] of this property, we use the type correction property for the emission of a name by the transition Q ⟶^{p̄q} Q′.

The fact the we can deduce Γ ⊢ Q′ from Γ ⊢ Q simply stems from the subject reduction property for the transition Q ⟶^{p̄q} Q′.

4.9.2 CLOSE rule

We take the CLOSEl rule as example. The derivation of the transition ends with:

\frac{P ⟶^{pq} P′ Q ⟶^{p̄(r:t)} Q′}{P |Q ⟶^{τ} (νx : t)(P′\{x/q\}|Q′\{x/r\})}

.

We know on one hand that q ∉ P(P), i.e. that P actually receives a name that is unknown to it, and on a second hand that x ∉ V(P′) ∪ V(Q′), i.e. that there is no risk of capture of the new binding that is created by this rule.

From Q ⟶^{p̄(r:t)} Q′ and Γ ⊢ Q we deduce t ≤ [Γ(p)]; thus (Γ ⊕ (q ↦ t))(q) ≤ [Γ(p)]. Also, q not appearing in P,

Γ ⊢ P ⟹ Γ ⊕ (q ↦ t) ⊢ P

by the subject reduction property on the INPUTs:

Γ ⊕ (q ↦ t) ⊢ P′.

we have P′ = P′{x/q}{q/x} since x does not appear in P′. So for every s free in P′{x/q} (lemma 4.5.3) we have:

Γ ⊕ (s ↦ t) ⊢ P′{x/q}{s/x}.

On the other hand, r not appearing in Q, we have Γ ⊕ (r ↦ t) ⊢ Q′, by the subject reduction property on bounded emissions, so

∀s ∉ P(Q′{x/r}) Γ ⊕ (s ↦ t) ⊢ Q′{x/r}{s/x}.

We can then conclude:

Γ ⊢ (νx : t)(P′{x/q}|Q′{x/r}).

Conclusion

We have presented here a encoding of the π-calculus and used it to do a proof in the COQ theorem proover. The various lemmas that were needed to perform basic manipulations on π-terms can be reused for proofs of other properties. This coding has allowed a almost direct transcription of the usual semantics into COQ, and to code a proof that is close to the intuitive informal proof. Some initial mistakes in the transcription of the semantics have been uncovered during the proof process by encontering unsolvable or inconsistent goals, which is an argument in favor of mecanizing proofs and having formal methods to help believing in proofs on mathematical objects. But the COQ system also allows to exploit the prooving-is-computing principle and extract algorithms from proofs.

A natural extension of this work, besides extending the calculus to being able to transport name tuples instead of just name, would use this capability to generate, for example type checking algorithms for π-terms

Acknowledgmeents

This study has been done during a three month pre-doctorate internship in the INRIA Sophia-Antipolis, under the supervision of Joelle Despeyroux of the CROAP team, and Davide Sangiorgi of the MEIJE team. I would like to thank both of them for their disponibility and their advices on the π-calculus and COQ tips and tricks.

References

[1] Tom Melham Andrew Gordon. Five axioms of alpha-conversion. In J. Harrison J. von Wright, J. Grundy, editor, TPHOL’96, volume 1125, pages 173–190. Springer-Verlag, 196.

[2] Daniel Hirschkoff. A full formalisation of pi-calculus theory in the calculus of constructions, 1997.

[3] Daniel Hirschkoff. Mise en oeuvre de preuves de bisimulation. Phd thesis, École Nationale des Ponts et Chaussées (ENPC), in preparation, January 1999. In French.

[4] Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant: a tutorial, version 6.1. Technical Report RT 0204, Inria, Rocquencourt, France, August 1997. page html: http://www.inria.fr/RRRT/RT-0204.html.

[5] James McKinna and Robert Pollack. Some Pure Type Sytems formalized. To appear in a special issue on Formal Proof of the Journal of Automated Reasoning (JAR), 1999.

[6] T.F. Melham. A mechanized theory of the pi-calculus in hol. Technical Report 244, University of Cambridge Computer Laboratory, 1992.

[7] Robin Milner. The polyadic pi-calculus : a tutorial. Technical Report ECS-LFCS-91-180, LFCS, 1991.

[8] Walker Milner, Parrow. A calculus of mobile processes. Technical Report ECS-LFCS-89-85/6, LFCS, 1989.

[9] Davide Sangiorgi. Typing and subtyping for mobile processes. Math. Struct. in Comp. Science, 11, 1995.

[10] Davide Sangiorgi. An interpretation of typed objects into typed pi-calculus. INRIA RR-3000, 1996.

                        Logo-INRIA-picto.epsi

Unité de recherche INRIA Sophia Antipolis

2004, route des Lucioles - B.P. 93 - 06902 Sophia Antipolis Cedex (France)

Unité de recherche INRIA Lorraine : Technopôle de Nancy-Brabois - Campus scientifique

615, rue du Jardin Botanique - B.P. 101 - 54602 Villers lès Nancy Cedex (France)

Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu - 35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l’Europe - 38330 Montbonnot St Martin (France)

Unité de recherche INRIA Rocquencourt : Domaine de Voluceau - Rocquencourt - B.P. 105 - 78153 Le Chesnay Cedex (France)

Éditeur

INRIA - Domaine de Voluceau - Rocquencourt, B.P. 105 - 78153 Le Chesnay Cedex (France)

http://www.inria.fr ISSN 0249-6399