We present strategic port graph rewriting as a basis for the implementation of visual modelling tools. The goal is to facilitate the specification and programming tasks associated with the modelling of complex systems. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. We give a formal semantics for the language, and describe its implementation: the graph transformation and visualisation tool Porgy.

In the context of understanding, planning and anticipating the behaviour of complex systems, such as biological networks or social networks, this paper proposes port graphs, rules and strategies, combined in strategic rewrite programs, as foundational ingredients for interactive and visual programming and shows how they can contribute to dynamic data analytics.

Security policies are one of the most fundamental elements of computer security. Current security policy design is concerned with the composition of components in security systems and interactions among them. Consequently, in a modular specification and verification of a policy, the composition of the modules must consistently assure security policies. A rigorous and systematic way to predict and assure such critical properties is crucial. This paper addresses the problem in a formal way. It uses colored Petri net process (CPNP) to specify and verify security policies in a modular way. It defines fundamental policy properties, i.e., completeness, termination, consistency, and confluence in Petri net terminology and gets some theoretical results. According to the eXtensible Access Control Markup Language (XACML) combiners and property preserving Petri net process algebra (PPPA), several policy composition operators are specified and property preserving results are stated for the policy correctness verification. As an application, the approach is illustrated for the design of Chinese Wall Policy.

Security policies are one of the most fundamental elements of computer security. For secure interoperation and sharing resources among heterogeneous systems, local policies should correspondingly be integrated for designing a global policy. This paper addresses the problem in a formal way. It uses extended Petri net process to specify and verify security policies in a modular way. It defines four types of policy compositions such that the integrated policy is capable of handling resources sharing, simultaneously executing operations and embedding sub-policies into main policies in multiple heterogeneous systems. Furthermore, the global policy can preserve the fundamental policy properties, i.e.,completeness, termination, consistency and confluence, and satisfy policy autonomy and security principles that are required for secure interoperation.

A termination proof method for rewriting under strategies, based on an explicit induction on the termination property, is presented and instantiated for the innermost, outermost, and local strategies. Rewriting trees are simulated by proof trees generated with an abstraction mechanism, narrowing and constraints representing sets of ground terms. Abstraction introduces variables to represent normal forms without computing them and to control the narrowing mechanism, well known to easily diverge. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. It is established that termination under strategy is equivalent to the construction of finite proof trees schematizing terminating rewriting trees. Sufficient effective conditions to ensure finiteness are studied and the method is illustrated on several examples for each specific strategy.

In the context of the study of rule-based programming, we focus in this paper on the property of C-reducibility, expressing that every term reduces to a constructor term on at least one of its rewriting derivations. This property implies completeness of function definitions, and enables to stop evaluations of a program on a constructor form, even if the program is not terminating. We propose an inductive procedure proving C-reducibility of rewriting. The rewriting relation on ground terms is simulated through an abstraction mechanism and narrowing. The induction hypothesis allows assuming that terms smaller than the starting terms rewrite into a constructor term. The existence of the induction ordering is checked during the proof process, by ensuring satisfiability of ordering constraints. The proof is constructive, in the sense that the branch leading to a constructor term can be computed from the proof trees establishing C-reducibility for every term.

In rule-based languages, control of rule application can be expressed thanks to strategy constructors. The paper addresses termination of such strategy-guided evaluation. To fix ideas, we use the ELAN strategy language. We first give a sufficient criterion for ELAN-like strategies to terminate, only lying on rewrite rules involved in the strategy. We then give a simplification process of strategies, itself described by rewriting, to empower the previous criterion. This simplification can also make proofs of other program properties easier.

We describe Cariboo, the implementation of an inductive process recently proposed to prove termination of rewriting under strategies on ground term algebras. The method is based on an abstraction mechanism, introducing variables that represent ground terms in normal form, and on narrowing, schematizing reductions on ground terms. It applies in particular to non-terminating systems which are terminating with innermost or local strategies. The narrowing process, well known to easily diverge, is controlled by using appropriate abstraction constraints. The abstraction mechanism lies on satisfiability of ordering constraints. Thanks to the power of induction, these ordering constraints are often simple and automatically solved by our system. Otherwise, they can be treated by the user or any external automatic solver. On many examples, Cariboo even enables to succeed without considering any constraint at all ; the process is then completely automatic. Cariboo offers a graphical view of the proof process. It is implemented in ELAN, a rule based programming environment, and so can be used for proving termination of ELAN programs.

First-order languages based on rewrite rules share many features with functional languages, but one difference is that matching and rewriting can be made much more expressive and powerful by incorporating some built-in equational theories. To provide reasonable programming environments, compilation techniques for such languages based on rewriting have to be designed. This is the topic addressed in this paper. The proposed techniques are independent from the rewriting language, and may be useful to build a compiler for any system using rewriting modulo Associative and Commutative (AC) theories. An algorithm for many-to-one AC matching is presented, that works efficiently for a restricted class of patterns. Other patterns are transformed to fit into this class. A refined data structure, namely compact bipartite graph, allows encoding of all matching problems relative to a set of rewrite rules. A few optimisations concerning the construction of the substitution and of the reduced term are described. We also address the problem of non-determinism related to AC rewriting, and show how to handle it through the concept of strategies. We explain how an analysis of the determinism can be performed at compile time, and we illustrate the benefits of this analysis for the performance of the compiled evaluation process. Then we briefly introduce the ELAN system and its compiler, in order to give some experimental results and comparisons with other languages or rewrite engines.

In most algebraic specification frameworks, the type system is restricted to sorts, subsorts, and first‐order function types. This is in marked contrast to the so‐called model‐oriented frameworks, which provide higher‐order types, interpreted set‐theoretically as Cartesian products, function spaces, and power‐sets. This paper presents a simple framework for algebraic specifications with higher‐order types and set‐theoretic models. It may be regarded as the basis for a Horn‐clause approximation to the Z framework, and has the advantage of being amenable to prototyping and automated reasoning. Standard set‐theoretic models are considered, and conditions are given for the existence of initial reducts of such models. Algebraic specifications for various set‐theoretic concepts are considered.

Two main applications of term rewriting systems are equational reasoning in theorem provers and equational computation in programming languages. The present paper examines a number of term rewriting systems in terms of how rewriting is used in different implementations of theorem provers, the use of rewriting techniques in logic programming languages and the problem of efficiency. In addition a non-exhaustive catalogue of distributed implementations is presented.

Publie dans : Proceedings ISSAC'89 (International symposium on symbolic and algebraic computation), Portland (Oregon, USA), July 1989

Abstract Church-Rosser properties are first presented, depending on an arbitrary relation R, an equivalence relation E and a reduction relation $R^E $ used to compute normal forms of R modulo E. Terminating rewriting systems operating on equational congruence classes of terms of a free algebra are then considered. In this framework, the Church–Rosser property is proved decidable for a very general reduction relation which may take into account the left-linearity of rules for efficiency reasons, under the only assumption of existence of a complete and finite unification algorithm for the underlying equational theory, whose congruence classes are assumed to be finite. This extends previous results by Lankford and Ballantyne, Peterson and Stickel, Huet, Jouannaud. A general completion procedure for mixed sets of rules and equations is then presented that generalizes and improves Peterson and Stickel’s one. In addition to computing a Church–Rosser set of rules when it terminates, it yields a semi-decision procedure for testing equality when it runs forever. Finally a post-processor is described that yields a Church–Rosser set of inter-reduced rules. All proofs, including the correctness proof of our completion algorithm, are based on the powerful proof technique of multiset induction.

Article Completion of a set of rules modulo a set of equations Share on Authors: Jean-Pierre Jouannaud CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE) CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)View Profile , Helene Kirchner CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE) CRIN, BP 239, 54506 Vandoeuvre les Nancy, CEDEX (FRENCE)View Profile Authors Info & Claims POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1984 Pages 83–92https://doi.org/10.1145/800017.800519Online:15 January 1984Publication History 41citation373DownloadsMetricsTotal Citations41Total Downloads373Last 12 Months8Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access