Rewriting Modulo in Deduction Modulo
F. Blanqui
(École Polytechnique, Palaiseau, France)
We study the termination of rewriting modulo a set of equations in the
Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with
functions and predicates defined by higher-order rewrite rules. In a previous work, we
defined general syntactic conditions based on the notion of computable closure for
ensuring the termination of the combination of rewriting and $\b$-reduction. Here, we
show that this result is preserved when considering rewriting modulo a set of equations if
the equivalence classes generated by these equations are finite, the equations are linear and
satisfy general syntactic conditions also based on the notion of computable closure. This
includes equations like associativity and commutativity, and provides an original treatment
of termination modulo equations.
Validation of the JavaCard Platform with Implicit Induction
Techniques
G. Barthe
(INRIA Sophia-Antipolis, France)
S. Stratulat
(Université de Metz, France)
The bytecode verifier (BCV), which performs a static analysis to reject
potentially insecure programs, is a key security function of the Java(Card) platform.
Over the last few years there have been numerous projects to prove formally the
correctness of bytecode verification, but relatively little effort has been made to provide
methodologies, techniques and tools that help such formalisations. In earlier work, we
develop a methodology and a specification environment featuring a neutral
mathematical language based on conditional rewriting, that considerably reduce the
cost of specifying virtual machines. In this work, we show that such a neutral
mathematical language based on conditional rewriting is also beneficial for performing
automatic verifications on the specifications, and illustrate in particular how implicit
induction techniques can be used for the validation of the Java(Card) Platform. More
precisely, we report on the successful use of SPIKE, a first-order theorem prover
based on implicit induction, (1) to cross-validate virtual machines, including a
reference virtual machine which performs saftey checks at run-time, an offensive
virtual machine which does not, and an abstract virtual machine that is used by the
BCV; (2) to show that the abstract virtual machine is monotone w.r.t. the order
induced by the subclass and subinterface relation. Both results are crucial to establish
the correctness of the BCV.
XML Schema, Tree Logic and Sheaves Automata
S. Dal Zilio
(CNRS, Marseille, France)
D. Lugiez
(Université de Provence, Marseille, France)
XML documents, and other forms of semi-structured data, may be roughly
described as edge labeled trees, it is therefore natural to use tree automata to reason on
them. This idea has already been successfully applied in the context of Document Type
Definition (DTD), the simplest standard for defining XML documents validity, but
additional work is needed to take into account XML Schema, a more advanced standard,
for which regular tree automata are not satisfactory. A major reason for this inadequacy is
the presence of an associative-commutative operator in the schema language, inherited
from the &-operator of SGML, and the inherent limitations of regular tree automata in
dealing with associative-commutative algebras. In this paper, we define a tree logic that
directly embeds XML Schema as a plain subset and that explicitly takes into account the
equational properties of the schema operators. Namely associativity of sequential
composition and associativity-commutativity of &. Another contribution is a new class of
automata for unranked trees, used to decide our logic, that is well-suited to the processing
of XML documents and schemas. We believe it is the first work applying tree automata to
XML that considers the &-operator. This addition is significant because this operator has
been the subject of many controversial debates among the XML community and because it
poses several difficult implementation problems. Our work provides some justifications
for these difficulties and gives several complexity results on problems related to XML
schema, such as checking that a document conform to a schema, checking whether the set
of documents matching a schema is empty, ... Among other results, we also make clear
how simple syntactical restrictions on schemas improve the complexity of simple
operations.
Termination of String Rewriting Rules That Have One
Pair of Overlaps
A. Geser
(National Institute of Aerospace, Hampton, USA)
This paper presents a partial solution to the long standing open problem of
termination of one-rule string rewriting. Overlaps between the two sides of the rule play a
central role in existing termination criteria. We characterize termination of all one-rule
string rewriting systems that have one such overlap at either end. This both completes a
result of Kurth and generalizes a result of Shikishima-Tsuji et al.
New decidability results for fragments of first order logic
and application to cryptographic protocols
H. Comon-Lundh
(ENS Cachan, France)
V. Cortier
(ENS Cachan, France)
We consider a new extension of the Skolem class for first-order logic and
prove its decidability by resolution techniques. We then extend this class including the
built-in equational theory of exclusive or. Again, we prove the decidability of the class by
resolution techniques. Considering such fragments of first-order logic is motivated by the
automatic verification of cryptographic protocols, for an arbitrary number of sessions; the
first-order formalization is an approximation of the set of possible traces, for instance
relaxing the nonce freshness assumption. As an application of the decision results for
extensions of the Skolem class, we get some new decidability results for the verification
of cryptographic protocols without the perfect cryptography assumption: we may include
the algebraic properties of exclusive or. The proof of our main result relies on classical
techniques: ordered strategies, narrowing modulo AC, semantic trees.
Associative-Commutative Rewriting on Large Terms
S. Eker
(SRI International, Menlo Park, USA)
We introduce a novel representation for associative-commutative (AC) terms
which, for certain important classes of rewrite rule, allows both the AC matching and the
AC renormalization steps to be accomplished using time and space that is logarithmic in
the size of the flattened AC argument lists involved. This novel representation can be
cumbersome for other, more general algorithms and manipulations. Hence, we describe
machine efficient techniques for converting to and from a more conventional
representation together with a heuristic for deciding at runtime when to convert a term to
the new representation. We sketch how our approach can be generalized to order-sorted
AC rewriting and to other equational theories. We also present some experimental results
using the Maude 2 interpreter.
Recognizing Boolean Closed A-Tree Languages with Membership Conditional
Rewriting Mechanism
H. Ohsaki
(AIST & JST, Amagasaki, Japan)
H. Seki
(Nara Institute of Science and Technology, Ikoma, Japan)
T. Takai
(AIST, Amagasaki, Japan)
This paper provides an algorithm to compute the complement of tree languages
recognizable with A-TA (tree automata with associativity axioms). Due to this closure
property together with the previously obtained results, we know that the class is boolean
closed, while keeping recognizability of A-closures of regular tree languages. In the proof
of the main result, a new framework of tree automata, called sequence-tree automata, is
introduced as a generalization of Lugiez and Dal Zilio's multi-tree automata of an
associativity case. It is also shown that recognizable A-tree languages are closed under a
one-step rewrite relation in case of ground A-term rewriting. This result allows us to
compute an under-approximation of A-rewrite descendants of recognizable A-tree
languages with arbitrary accuracy.
Termination of Simply Typed Term Rewriting Systems
by Translation and Labelling
T. Aoto
(Tohoku University, Sendai, Japan)
T. Yamada
(Mie University, Tsu, Japan)
Simply typed term rewriting proposed by Yamada (RTA 2001) is a framework
of term rewriting allowing higher-order functions. In contrast to the usual higher-order
term rewriting frameworks, simply typed term rewriting dispenses with bound variables.
This paper presents a method for proving termination of simply typed term rewriting
systems (STTRSs, for short). We first give a translation of STTRSs into many-sorted
first-order TRSs and shows that termination problem of STTRSs is reduced to that of
many-sorted first-order TRSs. Next, we introduce a labelling method which is applied to
first-order TRSs obtained by the translation to facilitate termination proof of them; our
labelling employs an extension of semantic labelling where terms are interpreted on a
many-sorted algebra.
Liveness in Rewriting
J. Giesl
(RWTH Aachen, Germany)
H. Zantema
(Eindhoven University of Technology, Eindhoven, The Netherlands)
In this paper, we show how the problem of verifying liveness properties is
related to termination of term rewrite systems (TRSs). We formalize liveness in the
framework of rewriting and present a sound and complete transformation to transform
liveness problems into TRSs. Then the transformed TRS terminates if and only if the
original liveness property holds. This shows that liveness and termination are essentially
equivalent. To apply our approach in practice, we introduce a simpler sound
transformation which only satisfies the `only if'-part. By refining existing techniques for
proving termination of TRSs we show how liveness properties can be verified
automatically. As examples, we prove a liveness property of a waiting line protocol for a
network of processes and a liveness property of a protocol on a ring of processes.
Rewriting Logic and Probabilities
O. Bournez
(INRIA, Villers-lés-Nancy, France)
M. Hoyrup
(ENS Lyon, France)
Rewriting Logic has shown to provide a general and elegant framework for
unifying a wide variety of models, including concurrency models and deduction systems.
In order to extend the modeling capabilities of rule based languages, it is natural to
consider that the firing of rules can be subject to some probabilistic laws. Considering
rewrite rules subject to probabilities leads to numerous questions about the underlying
notions and results. In this paper, we discuss whether there exists a notion of probabilistic
rewrite system with an associated notion of probabilistic rewriting logic.
Efficient Reductions with Director Strings
F.-R. Sinot
(King's College, London, United Kingdom)
M. Fernández
(King's College, London, United Kingdom)
I. Mackie
(King's College, London, United Kingdom)
We present a name free lambda-calculus with explicit substitutions based on a
generalized notion of director strings: we annotate a term with information about how each
substitution should be propagated through the term. We define a first calculus which
implements closed reduction and is adequate for the evaluation of programs (reduction to
weak head normal form). In contrast with standard weak strategies, we allow certain
reductions to take place inside lambda-abstractions, which offers more sharing of redexes.
We then present a generalized calculus where we can simulate arbitrary beta-reduction
steps, and another weak calculus, which is a compromise between simplicity and
generality. Our experimental results confirm that, for large combinator based terms, weak
strategies based on these calculi out-perform standard evaluators. Moreover, we derive
two abstract machines for strong reduction which inherit the efficiency of the weak
evaluators.
A Rewriting Alternative to Reidemeister-Schrier
N. Ghani
(University of Leicester, United Kingdom)
A. Heyworth
(University of Leicester, United Kingdom)
One problem in computational group theory is to find a presentation of the
subgroup generated by a set of elements of a group. The Reidermeister-Schreier algorithm
was developed in the 1930's and gives a solution based upon enumerative techniques.
This however means the algorithm can only be applied to finite groups. This paper
proposes a rewriting based alternative to the Reidermeister-Schreier algorithm which has
the advantage of being applicable to infinite groups.
On the complexity of higher-order matching in the linear
lambda-calculus
S. Salvati
(INPL, Vandoeuvre-lès-Nancy, France)
P. de Groote
(INRIA, Vandoeuvre-lès-Nancy, France)
We prove that second-order matching in the linear $\lambda$-calculus with
linear occurrences of the unknowns is NP-complete. This result shows that context
matching and second-order matching in the linear $\lambda$-calculus are, in fact, two
different problems.
Testing Extended Regular Language Membership Incrementally by Rewriting
G. Rosu
(University of Illinois at Urbana-Champaign, Urbana, USA)
M. Viswanathan
(University of Illinois at Urbana-Champaign, Urbana, USA)
In this paper we present lower bounds and rewriting algorithms for testing
membership of a word to a regular language described by an extended regular expression.
Motivated by intuitions from monitoring and testing, where the words to be tested
(execution traces) are typically much longer than the size of the regular expressions
(patterns or requirements), and by the fact that in many applications the traces are only
available incrementally, on an event by event basis, our algorithms are based on an
event-consumption idea: a just arrived event is ``consumed'' by the regular expression,
i.e., the regular expression modifies itself into another expression discarding the event.
We present an exponential space lower bound for monitoring extended regular
expressions and argue that the presented rewriting-based algorithms, besides their
simplicity and elegance, are practical and almost as good as one can hope. We
experimented with and evaluated our algorithms in Maude.
Relating derivation lengths with the slow
growing hierarchy directly
G. Moser
(University of Münster, Germany)
A. Weiermann
(University of Münster, Germany)
In this article we introduce the notion of a generalized system of fundamental
sequences and we define its associated slow growing hierarchy. We claim that these
concepts provide a bridge connecting (ordinal) proof theory and term rewriting theory.
More precisely these concepts are genuinely related to the classification of the
complexity---the derivation length--- of rewrite systems for which termination is proved
by a standard termination ordering. To substantiate this claim, we re-obtain multiple
recursive bounds on the the derivation length for rewrite systems terminating under
lexicographic path ordering. The novelty of our proof being that is clarifies precisely the
proof-theoretic concepts exploited in the original proof by the second author. In particular
it reveals the role played by the slow-growing hierarchy.
Stable Computational Semantics of Conflict-free Rewrite
Systems (Partial Orders with Duplication)
Z. Khasidashvili
(Intel, Haifa, Israel)
J. Glauert
(University Plain, Norwich, United Kingdom)
We study orderings on reductions in the style of Levy reflecting the growth of
information w.r.t. (super)stable sets S of 'values' (such as head-normal forms or
Bohm-trees). We show that sets of co-initial reductions ordered by such orderings form
finitary w-algebraic complete lattices, i.e., form computation and Scott domains. As a
consequence, we obtain a relativized version of computational semantics as proposed by
Boudol for term rewriting systems. Furthermore, we give a pure domain-theoretic
characterization of the orderings in the spirit of Kahn and Plotkin's concrete domains.
These constructions are carried out in the framework of Stable Deterministic Residual
Structures, which are abstract reduction systems with an axiomatized residual relations on
redexes, and model all orthogonal (or conflict-free) reduction systems as well as many
other interesting computation structures.
Residuals in Higher-Order Rewriting
S. Bruggink
(University of Utrecht, The Netherlands)
An interesting topic of research within rewriting theory is residual theory: what
remains of a reduction phi after another reduction psi, which starts at the same object, has
been performed? The residual of phi after psi, written varphi/psi, should consist of exactly
those steps of varphi, which were not performed by psi. Residuals were studied by Levy,
Huet, Mellies, Van Oostrom & De Vrijer, and residual systems are defined. We mention
the following important result: if a residual system can be specified for some rewriting
system R then R is confluent. In this article we study residuals in Pattern Rewriting
Systems, a subclass of Nipkow's Higher-Order Rewriting Systems (HRSs). First, the
rewrite relation is defined by means of a higher-order rewriting logic, and proof terms in
the style of Hilken are defined, which witness reductions. Now, we have the formal
machinery to define a residual operator for PRSs, and we will prove the following
theorem: Theorem: If H is an orthogonal HRS, then H with projection operator is a
residual system. As a side-effect, all results of residual theory are inherited by orthogonal
PRSs, such as confluence, and the notion of equivalence of reductions, also known as
Levy- or permutation equivalence.
Confluence as a cut elimination property
G. Dowek
(École polytechnique, Palaiseau, France)
The goal of this paper is to compare two notions, one coming from the theory
of rewrite systems and the other from proof theory: confluence and cut elimination. We
show that to each rewrite system on terms, we can associate a logical system: asymmetric
deduction modulo this rewrite system and that the confluence property of the rewrite
system is equivalent to the cut elimination property of the associated logical system. This
equivalence, however, does not extend to rewrite systems on propositions.
Two-Way Equational Tree Automata for AC-like Theories:
Decidability and Closure Properties
K.N. Verma
(ENS Cachan, France)
We study two-way tree automata modulo equational theories. We deal with the
theories of Abelian groups ($ACUM$), idempotent commutative monoids ($ACUI$), and
the theory of exclusive-or ($ACUX$), as well as some variants including the theory of
commutative monoids ($ACU$). We show that the one-way automata for all these
theories are closed under union and intersection, and emptiness is decidable. For two-way
automata the situation is more complex. In all these theories except $ACUI$, we show
that two-way automata can be effectively reduced to one-way automata, provided some
care is taken in the definition of the so-called push clauses. (The $ACUI$ case is open.) In
particular, the two-way automata modulo these theories are closed under union and
intersection, and emptiness is decidable. We also note that alternating variants have
undecidable emptiness problem for most theories, contrarily to the non-equational case
where alternation is essentially harmless.
Size-Change Termination for Term Rewriting
R. Thiemann
(RWTH Aachen, Germany)
J. Giesl
(RWTH Aachen, Germany)
In [Lee, Jones & Ben-Amram, 2001], a new size-change principle was
proposed to verify termination of functional programs automatically. We extend this
principle in order to prove termination and innermost termination of arbitrary term rewrite
systems (TRSs). Moreover, we compare this approach with existing techniques for
termination analysis of TRSs (such as recursive path orderings or dependency pairs). It
turns out that the size-change principle on its own fails for many examples that can be
handled by standard techniques for rewriting, but there are also TRSs where it succeeds
whereas existing rewriting techniques fail. In order to benefit from their respective
advantages, we show how to combine the size-change principle with classical orderings
and with dependency pairs. In this way, we obtain a new approach for automated
termination proofs of TRSs which is more powerful than previous approaches.
Expression Reduction Systems with Patterns
J. Forest
(Université Paris-Sud, Orsay, France)
D. Kesner
(Université Paris 7, Paris, France)
We introduce a new higher-order rewriting formalism, called Expression
Reduction Systems with Patterns (ERSP), where abstraction is not only allowed on
variables but also on nested patterns. These patterns are built by combining standard
algebraic patterns with choice constructors used to denote different possible structures
allowed for an abstracted argument. In other words, the non deterministic choice between
different rewriting rules which is inherent to classical rewriting formalisms can be lifted
here to the level of patterns. We show that confluence holds for a reasonable class of
systems and terms.
Diagrams for Meaning Preservation
J.B. Wells
(Heriot-Watt University, Edinburgh, United Kingdom)
D. Plump
(University of York, United Kingdom)
F. Kamareddine
(Heriot-Watt University, Edinburgh, United Kingdom)
This paper presents an abstract framework and multiple diagram-based
methods for proving meaning preservation, i.e., that all rewrite steps of a rewriting
system preserve the meaning given by an operational semantics based on a rewriting
strategy. While previous rewriting-based methods have generally needed the treated
rewriting system as a whole to have such properties as, e.g., confluence, standardization,
and/or termination or boundedness of developments, our methods can work when all of
these conditions fail, and thus can handle more rewriting systems. We isolate the new
lift/project diagram as the key proof idea and show that previous rewriting-based methods
(Plotkin's method based on confluence and standardization and Machkasova and Turbak's
method) implicitly use this diagram. Furthermore, our framework and proof methods help
reduce the proof burden substantially by, e.g., supporting separate treatment of partitions
of the rewrite steps, needing only elementary diagrams for rewrite step interactions,
excluding many rewrite step interactions from consideration, needing weaker termination
properties, and providing generic support for using developments in combination with any
method.
Monotonic AC-compatible semantic path orderings
C. Borralleras
(Universitat de Vic, Spain)
A. Rubio
(Universitat Politecnica de Catalunya, Barcelona, Spain)
Polynomial interpretations and RPO-like orderings allow one to prove
termination of Associative and Commutative (AC-)rewriting by only checking the rules of
the given rewrite system without considering the so-called extended rules. However, these
methods have important limitations as termination proving tools. To overcome these
limitations, more powerful methods like the dependency pairs method have been extended
to the AC-case. Unfortunately, in order to ensure AC-termination, the extended rules,
which, in general, are hard to prove, must be added to the rewrite system. In this paper
we present a new automatable ordering-based termination proving method for
AC-rewriting which does not need to consider extended rules. Due to this, we can easily
prove several non-trivial examples appearing in the literature that, to our knowledge, can
be handled by no other automatic method.
"Term Partition" for Mathematical Induction
P. Urso
(Université de Nice - Sophia Antipolis, Nice, France)
E. Kounalis
(Université de Nice - Sophia Antipolis, Nice, France)
A key new concept, term partition, allows to design a new method for proving
theorems whose proof usually requires mathematical induction. A term partition of a term t
is a well-defined splitting of t into a pair (a,b) of terms that describes the language of
normal forms of the ground instances of t. If A is a monomorphic set of axioms (rules)
and (a,b) is a term partition of t, then the normal form (obtained by using A) of any
ground instance of t can be ``divided'' into the normal forms (obtained by using A) of the
corresponding ground instances of a and b. Given a conjecture t = s to be checked for
inductive validity in the theory of A, a partition (a,b) of t and a partition (c,d) of s is
computed. If a = c and b = d, then t = s is an inductive theorem for A. The method is
conceptually different to the classical theorem proving approaches since it tries to directly
mechanize the omega-rule. It allows to obtain elegant and natural proofs of a large number
of conjectures (including non-linear ones) without additional lemmas and/or
generalizations.
A Rule-Based Approach for Automated Generation of Kinetic
Chemical Mechanisms
O. Bournez
(LORIA & INRIA, Villers-lés-Nancy, France)
G.-M. Come
(INPL-ENSIC, Nancy, France)
V. Conraud
(LORIA & INRIA, Villers-lés-Nancy, France)
H. Kirchner
(LORIA & INRIA, Villers-lés-Nancy, France)
L. Ibanescu
(LORIA, Villers-lés-Nancy, France)
Several software systems have been developed recently for the automated
generation of combustion reactions kinetic mechanisms using different representations of
species and reactions and different generation algorithms. In parallel, several software
systems based on rewriting have been developed for the easy modeling and prototyping of
systems using rules controlled by strategies. This paper presents our current experience in
using the rewrite system ELAN for the automated generation of the combustion reactions
mechanisms previously implemented in the EXGAS kinetic mechanism generator system.
We emphasize the benefits of using rewriting and rule-based programming controlled by
strategies for the generation of kinetic mechanisms.
An E-unification algorithm for analyzing protocols
that use modular exponentiation
D. Kapur
(University of New Mexico, Albuquerque, USA)
P. Narendran
(SUNY at Albany, USA)
L. Wang
(SUNY at Albany, USA)
Multiplication and exponentiation modulo a prime are common operations in
modern cryptography. Unification problems modulo some equational theories that these
operations satisfy are investigated. The algorithms for some of these unification problems
are expected to be integrated into Naval Research Lab.'s Protocol Analyzer (NPA), a tool
developed by Catherine Meadows, which has been successfully used to analyze
cryptographic protocols, particularly emerging standards such as the Internet Engineering
Task Force's (IETF) Internet Key Exchange~\cite{ike} and Group Domain of
Interpretation~\cite{gdoi} protocols. Currently, for equational unification, NPA uses
narrowing procedures which work only for terminating and confluent rewrite systems.
Given that modular multiplication is associative and commutative, NPA cannot be
effectively applied for protocols that use these operations. Two different but related
equational theories are analyzed here. A unification algorithm is given for one of the
theories which relies on solving syzygies over multivariate integral polynomials with
noncommuting indeterminates. For the other theory, in which the distributivity property of
exponentiation over multiplication is assumed, the unifiability problem is shown to be
undecidable by adapting a construction developed by one of the authors to reduce
Hilbert's 10th problem to the solvability problem for linear equations over semi-rings. A
new algorithm for computing strong \Groebner\ basis of right ideals over the polynomial
ring Z is proposed; unlike earlier algorithms proposed by Baader as well as by Madlener
and Reinert which work only for right admissible term orderings with the boundedness
property, this algorithm works for {\em any\/} right admissible term ordering. Techniques
from several different fields -- particularly symbolic computation (ideal theory and
Groebner basis algorithms) and unification theory --- are used to address problems
arising in state-based cryptographic protocol analysis.
The Equational Prover of THEOREMA
T. Kutsia
(SUNY at Albany, USA)
The paper describes the equational prover of Theorema. It is a prover for unit
equational deduction implemented on Mathematica. The prover accepts input either in the
first order or in the applicative higher order form. Besides, sequence variables can occur
and a (restricted) usage of Mathematica built-in functions are allowed. Main proving
method is unfailing completion, extended for terms with sequence variables, and
narrowing (for existential goals). Mathematica technology is exploited to implement
rewriting. Warren's translation method is used to transform applicative higher order
expressions into the first order form. Proof presentation is based on a slightly modified
variant of Equational Chain calculus. Implementation issues are discussed.
Tsukuba Termination Tool
N. Hirokawa
(University of Tsukuba, Japan)
A. Middeldorp
(University of Tsukuba, Japan)
We present a tool for automatically proving termination of first-order rewrite
systems. The tool is based on the dependency pair method of Arts and Giesl. It
incorporates several new techniques to make the method more efficient. The tool produces
high-quality output and has a convenient web interface. We explain the features of the tool
and we give some implementation details. We conclude with some experiments, including
a brief comparison with other termination tools that implement the dependency pair
method.
Rule-based Analysis of Dimensional Safety
F. Chen
(University of Illinois at Urbana-Champaign, Urbana, USA)
G. Rosu
(University of Illinois at Urbana-Champaign, Urbana, USA)
R.P. Venkatesan
(University of Illinois at Urbana-Champaign, Urbana, USA)
Dimensional safety policy checking is an old topic in software analysis
concerned with ensuring that programs do not violate basic principles of units of
measurement. Scientific and/or navigation software is routinely dimensional and violations
of measurement unit safety policies can hide significant domain-specific errors which are
hard or impossible to find otherwise. Dimensional analysis of programs written in
conventional programming languages is addressed in this paper. We draw general design
principles for dimensional analysis tools and then discuss our prototypes, implemented by
rewriting, which include both dynamic and static checkers. Our approach is based on
assume/assert annotations of code which are properly interpreted by our tools and ignored
by standard programming language compilers/interpreters. The output of our prototypes
consists of warnings that list those expressions violating the unit safety policy. These
prototypes are implemented in the rewriting system Maude, using more than 2,000
rewriting rules. This paper presents a non-trivial application of rewriting techniques to
software analysis.
Environments for Term Rewriting Engines for Free!
M. van den Brand
(CWI, Amsterdam, The Netherlands and LORIA-INRIA, Villers-lés-Nancy, France)
P.-E. Moreau
(LORIA-INRIA, Villers-lés-Nancy, France)
J. Vinju
(CWI, Amsterdam, The Netherlands)
Term rewriting can only be applied if practical implementations of term
rewriting engines exist. New rewriting engines are designed and implemented either to
experiment with new (theoretical) results or to be able to tackle new application areas. In
this paper we present the Meta-Environment: an environment rapidly implementing the
syntax and semantics of term rewriting based formalisms. We provide not only the basic
building blocks, but complete interactive programming environments that only need to be
instantiated by the details of a new formalism.
Rewriting UNITY
A. Granicz
(California Institute of Technology, Pasadena, USA)
D. Zimmerman
(California Institute of Technology, Pasadena, USA)
J. Hickey
(California Institute of Technology, Pasadena, USA)
In this paper we describe the implementation of the UNITY formalism as
an extension of general-purpose languages and show its translation to C abstract
syntax using Phobos, our generic front-end in the Mojave compiler. Phobos uses term
rewriting to define the syntax and semantics of arbitrary languages, and automates their
translation to an internal compiler representation. Furthermore, it provides access to
formal reasoning capabilities using the integrated MetaPRL theorem prover, through
which advanced optimizations and transformations can be implemented or formal
proofs derived.
The Maude 2.0 System
M. Clavel
(Universidad Complutense de Madrid, Spain)
F. Durán
(Universidad de Málaga, Spain)
S. Eker
(SRI International, Menlo Park, USA)
P. Lincoln
(SRI International, Menlo Park, USA)
N. Martí-Oliet
(Universidad Complutense de Madrid, Spain)
J. Meseguer
(University of Illinois at Urbana-Champaign, Urbana, USA)
C. Talcott
(SRI International, Menlo Park, USA)
The Maude 2.0 system supports both equational and rewriting logic
computation with high generality and expressiveness, yet without compromising
performance. Functional mod ules are membership equational theories, whereas
system modules are very general rewrite theories whose rules can have equations, memberships,
and rewrites in their conditions, and where some operator arguments can be
frozen to block undesired rewrites. Furt hermore, Full Maude 2.0 supports
parameterized modules, theories, and views, and objec t-oriented modules.
Besides supporting equational simplification, Maude 2.0 supports several
fair rewriting strategies as well as breadth-first search for rule computations. Reflective capabilities are substantially extended in a new
META-LEVEL module. There are also efficient predefined implementations of
useful arithmetic and string data types. Since rewrite theories are ideally
suited to specify concurrent systems, Maude 2.0 supports efficient
explicit-state model checking of linear temporal logic properties satisfied
by (finite-state) rewrite theories. The efficiency of rewriting modulo axioms
has also been increased thanks to some novel techniques.
Finally, using reflection an environment of formal tools for Maude 2.0,
extending earlier tools, is currenty under development.