Encoding an Object Calculus into Interaction Nets

We propose an encoding of an object calculus into interaction nets in two stages. First, we make the calculus fully explicit, i.e. with explicit substitutions, duplications and erasures. Then, we use this explicit calculus to produce an interaction net encoding of objects.     

Coding Mobile Synchronizing Petri Nets into Rewriting Logic

Mobile Synchronizing Petri Nets (MSPN's) are a model for mobility and coordination based on coloured Petri Nets, in which systems are composed of a collection of (possibly mobile) hardware devices and mobile agents, both modelled homogenously. In this paper we approach their verification, for which we have chosen to code MSPN's into rewriting logic. In order to obtain a representation of MSPN systems by means of a rewrite theory, we develop a class of them, that we call ν-Abstract Petri nets (ν-APN's), which are easily representable in that framework. Moreover, the obtained representation provides a local mechanism for fresh name generation. Then we prove that, even if ν-APN's are a particular class of MSPN systems, they are strong enough to capture the behaviour of any MSPN system. We have chosen Maude to implement ν-APN's, as well as the translation from MSPN's to ν-APN's, for which we make intensive use of its reflective features.     

A Rewriting Calculus for Cyclic Higher-order Term Graphs

Introduced at the end of the nineties, the Rewriting Calculus (ρ-calculus, for short) is a simple calculus that fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the obtained structured results are first class objects of the calculus. The evaluation mechanism, generalizing beta-reduction, strongly relies on term matching in various theories.In this paper we propose an extension of the ρ-calculus, handling graph like structures rather than simple terms. The transformations are performed by explicit application of rewrite rules as first class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.The calculus over terms is naturally generalized by using unification constraints in addition to the standard ρ-calculus matching constraints. This therefore provides us with the basics for a natural extension of an explicit substitution calculus to term graphs. Several examples illustrating the introduced concepts are given.     

Package Duplication in Interaction Nets and Weak Head Reduction in the lambda-calculus

We present a simple implementation of weak head reduction in the λ-calculus with interaction nets using package duplication.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

结合Petri网和Pi演算的协同业务过程建模

协同业务过程使组织业务过程同其他组织的业务过程间进行交互和协作,以形成相对稳定的过程视图,从而满足共同的商业目标。为确保过程模型的正确性,采用形式化方法对协同业务过程进行建模变得越来越重要。将Petri网和Pi演算进行交叉应用,提出了一种协同业务过程的建模方法。该方法采取关注点分离的原则,一方面,从控制流角度,针对协同业务过程面向流的特点,提出公共视图,使用Petri网直观描述参与协同组织的业务过程的静态结构和状态转换;另一方面,从交互角度,针对协同业务过程面向协作的特点,提出协作视图,使用Pi演算描述业务过程间的交互。为建立Petri网和Pi演算间的关联,提出了进程标号迁移系统。与传统的业务过程建模方法相比,该方法能有效支持协同业务过程具有的个性化特征。     

Macros for Interaction Nets: A Conservative Extension of Interaction Nets

We propose a conservative extension of interaction nets which offers enriched pattern-matching facilities. The extension is conservative in the sense that it can be implemented inside standard interaction nets, and thus can be seen as a system of macros. Consequently, we are guaranteed to keep all the good properties of interaction nets, in particular strong confluence. We see this extension as a crucial step towards using interaction nets as a programming language, which remains a relatively unexplored area. One significant feature of the extension presented here is that, in contrast to other extensions presented previously, we essentially follow the syntax and spirit of interaction nets, and moreover the extension lives at the same level.     

k-选择网和Pi演算的表达能力

文中定义了Petri网的一子类系列:k-选择网,它形成一个后类包含前类的Petri网子类的无穷序列,证明了此无穷序列的并集等于Petri网类,自由选择网是k=1的k-选择网,即1-选择网.在证明自由选择网系统可以用Pi演算表达的基础上,文中进一步证明了所有2-选择网系统可以用Pi演算表达.     

From Chemical Rules to Term Rewriting

In this paper, rule-based programming is explored in the field of automated generation of chemical reaction mechanisms. We explore a class of graphs and a graph rewriting relation where vertices are preserved and only edges are changed. We show how to represent cyclic labeled graphs by decorated labeled trees or forests, then how to transform trees into terms. A graph rewriting relation is defined, then simulated by a tree rewriting relation, which can be in turn simulated by a rewriting relation on equivalence classes of terms. As a consequence, this kind of graph rewriting can be implemented using term rewriting. This study is motivated by the design of the GasEl system for the generation of kinetics reactions mechanisms. In GasEl, chemical reactions correspond to graph rewrite rules and are implemented by conditional rewriting rules in ELAN. The control of their application is done through the ELAN strategy language.     

Towards a Programming Language for Interaction Nets

Interaction nets were introduced almost 15 years ago. Since then they have been put forward as both a graphical programming paradigm and as an intermediate language into which we can compile other languages. Whichever way we use interaction nets, a problem remains in that the language is very primitive. Drawing an analogy with functional programming, we have the λ-calculus but we are missing the functional programming language: syntactic sugar, language constructs, data-structures, etc. The purpose of this paper is to make a first step towards defining such a programming language for interaction nets.     

Interaction Nets With Nested Pattern Matching

Reduction rules in Interaction Nets are constrained to pattern match exactly one argument at a time. Consequently, a programmer has to introduce auxiliary rules to perform more sophisticated matches. We propose an extension of Interaction Nets which facilitates nested pattern matching on interaction rules. We then define a practical compilation scheme from extended rules to pure interaction rules. We achieve a system that provides convenient ways to express Interaction Net programs without defining auxiliary rules.     

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.     

泛函程序设计语言实现中的图归约演算

本文叙述了在Ｖｏｎ Ｎｅｕｍａｎｎ机器上实现基于λ演算，ＳＫＩ演算的泛函程序设计语言所采用的图归约演算。ＳＫＩ－Ｇ演算是ＳＫＩ演算的图形表示，是基于图形的形式归约系统，面向机器实现，是实现高阶，引用透明，归约语义，全惰性泛函程序设计语言的主要技术基础。     

基于重写逻辑的Web服务事务处理形式化描述

Web服务的事务处理研究越来越活跃,对于Web服务中的长、短事务进行形式化描述与验证是很重要的,但目前还没有成熟的方法．该文提出了一种基于重写逻辑的Web服务事务处理形式化描述方法,采用重写逻辑工具Maude,对于描述Web事务的细胞膜演算,给出一个事务处理的通用框架,采用重写逻辑中的规则描述事务的具体活动,并且引入事务补偿机制刻画长事务的运行;并应用该模型形式化描述文中的Web事务经典例子,得到一个可执行的重写逻辑模型,便于以后采用Maude线性时序逻辑分析器进行形式化分析．     

Logical Semantics for the Rewriting Calculus

The Rewriting Calculus has been proposed as a language for defining term rewriting strategies. Rules are explicitly represented as terms, and are applied explicitly to other terms to transform them. Sets of rules may be applied to (sets of) terms non-deterministically to obtain sets of results. Strategies are implemented as rules which accept other rules as arguments and apply them in certain ways. This paper describes work in progress to strengthen the Rewriting Calculus by giving it a logical semantics. Such a semantics can provide crucial guidance for studying the language and increasing its expressive power. The latter is demonstrated by adding support to the Rewriting Calculus for what we call higher-form rewriting, where rules rewrite other rules. The logical semantics used is based on ordered linear logic. The paper develops the ideas through several examples.     

Using Term-Graph Rewriting Models to Analyse Relative Space Efficiency

Space leaks are a common operational problem in programming languages with automated memory man-agement. Graph rewriting is a natural model of operational behaviour. This paper summarises a PhD thesis which gives a graph-rewriting framework suitable for modelling language implementations and proof techniques for determining the presence or absence of leaks. The approach is to model implementations as graph evaluators with garbage collectors. An evaluator may leak relative to another evaluator, with respect to a translation between their states. Leaks are classified according to their cause and the behaviour which exposes them.Graphs naturally model state size, but we argue that this is too concrete. Accurate evaluators are introduced which allow for a more abstract model in which initial program size is ignored. Evaluators are compared by defining a translation between graphs. Space-safe translations, and non-standard garbage collectors, are defined as another kind of term-graph rewrite system. Leaky evaluators are detected by a proof method which searches for graphs whose evaluation trace is a self-feeding rule sequence.     

Termination Proofs for String Rewriting Systems via Inverse Match-Bounds

Annotating a letter by a number, one can record information about its history during a rewrite derivation. In each rewrite step, numbers in the reduct are updated depending on the redex numbering. A string rewriting system is called match-bounded if there is a global upper bound to these numbers. Match-boundedness is known to be a strong sufficient criterion for both termination and preservation of regular languages. We show that the string rewriting systems whose inverse (left and right hand sides exchanged) is match-bounded, also have exceptional properties, but slightly different ones. Inverse match-bounded systems need not terminate; they effectively preserve context-free languages; their sets of normalizable strings and their sets of immortal strings are effectively regular. These languages can be used to decide the normalization, the uniform normalization, the termination and the uniform termination problem for inverse match-bounded systems. We also prove that the termination problem is decidable in linear time, and that a certain strong reachability problem is decidable, thereby solving two open problems of McNaughton’s. Like match-bounds, inverse match-bounds entail linear derivational complexity on the set of terminating strings.     

Tutorial and Survey Articles: An introduction to Petri Nets

This paper describes the fundamental concepts and characteristics of Petri nets (PNs) that make them a significant tool for modeling and analyzing asynchronous systems with concurrent and parallel activities and follows the extensions that improved the implementation capabilities of the original PNs.

Their first and most relevant extension was time modeling, a vital aspect of system performances not considered in the original version. There are several possibilities for introducing time in PNs. Among them, a technique that associates time with places is presented in some detail. As PNs tend to become cumbersome and time consuming when large and complex systems are involved, a method for decomposing timed PNs of open queuing networks is reviewed here.

Though initially developed as an information/computer-based technique, PNs were immediately adopted in a variety of application areas, such as manufacturing, design, planning and control. Viewed through a more recently developed programming perspective, the ordinary PNs became “high level” PNs suitable for defining different data types and for applying hierarchical approaches.

It is expected that the robust theoretical basis of this tool coupled with its visual and flexibility features will continue to appeal to researchers and practitioners alike in a variety of domains and as a result will continue to evolve and expand.     

A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.