A Type System - From the Applied Pi Calculus to Horn Clauses for Protocols with Lists

The type rules are given in Figure 5. The type system defines the following judgments:

i: [1, L]∈Γ Fig. 5.Type system for the generalized process calculus

– Γ `ι: [1, L], which means thatιhas type[1, L]in the type environmentΓ; – Γ `M^G,Γ `P^G, which mean thatM^G,P^G, respectively, are well-typed in

the type environmentΓ.

– i₁: [1, L₁], . . . , i_h : [1, L_h]`pat^G Γ, which means that the patternpat^G has free indicesi₁, . . . , i_h of types [1, L₁], . . . ,[1, L_h] respectively, and binds the variables inΓ.

Most type rules are straightforward. For instance, the rule (Var) means that xi₁,...,i_h is well-typed when the types expected by x for its indices match the types of i1, . . . , ih. The rules (PatVar), (PatData), and (PatList) deal with the patterns xi1,...,i_h, f(pat^G₁, . . . ,pat^G_n), and list(i ≤ L,pat^G), respectively. They build the type environment that gives types to the variables bound in the pattern.

B Proofs

We writeP ≡α Qwhen the process P is equal toQ up to renaming of bound names: in an instrumented process(νa:a⁰[x1, . . . , xn, s1, . . . , sn⁰])P, the namea can be renamed, but the function symbola⁰ remains unchanged. This is why we may end up with instrumented processes in which the name ais different from the function symbol a⁰.

B.1 Proof of Lemma 1

Lemma 1 is an immediate consequence of the following lemma.

Lemma 2. LetΓ `P^G be a well-typed generalized process, such that the bound names of P^G are pairwise distinct and distinct from free names of P^G. Given an environment T forΓ `P^G, and a list of indicesei≤L, we have:e

Tren(P^G, T,ei≤L)e ≡_αP^GT. Furthermore, we have the following two properties:

P1. The bound names in Tren(P^G, T,ei ≤L)e are pairwise distinct and distinct from free names, except that in processesP+Q, the bound names inP need not be distinct from those inQ.

P2. All bound names inTren(P^G, T,ei≤L)e are of the forma^L^e^T^,...

ei^T,... when they come from(νa)inP^G and of the forma^L^T^,e^L^T^,...

v,ei^T,... when they come from(for alli≤ L, νai)inP^G.

Proof. The propertyTren(P^G, T,ei≤L)e ≡αP^GT is proved by an easy induction on the syntax ofP^G.

Properties P1 and P2 are proved by simultaneous induction on the syntax of P^G.

– CaseΠ_i≤LP^G: for eachv≤L^T, by induction hypothesis, the bound names in Tren(P^G, T[i 7→ v],(ei, i) ≤(L, L))e are pairwise distinct (except that in processes P +Q, the bound names in P need not be distinct from those in Q) and distinct from free names. Furthermore, they are of the form a^L^e^T^,L^T^,...

ei^T,v,... when they come from (νa) in P^G and of the form a^L^0T^,e^L^T^,L^T^,...

v⁰,ei^T,v,...

when they come from(for alli⁰ ≤L⁰, νa_i⁰)in P^G, so P2 holds. Hence the names Tren(P^G, T[i 7→ v],(ei, i) ≤ (eL, L)) are distinct from the names in Tren(P^G, T[i7→v⁰],(ei, i)≤(eL, L))whenv6=v⁰, so P1 holds.

– Case (for alli ≤ L, νai)P^G: by induction hypothesis, the bound names in Tren(P^G, T,ei≤L)e are pairwise distinct (except that in processesP+Q, the bound names inPneed not be distinct from those inQ) and distinct from free names. Furthermore, they are of the forma⁰^L^e^T^,...

ei^T,... when they come from(νa⁰) in P^G and of the form a⁰^L^T^,e^L^T^,...

v,ei^T,... when they come from(for alli ≤L, νa⁰_i) inP^G. The new bound namesa^L^T^,e^L^T

v,ei^T forv≤L^T are of the required form, so P2 holds. They are distinct from the free names and from the bound names ofTren(P^G, T,ei ≤L), since the bound names ine (for alli ≤L, νai)P^G are pairwise distinct and distinct from free names, so they do not use the same symbola. So P1 holds.

– The case(νa)P^G is similar to the previous one. All other cases follow easily using the induction hypothesis. We use the property that the bound names ofP^G are pairwise distinct and distinct from free names ofP^G. In the cases

“choose”, we also use that in processesP+Q, the bound names inP need not be distinct from those inQ, so the induction hypothesis already guarantees

that names are distinct when desired.

B.2 Proof of Theorem 3

Theorem 3 comes from the combination of two different results. The first result (Lemma 4) shows that the translation from generalized processes to processes commutes with the instrumentation (provided the translation is suitably re-named usingTren). The second result (Lemma 10) shows the soundness of the translation from instrumented processes to generalized Horn clauses.

Instrumentation Before proving the first result, we define the instrumentation of processes and generalized processes more formally by induction on the syntax of the processes, as follows.

Definition 5 Given a process P, a list of variables Vars =x1, . . . , xn, and a list of session identifiersSessId=s1, . . . , sn⁰, we define the instrumented process as follows:

– instr(in(M, x).P,Vars,SessId) =in(M, x).instr(P,(Vars, x),SessId);

– instr(!P,Vars,SessId) = !^sinstr(P,Vars,(SessId, s));

– instr((νa)P,Vars,SessId) = (νa:a[Vars,SessId])instr(P,Vars,SessId);

– In all other cases, the same instrumentation is applied recursively on the sub-processes. For instance,instr(P |Q,Vars,SessId) = instr(P,Vars,SessId)| instr(Q,Vars,SessId).

We letinstr(P) = instr(P,∅,∅).

Definition 6 Given a generalized processP^G, a list of variablesVars=x1, . . . , xn, a list of session identifiersSessId =s1, . . . , sn⁰, and a list of indicesei≤L,e we define the instrumented generalized process as follows:

– instr^G(in(M^G, x).P^G,Vars,SessId,ei≤L) =e in(M^G, x).instr^G(P^G,(Vars, x),SessId,ei≤L);e

– instr^G(!P^G,Vars,SessId,ei≤L) = !e ^sinstr^G(P^G,Vars,(SessId, s),ei≤L);e – instr^G(Π_i≤LP^G,Vars,SessId,ei≤L) =e

Π_i≤Linstr^G(P^G,Vars,SessId,(ei, i≤L, L));e – instr^G((for alli≤L, νai)P^G,Vars,SessId,ei≤L) =e

(for alli≤L, νa_i:a^L,e^L

i,ei [Vars,SessId])instr^G(P,Vars,SessId,ei≤L);e – instr^G((νa)P^G,Vars,SessId,ei≤L) =e

(νa:a^L^e

ei[Vars,SessId])instr^G(P^G,Vars,SessId,ei≤L);e

– In all other cases, the same instrumentation is applied recursively on the sub-processes. For instance,instr^G(P^G | Q^G,Vars,SessId,ei≤L) = instre ^G(P^G, Vars,SessId,ei≤L)e |instr^G(Q^G,Vars,SessId,ei≤L).e

We letinstr^G(P^G) = instr^G(P^G,∅,∅,∅ ≤ ∅).

The translationP^GT on instrumented processes is defined similarly to the translation on non-instrumented processes; the cases that differ are as follows:

– (!^sP^G)^T = !^sP^GT – ((νa : a⁰^L^e

ei[x1, . . . , xn, s1, . . . , sn⁰])P^G)^T = (νa : a⁰^L^e^T

ei^T [x1, . . . , xn, s1, . . . , sn⁰])P^GT

– ((for alli ≤L, νai : a⁰^L,e^L

i,ei [x1, . . . , xn, s1, . . . , sn⁰])P^G)^T = (νa1 :a⁰^L^T^,e^L^T

1,ei^T [x1, . . . , xn, s1, . . . , sn⁰]). . .(νaL_T :a⁰^L^T^,e^L^T

L^T,ei^T [x1, . . . , xn, s1, . . . , sn⁰])P^GT

Lemma 3. Given a well-typed generalized processΓ `P^G, an environment T for Γ ` P^G, a list of variables Vars = x₁, . . . x_n, a list of session identifiers SessId =s₁, . . . , s_n⁰, and a list of indicesei≤L, we have:e

(instr^G(P^G,Vars,SessId,ei≤L))e ^T ≡_αinstr(Tren(P^G, T,ei≤L),e Vars,SessId). Proof. This proof is done by structural induction on the processP^G. We detail here the most interesting cases.

– Casein(M^G, x).P^G:

(instr^G(in(M^G, x).P^G,Vars,SessId,ei≤L))e ^T

= (in(M^G, x).instr^G(P^G,(Vars, x),SessId,ei≤L))e ^T

=in(M^GT, x).(instr^G(P^G,(Vars, x),SessId,ei≤L))e ^T

≡_αin(M^GT, x).instr(Tren(P^G, T,ei≤L),e (Vars, x),SessId) by induction hypothesis

≡αinstr(in(M^GT, x).Tren(P^G, T,ei≤L),e Vars,SessId)

≡αinstr(Tren(in(M^G, x).P^G, T,ei≤L),e Vars,SessId) – Case!P^G:

(instr^G(!P^G,Vars,SessId,ei≤L))e ^T

= (!^sinstr^G(P^G,Vars,(SessId, s),ei≤L))e ^T

= !^s(instr^G(P^G,Vars,(SessId, s),ei≤L))e ^T

≡α!^sinstr(Tren(P^G, T,ei≤L),e Vars,(SessId, s))

by induction hypothesis

≡αinstr(!Tren(P^G, T,ei≤L),e Vars,SessId)

≡αinstr(Tren(!P^G, T,ei≤L),e Vars,SessId) – CaseΠ_i≤LP^G:

(instr^G(Π_i≤LP^G,Vars,SessId,ei≤L))e ^T

=Π_i≤L(instr^G(P^G,Vars,SessId,(ei, i)≤(eL, L)))^T

= (instr^G(P^G,Vars,SessId,(ei, i)≤(eL, L)))^T^[i7→1] | · · · | (instr^G(P^G,Vars,SessId,(ei, i)≤(eL, L)))^T^[i7→L^T^] For eachv≤L^T, we have by induction hypothesis:

instr^G(P^G,Vars,SessId,(ei, i)≤(L, L))e ^T[i7→v] ≡α

instr(Tren(P^G, T[i7→v],(ei, i)≤(L, L)),e Vars,SessId).

Hence:

(instr^G(Π_i≤LP^G,Vars,SessId,ei≤L))e ^T

≡αinstr(Tren(P^G, T[i7→1],(ei, i)≤(L, L)),e Vars,SessId)| · · · | instr(Tren(P^G, T[i7→L^T],(ei, i)≤(eL, L)),Vars,SessId)

≡αinstr(Tren(P^G, T[i7→1],(ei, i)≤(L, L))e | · · · |

Tren(P^G, T[i7→L^T],(ei, i)≤(eL, L)),Vars,SessId)

≡αinstr(Tren(Πi≤LP^G, T,ei≤L),e Vars,SessId)

– Case(for alli≤L, νa_i)P^G:

(instr^G((for alli≤L, νai)P^G,Vars,SessId,ei≤L))e ^T

= ((for alli≤L, νai :a^L,e^L

i,ei [Vars,SessId]) instr^G(P^G,Vars,SessId,ei≤L))e ^T

= (νa₁:a^L^T^,e^L^T

1,ei^T [Vars,SessId]). . .(νa_LT :a^L^T^,e^L^T

L^T,ei^T [Vars,SessId]) (instr^G(P^G,Vars,SessId,ei≤L))e ^T

Moreover, by induction hypothesis, (instr^G(P^G,Vars,SessId,ei ≤L))e ^T ≡_α instr(Tren(P^G, T,ei≤L),e Vars,SessId). Therefore,

(instr^G((for alli≤L, νai)P^G,Vars,SessId,ei≤L))e ^T

≡α(νa₁:a^L^T^,e^L^T

1,ei^T [Vars,SessId]). . .(νa_LT :a^L^T^,e^L^T

L^T,ei^T [Vars,SessId]) instr(Tren(P^G, T,ei≤L),e Vars,SessId)

≡α(νa^L^T^,e^L^T

1,ei^T :a^L^T^,e^L^T

1,ei^T [Vars,SessId]). . .(νa^L^T^,e^L^T

L^T,ei^T :a^L^T^,e^L^T

L^T,ei^T [Vars,SessId]) (instr(Tren(P^G, T,ei≤L),e Vars,SessId){a^L^T^,e^L^T

1,ei^T /a1, . . . , a^L^T^,e^L^T

1,ei^T /a_LT}) by renaming bound names

≡αinstr((νa^L^T^,e^L^T

1,ei^T ). . .(νa^L^T^,e^L^T

L^T,ei^T )Tren(P^G, T,ei≤L){ae ^L^T^,e^L^T

1,ei^T /a1, . . . , a^L^T^,e^L^T

1,ei^T /a_LT},Vars,SessId)

≡αinstr(Tren((for alli≤L, νai)P^G, T,ei≤L),e Vars,SessId)

– The case (νa)P^G can be handled similarly to the previous case. All other cases follow easily from the induction hypothesis.

Lemma 4. Given a well-typed generalized process Γ₀`P₀^G, we have:

(instr^G(P₀^G))^T⁰ ≡αinstr(Tren(P₀^G, T0,∅ ≤ ∅)).

Proof. This result comes immediately from Lemma 3 applied to instr^G(P₀^G) =

instr^G(P₀^G,∅,∅,∅ ≤ ∅).

Translation from Instrumented Processes to Clauses We use the follow-ing standard result.

Lemma 5. LetE1,E2be two sets of equations over standard clause terms. Then mgu(E1∪ E2)is defined if and only ifmgu(mgu(E2)E1)mgu(E2)is defined, and mgu(E₁∪ E₂) =mgu(mgu(E₂)E₁)mgu(E₂).

Lemma 6. Let P be an instrumented process, ρ a function that associates a clause term with each name and variable, and H a sequence of facts. Given a substitution σover the variables inρ, we have that:

[[P]](σρ)(σH)v[[P]]ρH .

Proof. The proof of this lemma is done by structural induction on the process P. We detail here the most interesting cases.

– CaseM(x).P:

[[M(x).P]](σρ)(σH)

= [[P]]((σρ)[x7→x])(σH∧message(σρ(M), x))

= [[P]](σ⁰(ρ[x7→x]))(σ⁰(H∧message(ρ(M), x)))

where we define the substitutionσ⁰=σ[x7→x]

v[[P]](ρ[x7→x])(H∧message(ρ(M), x)) by induction hypothesis v[[M(x).P]]ρH

– Caseletx=g(M1, . . . , Mn)inP elseQ:

[[letx=g(M₁, . . . , M_n)inP elseQ]](σρ)(σH)

= [[Q]](σρ)(σH)∪[

{[[P]](σ1σρ[x7→σ₁⁰p⁰])(σ1σH)|g(p⁰₁, . . . , p⁰_n)→p⁰ is in def(g)and (σ₁, σ⁰₁)is a most general pair of substitutions such that σ1σρ(Mi) =σ₁⁰p⁰_i,for eachi= 1, . . . n}

By induction hypothesis, we have [[Q]](σρ)(σH) v [[Q]]ρH. Let g(p⁰₁, . . . , p⁰_n) → p⁰ be a rule in def(g), and (σ1, σ₁⁰) be a most general pair of sub-stitutions such that σ1σρ(Mi) = σ₁⁰p⁰_i, for each i = 1, . . . n. Let σ2 = σ1σ and σ₂⁰ = σ₁⁰. For each i = 1, . . . , n, we have σ2ρ(Mi) = σ₂⁰p⁰_i. Let (σ3, σ₃⁰) be a most general pair of substitutions such that for each i = 1, . . . , n:

σ3ρ(Mi) =σ⁰₃p⁰_i. As (σ2, σ⁰₂) is such a pair (but maybe not a most general one), there exists a substitution σ4 such that σ2 = σ4σ3 and σ⁰₂ = σ4σ₃⁰. Hence we have that

[[P]](σ1σρ[x7→σ₁⁰p⁰])(σ1σH)

= [[P]](σ₄σ₃ρ[x7→σ₄σ⁰₃p⁰])(σ₄σ₃σH)

= [[P]](σ4(σ3ρ[x7→σ₃⁰p⁰]))(σ4(σ3σH)) v[[P]](σ₃ρ[x7→σ₃⁰p⁰])(σ₃σH)

by induction hypothesis. Therefore,

[[letx=g(M1, . . . , Mn)in P elseQ]](σρ)(σH) v[[Q]]ρH∪[

{[[P]](σ3ρ[x7→σ₃⁰p⁰])(σ3σH)|g(p⁰₁, . . . , p⁰_n)→p⁰ is indef(g)and(σ3, σ₃⁰)is a most general pair of substitutions such thatσ₃ρ(M_i) =σ⁰₃p⁰_i,for eachi= 1, . . . n}

v[[letx=g(M1, . . . , Mn)in P elseQ]]ρH.

– The other cases are straightforward using the induction hypothesis.

Lemma 7. We have

[[letE1 in . . . letEl in P elseQ . . . elseQ]]ρH

v[[Q]]ρH∪[[P]](mgu(E)(ρ[x17→p⁰₁, . . . , xl7→p⁰_l]))(mgu(E)H) where

– for eachi≤l,Ei isxi=gi(Mi,1, . . . , Mi,n_i);

– for eachi ≤l, xi does not occur in Q nor in Mk,j for all k= 1, . . . , l and j= 1, . . . , nk;

– for each i ≤ l, g_i(p⁰_i,1, . . . , p⁰_i,n

i) → p⁰⁰_i is the rewriting rule of g_i and pi,1, . . . , pi,n_i, p⁰_i are obtained by renamingp⁰_i,1, . . . , p⁰_i,n_i, p⁰⁰_i with fresh vari-ables;

– E={ρ(Mk,j) =pk,j |k= 1, . . . , l andj= 1, . . . , nk}.

When the equations inEcannot be unified,mgu(E)is not defined, and the second component of the union is omitted.

Proof. The proof is done by induction onl.

– Base case:l= 1.

[[letE1in P elseQ]]ρH = [[Q]]ρH∪[[P]](σρ[x17→σp⁰₁])(σH)

whereσis a most general substitution such that σρ(M1,j) =σp1,j for each j = 1, . . . , n1, assuming that σ exists. (Finding such a σ is equivalent to finding a most general pair of substitutions (σ⁰, σ⁰⁰) such thatσ⁰ρ(M1,j) = σ⁰⁰p⁰_1,j: we can define σ by σx =σ⁰⁰α⁻¹x where α is the renaming of p⁰_i,j intopi,jandxis a fresh variable introduced by this renaming, andσx=σ⁰x otherwise.) Henceσ=mgu(E) whereE ={ρ(M1,j) =p1,j |j = 1, . . . , n1} and we can conclude that

[[letE₁ inP elseQ]]ρH= [[Q]]ρH∪[[P]](mgu(E)(ρ[x₁7→p⁰₁]))(mgu(E)H) Whenmgu(E)is not defined, that is,σdoes not exist, the second component of the union is omitted.

– Inductive step. We have

[[letE1 in letE2in . . . letElin P elseQ . . . elseQelseQ]]ρH

= [[Q]]ρH∪[[letE2 in . . . letEl inP elseQ . . . elseQ]]ρ1H1

whereρ₁=mgu(E1)(ρ[x₁7→p⁰₁]),H₁=mgu(E1)H, and E1={ρ(M1,j) =p1,j |j= 1, . . . , n1}, by the base case v[[Q]]ρH∪[[Q]]ρ₁H₁∪

[[P]](mgu(E2)(ρ1[x27→p⁰₂, . . . , xl7→p⁰_l]))(mgu(E2)H1)

where E₂ = {ρ₁(M_k,j) = p_k,j | k = 2, . . . , landj = 1, . . . , n_k}, by induc-tion hypothesis, assuming thatmgu(E₁)andmgu(E₂)are defined. We have [[Q]]ρ₁H₁ = [[Q]](mgu(E₁)ρ)(mgu(E₁)H) since x₁ does not occur in Q, so [[Q]]ρ1H1v[[Q]]ρH by Lemma 6.

LetE₂⁰ = {ρ(Mk,j) = pk,j | k = 2, . . . , landj = 1, . . . , nk}. The variables of p_k,j (k ≥ 2) are fresh, so they are untouched by mgu(E1), so we have E2=mgu(E1)E₂⁰ andE =E1∪ E₂⁰, so

mgu(E₂)mgu(E₁) =mgu(mgu(E₁)E₂⁰)mgu(E₁) =mgu(E₁∪ E₂⁰) =mgu(E) by Lemma 5. Moreover, the variables of p⁰₂, . . . , p⁰_l are fresh, so they are untouched bymgu(E1). Hence

mgu(E2)(ρ1[x27→p⁰₂, . . . , xl7→p⁰_l])

=mgu(E2)mgu(E1)(ρ[x17→p⁰₁, x27→p⁰₂, . . . , xl7→p⁰_l])

=mgu(E)(ρ[x17→p⁰₁, . . . , x_l7→p⁰_l])

andmgu(E₂)H₁=mgu(E₂)mgu(E₁)H =mgu(E)H. Therefore, [[letE1 in letE2in . . . letElin P elseQ . . . elseQelseQ]]ρH

v[[Q]]ρH∪[[P]](mgu(E)(ρ[x₁7→p⁰₁, . . . , x_l7→p⁰_l]))(mgu(E)H) As before, when mgu(E) is not defined, that is, mgu(E₂)mgu(E₁) is not defined, the second component of the union is omitted.

From this lemma, we obtain the following result for the special case of the decomposition of data constructors.

Corollary 3. Let f be a data constructor of arity n and f₁⁻¹, . . . , f_n⁻¹ be its associated destructors.

[[letx1=f₁⁻¹(M)in . . . letxn=f_n⁻¹(M)inP elseQ . . . elseQ]]ρH v[[Q]]ρH∪[[P]](mgu(E)(ρ[x17→v1, . . . , xn7→vn]))(mgu(E)H)

wherex1, . . . , xn do not occur inQnor inM, andE={f(v1, . . . , vn) =ρ(M)}.

Whenmgu(E)is not defined, the second component of the union is omitted.

Proof. By Lemma 7, we obtain

[[letx1=f₁⁻¹(M)in . . . letxn =f_n⁻¹(M)inP elseQ . . . elseQ]]ρH v[[Q]]ρH∪[[P]](mgu(E⁰)(ρ[x₁7→v_1,1, . . . , x_n7→v_n,n]))(mgu(E⁰)H) where E⁰ = {ρ(M) = f(vk,1, . . . , vk,n) | k = 1, . . . , n} and the variables vk,j

(k= 1, . . . , n,j= 1, . . . , n) are fresh. We have mgu(E⁰)vk,j =mgu(E⁰)vk⁰,j for allk, k⁰, j, so for allj= 1, . . . , n, we can rename the variablesvk,j for allk into the same variablevj. After this renaming, we obtain the announced result.

Lemma 8. Suppose that the variables ofpat₁, . . . ,pat_n are pairwise distinct and fresh (that is, they do not occur inρ,H,M₁, . . . ,M_n, andQ).

[[letpat₁=M1 in . . . letpat_n=Mn in P elseQ . . . elseQ]]ρH

v[[Q]]ρH∪[[P]](mgu(E)(ρ[x7→x|xoccurs inpat₁, . . . ,pat_n]))(mgu(E)H) whereE ={pat_i=ρ(M_i)|i= 1, . . . , n}.

Proof. The proof is done by induction on the total size of the patternspat₁, . . . , pat_n.

– Case 1: there is a single patternpat =x.

[[letx=M inP elseQ]]ρH

= [[letx=id(M)in P elseQ]]ρH

= [[Q]]ρH∪[[P]](mgu({ρ(M) =y})(ρ[x7→y]))(mgu({ρ(M) =y})H) wherey is a fresh variable and the rewrite rule for destructor id is renamed intoid(y)→y (see the base case of Lemma 7).

v[[Q]]ρH∪[[P]](mgu({ρ(M) =x})(ρ[x7→x]))(mgu({ρ(M) =x})H) by renamingxinto y sincexand y do not occur in ρ, ρ(M), andH.

– Case 2: there is a single patternpat =f(pat₁, . . . ,pat_n).

[[letf(pat₁, . . . ,pat_n) =M inP elseQ]]ρH

= [[letx1=f₁⁻¹(M)in . . . letxn =f_n⁻¹(M)in

letpat₁=x1in . . . letpat_n=xn in P elseQ . . . elseQ elseQ . . . elseQ]]ρH

wherex1, . . . , xn are fresh variables

v[[Q]]ρH∪[[letpat₁=x₁ in . . . letpat_n=x_n inP elseQ . . . elseQ]]

(mgu(E)(ρ[x17→v1, . . . , xn7→vn]))(mgu(E)H) whereE={f(v1, . . . , vn) =ρ(M)}, by Corollary 3 v[[Q]]ρH∪[[Q]]ρ⁰H⁰∪

[[P]](mgu(E⁰)(ρ⁰[x7→x|xoccurs inpat₁, . . . ,pat_n]))(mgu(E⁰)H⁰) where ρ⁰ =mgu(E)(ρ[x₁ 7→v₁, . . . , x_n 7→v_n]), H⁰ =mgu(E)H, andE⁰ = {pat₁=ρ⁰(x1), . . . ,pat_n=ρ⁰(xn)}, by induction hypothesis (since the total size ofpat₁, . . . ,pat_n is less than the size off(pat₁, . . . ,pat_n)).

Asx₁, . . . , x_n do not appear inQ,[[Q]]ρ⁰H⁰ = [[Q]](mgu(E)ρ)(mgu(E)H)v [[Q]]ρH, by Lemma 6.

We have E⁰ = {pat_i = mgu(E)v_i | i = 1, . . . , n} = mgu(E){pat_i = v_i | i = 1, . . . , n}, so by Lemma 5, mgu(E⁰)mgu(E) = mgu({f(v₁, . . . , v_n) = ρ(M)} ∪ {pat_i =vi | i= 1, . . . , n}) =mgu({f(pat₁, . . . ,pat_n) =ρ(M)} ∪ {pat_i = vi | i = 1, . . . , n}). Let E⁰⁰ = {f(pat₁, . . . ,pat_n) = ρ(M)}. Then

we have mgu(E⁰)mgu(E) = (mgu(E⁰⁰))[v_i 7→mgu(E⁰⁰)pat_i]. Therefore we obtain that:

[[letf(pat₁, . . . ,pat_n) =M inP elseQ]]ρH v[[Q]]ρH

∪[[P]](mgu(E⁰⁰)(ρ[x7→x|xoccurs inpat₁, . . . ,pat_n]))(mgu(E⁰⁰)H) since the variablesv1, . . . , vn do not occur inρandH, and the variablesx1, . . . , xn can be removed from the environment since they do not occur inP. – Case 3: there are several patterns.

[[letpat₁=M1 in . . . letpat_n=Mn inP elseQ . . . elseQ]]ρH

v[[Q]]ρH∪[[letpat₂=M₂ in . . . letpat_n =M_n inP elseQ . . . elseQ]]

(mgu(E1)(ρ[x7→x|xoccurs inpat₁]))(mgu(E1)H)

whereE₁={pat₁=ρ(M₁)}, by induction hypothesis applied to pat₁ v[[Q]]ρH∪[[Q]]ρ⁰H⁰∪

[[P]](mgu(E2)(ρ⁰[x7→x|xoccurs inpat₂, . . . ,pat_n]))(mgu(E2)H⁰) where ρ⁰ = mgu(E1)(ρ[x 7→ x | xoccurs inpat₁]), H⁰ = mgu(E1)H, and E2={pat_i =ρ⁰(Mi)|i= 2, . . . , n}, by induction hypothesis applied topat₂, . . . ,pat_n.

Since the variables ofpat₁do not occur in the processQ, we have[[Q]]ρ⁰H⁰= [[Q]](mgu(E1)ρ)(mgu(E1)H)v[[Q]]ρH by Lemma 6.

Let E₂⁰ = {pat_i = ρ(M_i) | i = 2, . . . , n} and E = {pat_i = ρ(M_i) | i = 1, . . . , n}. Since the variables ofpat_i for i≥2 do not occur inE₁, we have mgu(E2)mgu(E1) =mgu(mgu(E1)E₂⁰)mgu(E1) =mgu(E1∪ E₂⁰) =mgu(E) by Lemma 5. So

mgu(E2)(ρ⁰[x7→x|xoccurs inpat₂, . . . ,pat_n])

=mgu(E2)mgu(E1)(ρ[x7→x|xoccurs inpat₁, . . . ,pat_n])

=mgu(E)(ρ[x7→x|xoccurs inpat₁, . . . ,pat_n]) andmgu(E2)H⁰=mgu(E2)mgu(E1)H =mgu(E)H. Therefore,

[[letpat₁=M1 in . . . letpat_n=Mn inP elseQ . . . elseQ]]ρHv[[Q]]ρH

∪[[P]](mgu(E)(ρ[x7→x|xoccurs inpat₁, . . . ,pat_n]))(mgu(E)H) Lemma 9. LetΓ_P `M^G be a well-typed pattern, ρ^G a function that associates a clause term with each name and variable, possibly with indices, andΓ an envi-ronment for generalized Horn clauses such thatΓ_P, Γ `ρ^G. ThenΓ `ρ^G(M^G) Proof. We detail here the three interesting cases.

– Case M^G = x

eι. Since ΓP typesx

eι, we have two judgments x_ : Le ∈ ΓP

and Γ_P ` eι : L. From the definition ofe Γ_P, Γ ` ρ^G, if {x

ei 7→ p^G} ∈ ρ^G, then Γ,ei : Le ` p^G. Moreover, as ΓP ` eι : L, we havee Γ ` eι : L. Hencee ρ^G(M^G) =p^G{eι/ei}and Γ `ρ^G(M^G).

– Case M^G = a. From the definition of Γ ` ρ^G, if {a 7→ p^G} ∈ ρ^G, then Γ `p^G=ρ^G(M^G).

– CaseM^G =aι. SinceΓP typesaι, we have two judgmentsa_ : [1, L]∈ΓP

andΓP `i: [1, L]. From the definition of ΓP, Γ ` ρ^G, if {ai 7→p^G} ∈ρ^G, then Γ, i : [1, L] ` p^G. Moreover, as Γ_P ` i : [1, L], we have Γ `i : [1, L].

Henceρ^G(M^G) =p^G{ι/i} andΓ `ρ^G(M^G).

We writeT⁰extT to mean thatT⁰is an extension of the environmentT. Given a type environment ΓP for processes and a type environmentΓ for generalized Horn clauses, we define{x

ei7→p^G}^T ={x

ve7→p^GT^[e^i7→^e^v]|ev≤L}e whenx_ :Le∈ Γ,{a7→p^G}^T ={a7→p^GT}, and{ai7→p^G}^T ={av7→p^GT^[i7→v] |v≤L}when a_: [1, L]∈ΓP. We extend this definition naturally toρ^GT.

Lemma 10. LetΓP `P^Gbe a well-typed instrumented generalized process,ρ^Ga function that associates a clause term with each name and variable, possibly with indices,H^G a sequence of facts,E a set of equations, and Γ is an environment for generalized Horn clauses such that:

– Γ `H^G; – Γ ` E;

– ΓP, Γ `ρ^G. Then

[[P^GT]](mgu(E^T)ρ^GT)(mgu(E^T)H^GT)v [

T⁰extT

([[P^G]]ρ^GH^GEΓ)^T⁰

and the clauses in the right hand side are well-typed.

Proof. The proof is done by structural induction on the process P^G. Let ρ = mgu(E^T)ρ^GT and H = mgu(E^T)H^GT, and let us show that [[P^GT]]ρH v S

T⁰extT([[P^G]]ρ^GH^GEΓ)^T⁰. – Caseout(M^G, N^G).P^G:

[[(out(M^G, N^G).P^G)^T]]ρH

= [[out(M^GT, N^GT)i.P^GT]]ρH

= [[P^GT]]ρH∪ {(mgu(E^T)H^GT

⇒message(mgu(E^T)ρ^GT(M^GT),mgu(E^T)ρ^GT(N^GT))}

= [[P^GT]]ρH∪({Γ `H^G∧ E ⇒message(ρ^G(M^G), ρ^G(N^G))})^T

v [

T⁰extT

([[P^G]]ρ^GH^GEΓ)^T⁰∪ [

T⁰extT

({Γ `H^G∧ E ⇒message(ρ^G(M^G), ρ^G(N^G))})^T⁰ by induction hypothesis and using thatT is an extension of itself

v [

T⁰extT

([[out(M^G, N^G).P^G]]ρ^GH^GEΓ)^T⁰

– Casein(M^G, x).P^G:

[[(in(M^G, x).P^G)^T]]ρH= [[in(M^GT, x).P^GT]]ρH

= [[P^GT]](ρ[x7→x])(H∧message(ρ(M^GT), x)) The right-hand side of the theorem develops in

[

T⁰extT

([[in(M^G, x).P^G]]ρ^GH^GEΓ)^T⁰ = [

T⁰extT

([[P^G]]ρ^G₁H₁^GEΓ1)^T⁰

whereρ^G₁ =ρ^G[x7→x],H₁^G=H^G∧message(ρ^G(M^G), x), and Γ1=Γ, x_: [ ]. We show that ρ[x7→x] =mgu(E^T)ρ^GT₁ :

mgu(E^T)ρ^GT₁ =mgu(E^T)ρ^GT[x7→x] =ρ[x7→x]

andH∧message(ρ(M^GT), x) =mgu(E^T)H₁^GT:

mgu(E^T)H₁^GT =mgu(E^T)(H^G∧message(ρ^G(M^G), x))^T

=mgu(E^T)H^GT ∧mgu(E^T)(message(ρ^GT(M^GT), x)

=H∧message(mgu(E^T)ρ^GT(M^GT), x)

=H∧message(ρ(M^GT), x)

LetΓ_P⁰ the environment that types P^G, Γ_P⁰ =ΓP, x_ : [ ]. Before applying the induction hypothesis we need to show thatΓ_P⁰, Γ₁ ` ρ^G₁ and Γ₁ ` H₁^G (clearly,Γ₁ ` E). SinceΓ_P, Γ `ρ^G, we have Γ_P⁰, Γ₁`ρ^G. For the new map [x7→x]∈ρ^G₁ we have thatx_{_}: [ ]∈Γ_P⁰ andΓ₁`x. HenceΓ_P⁰, Γ₁`ρ^G₁. Since Γ ` H^G, we have Γ1 ` H^G. From Lemma 9 we have that Γ ` ρ^G(M^G), as ΓP, Γ ` ρ^G and ΓP ` M^G. Finally Γ1 ` x. Hence Γ1 ` message(ρ^G(M^G), x), and thus Γ1 ` H₁^G. Therefore, we can apply the in-duction hypothesis and conclude.

– Case0:[[0^T]]ρH=∅=S

T⁰extT([[0]]ρ^GH^GEΓ)^T⁰. – CaseP^G|Q^G:

[[(P^G|Q^G)^T]]ρH = [[P^GT |Q^GT]]ρH= [[P^GT]]ρH∪[[Q^GT]]ρH

v [

T⁰extT

([[P^G]]ρ^GH^GEΓ)^T⁰∪ [

T⁰extT

([[Q^G]]ρ^GH^GEΓ)^T⁰

v [

T⁰extT

([[P^G|Q^G]]ρ^GH^GEΓ)^T⁰

– Case!^sP^G:

[[(!^sP^G)^T]]ρh= [[!^sP^GT]]ρH= [[P^GT]](ρ[s7→s])H

v [

T⁰extT

([[P^G]](ρ^G[s7→s])H^GEΓ)^T⁰

v [

T⁰extT

([[!^sP^G]]ρ^GH^GEΓ)^T⁰

– CaseΠ_i≤LP:

[[(Π_i≤LP)^T]]ρH = [[P^GT^[i7→1]|. . . |P^GT^[i7→L^T^]]]ρH

= [[P^GT^[i7→1]]]ρH∪ · · · ∪[[P^GT^[i7→L^T^]]]ρH

By induction hypothesis,[[P^GT^[i7→v]]]ρH vS

T⁰extT[i7→v]([[P^G]]ρ^GH^GE(Γ, i : [1, L]))^T⁰ for each v∈ {1, . . . , L^T}. Therefore

[[(Π_i≤LP)^T]]ρHv [

T⁰extT[i7→1]

([[P^G]]ρ^GH^GE(Γ, i: [1, L]))^T⁰∪ · · · ∪

[

T⁰extT[i7→L^T]

([[P^G]]ρ^GH^GE(Γ, i: [1, L]))^T⁰

v [

T⁰extT

([[P^G]]ρ^GH^GE(Γ, i: [1, L]))^T⁰

v [

T⁰extT

([[Π_i≤LP^G]]ρ^GH^GEΓ)^T⁰

sinceT[i7→v]is an extension ofT for each v∈ {1, . . . , L^T}.

– Case(for alli≤L, νai :a^L,e^L

i,ei [x1, . . . , xn, s1, . . . , sn⁰])P^G: [[((for alli≤L, νai:a^L,e^L

i,ei [x1, . . . , xn, s1, . . . , sn⁰])P^G)^T]]ρH

= [[(νa₁:a^L^T^,e^L^T

1,ei^T [x₁, . . . , x_n, s₁, . . . , s_n⁰]). . . (νa_LT :a^L^T^,e^L^T

L^T,ei^T [x1, . . . , xn, s1, . . . , sn⁰])P^GT]]ρH

= [[P^GT]]ρ1H

where

ρ1=ρ[a17→a^L^T^,e^L^T

1,ei^T [ρ(x1), . . . , ρ(xn), ρ(s1), . . . , ρ(sn⁰)], . . . , a_LT 7→a^L^T^,e^L^T

L^T,ei^T [ρ(x₁), . . . , ρ(x_n), ρ(s₁), . . . , ρ(s_n⁰)]]. The right-hand side of the theorem develops in

[

T⁰extT

([[(for alli≤L, νai :a^L,e^L

i,ei [x1, . . . , xn, s1, . . . , sn⁰])P^G]]ρ^GH^GEΓ)^T⁰

= [

T⁰extT

([[P^G]]ρ^G₁H^GEΓ)^T⁰

whereρ^G₁ =ρ^G[ai7→a^L,e^L ρ^G₁. We can then apply the induction hypothesis and conclude.

– Case(νa)P^G: this case is similar to the previous one.

– Case let for allei ≤ L, xe

ei = g(M₁^G, . . . , M_n^G)in P^G elseQ^G: let g(p1, . . . , pn)→p⁰be the rewrite rule for the destructorg. We suppose that the tuples of indicesev ≤Le^T are indexed by1, . . . , l, that is, we define {ev₁, . . . ,ve_l} = mgu(E1)does not exist, the second component of the union is omitted, and the rest of the proof can easily be adapted.) The right-hand side of the theorem develops in

rule with fresh variables with indicesei: y⁰ Let Γ_P⁰ the environment that types P^G: by the typing rules we have that Γ_P⁰ =ΓP, x_ :L. Before applying induction we need to show thate Γ_P⁰, Γ⁰ `

This means that each equation inE⁰ is well typed in Γ⁰; moreover Γ⁰ ` E becauseΓ⁰ extends Γ andΓ ` E by hypothesis. ThusΓ⁰` E ∪ E⁰.

We can then apply the induction hypothesis, which yields [[P^GT]](mgu(αE₁)(ρ[x

ev1 7→αp⁰₁, . . . , x

vel 7→αp⁰_l]))(mgu(αE₁)H)

v [

T⁰extT

([[P^G]](ρ^G[x

ei7→p^0G])H^G(E ∪ E⁰)Γ⁰)^T⁰ and[[Q^GT]]ρHvS

T⁰extT([[Q^G]]ρ^GH^GEΓ)^T⁰. Moreover,

[[P^GT]](mgu(E1)(ρ[x

ev1 7→p⁰₁, . . . , x

evl7→p⁰_l]))(mgu(E1)H) v[[P^GT]](mgu(αE1)(ρ[x

ve₁ 7→αp⁰₁, . . . , x

ev_l7→αp⁰_l]))(mgu(αE1)H) (These two sets of clauses are in fact equal up to renaming of variables, by construction.)

Hence we can conclude that:

[[(let for allei≤L, xe

ei=g(M₁^G, . . . , M_n^G)inP^G elseQ^G)^T]]ρH v [

T⁰extT

([[let for allei≤L, xe

ei=g(M₁^G, . . . , M_n^G)inP^G elseQ^G]]ρ^GH^GEΓ)^T⁰

– Caselet for allei≤L,e pat^G =M^G inP^G elseQ^G: as in the previous case, we suppose that the tuples of indicesev≤Le^T are indexed by1, . . . , l, that is, we define{ev₁, . . . ,ev_l}={e1, . . . ,Le^T}.

[[(let for allei≤L,e pat^G =M^G in P^G elseQ^G)^T]]ρH

= [[letE1 in . . . letEl inP^GT elseQ^GT . . . elseQ^GT]]ρH whereE_i is the equationpat^GT^[e^i7→^e^vⁱ^]=M^GT^[e^i7→^e^vⁱ^]. v[[Q]]ρH∪[[P]]ρ⁰H⁰

by Lemma 8, where E1 = {pat^GT⁰⁰ = ρ(M^GT⁰⁰) | T⁰⁰ = T[ei 7→ ev],ve ≤ Le^T}, ρ⁰ =mgu(E₁)(ρ[x7→ x| xoccurs inpat^GT^[e^i7→^e^v],ev ≤ Le^T]), and H⁰ = mgu(E₁)H, assuming thatmgu(E₁)exists. (Whenmgu(E₁)does not exist, the second component of the union is omitted, and the rest of the proof can easily be adapted.)

The right-hand side of the theorem develops in:

[

T⁰extT

([[let for allei≤L,e pat^G=M^G in P^G elseQ^G]]ρ^GH^GEΓ)^T⁰

= [

T⁰extT

([[Q]]ρ^GH^GEΓ)^T⁰∪

[[P]](ρ^G[x

ei⁰ 7→x

ei⁰ |x

ei⁰ occurs inpat^G])H^G(E ∪ E⁰)Γ⁰)^T⁰

whereE⁰ =V

ei≤Lepat^G .

=ρ^G(M^G)andΓ⁰ isΓ extended for the variables oc-curring inpat^G. More precisely, if the typing rule for the processlet for allei≤ L,e pat^G =M^G inP^G elseQ^G hasi1 : [1, L1], . . . , ih : [1, Lh] ` pat^G Γ⁰⁰ Let Γ_P⁰ the environment that types P^G: by the typing rules we have that Γ_P⁰ =ΓP, Γ_P⁰⁰, whereei:Le `pat^G Γ_P⁰⁰. Before applying induction we need

– CasechooseL inP^G: [[(chooseLin P^G)^T]]ρH

= [[P^GT^[L7→1]+· · ·+P^GT^[L7→n]+· · ·]]ρH

= [[P^GT^[L7→1]]]ρH∪ · · · ∪[[P^GT^[L7→n]]]ρH∪ · · ·

v [

T⁰extT[L7→1]

([[P^G]]ρ^GH^GEΓ)^T⁰∪ · · · ∪ [

T⁰extT[L7→n]

([[P^G]]ρ^GH^GEΓ)^T⁰∪ · · ·

v [

T⁰extT

([[chooseLinP^G]]ρ^GH^GEΓ^T⁰)

– Casechoosek≤LinP^G:

[[(choosek≤LinP^G)^T]]ρH

= [[P^GT^[k7→1]+· · ·+P^GT^[k7→L^T^]]]ρH

= [[P^GT^[k7→1]]]ρH∪ · · · ∪[[P^GT^[k7→L^T^]]]ρH

v [

T⁰extT[k7→1]

([[P^G]]ρ^GH^GE(Γ, k: [1, L]))^T⁰∪ · · · ∪

[

T⁰extT[k7→L^T]

([[P^G]]ρ^GH^GE(Γ, k: [1, L]))^T⁰

v [

T⁰extT

([[choosek≤L inP^G]]ρ^GH^GEΓ^T⁰)

– Casechooseφ :L₁× · · · ×L_h →L⁰ in P^G: this case is similar to previous

one.

Combining the results From the previous results, we easily obtain Theorem 3.

Proof (of Theorem 3). By Lemma 10, ([[P₁^G]]ρ₀∅∅Γ₀)^T =S

T([[P₁^G]]ρ₀∅∅Γ₀)^T w [[P₁^GT⁰]]ρ0∅, whereP₁^G = instr^G(P₀^G). By Lemma 4,instr(P₀⁰) = instr(Tren(P₀^G, T0,∅ ≤ ∅)) ≡α instr^G(P₀^G)^T⁰ = P₁^GT⁰, so we have ([[instr^G(P₀^G)]]ρ0∅∅Γ0)^T w [[instr(P₀⁰)]]ρ0∅since the translation to Horn clauses [[·]]is invariant by renaming of bound names.

Moreover, for each clauseR in{att(a[ ])|a∈S} ∪ {(Rn), (Rf), (Rg), (Rl), (Rs)} except the clauses (Rf) and (Rg) for lists of fixed length, R is also a generalized Horn clause and we have {R}^T = {R}. The clauses (Rf) for lists of fixed length are in {R^G}^T = {att(x1)∧ · · · ∧att(xn) ⇒ att(hx1, . . . , xni) | n∈ N}, where R^G =(Rf-list). The clauses (Rg) for lists of fixed length are in {R^G}^T ={att(hx1, . . . , x_ni)⇒att(x_v)|n∈N, v≤n} whereR^G=(Rg-list).

So we obtainR^GT_PG

0,S w RP₀⁰,S.

In document From the Applied Pi Calculus to Horn Clauses for Protocols with Lists (Sider 23-42)