英语论文网

Abstract
This is the second of two papers in which we present the -calculus, a calculus of mobile pro cesses. We provide a detailed presentation of some of https://www.51lunwen.org/liuxuelunwendx/the theory of the calculus develop ed to date, and in particular we establish most of the results stated in the companion paper.

Introduction

This is the second of two papers in which we present the -calculus, a calculusof mobile pro cesses. The companion paper 2] contains an intro duction tothe calculus through a sequence of examples, together with statements ofmany results ab out it. The purp ose of the present pap er is to provide adetailed presentation of some of the theory of the calculus develop ed to date,and in particular to establish most of the results stated in the companionpap er. Once the motivation and intuition for the -calculus are understo o d,with the help of 2], the present pap er serves as a self-contained developmentof the theory. To achieve this we have found it necessary to rep eat somematerial from the companion pap er.

Section 1 contains a description of the syntax of agents and a discursivepresentation代写留学生论文of the transitional semantics. In Section 2 we present and mo-tivate the de nitions of strong bisimulation and strong bisimilarity, strongequivalence, and a useful family of indexed equivalences. Section 3 containsa series of prop erties of strong bisimilarity, while prop erties of strong equiv-alence and indexed equivalences are develop ed in Section 4. A completeaxiomatization for nite agents is presented in Section 5.

There are many p oints of interest in the detailed development of the the-ory. However, in order to reduce the length of the pap er and to avoid givingthe impression that the theory generally is more complicated or surprisingthan it in fact is, we do not include complete pro ofs of all results. Instead, theApp endix contains extracts giving a taste of the techniques used. Completepro ofs may b e found in 3].

1 Agents and their transitional semantics
1.1 Agents
We rst recapitulate some of the de nitions and the notation from our com-panion pap er. Assume an in nite set N of names and use x; y ; z ; w ; v ; u as metavariables over names. We assume also a set of agent identi ers. Each agent identi er A has a nonnegative arity. De nition 1 The set of agents is de ned as follows (we use P ; Q; R as metavariables over agents):The order of precedence among the op erators is the order listed ab ove. Fora description of the intended interpretation of agents see 2]. In that pap erwe also use a general summation op erator ; in the present pap er we will b esatis ed with nullary and binary summation (0 and +) and regard generalsummation as a derived op erator.

De nition 2 In each agent of one of the forms x(y ): P and (y )P theo ccurrence of y within parentheses is a binding o ccurrence, and in each casethe scop e of the o ccurrence is P . An o ccurrence of y in an agent is saidto b e free if it do es not lie within the scop e of a binding o ccurrence of y .The set of names o ccurring free in P is denoted fn(P ). We sometimes writefn as an abbreviation for fn .

De nition 3 A de ning equation for an agent identi er A of arity n is ofthe formA(x1; . . . ; xn)def= Pwhere the xiare pairwise distinct and fn(P ) fx1; .本论文由英语论文网提供整理，提供论文代写，英语论文代写，代写论文，代写英语论文，代写留学生论文，代写英文论文，留学生论文代写相关核心关键词搜索。