WRS
|
List of invited speakers of WRS:
IWS 2012
|
A rewriting point of view on strategies
|
|
Hélène Kirchner
(INRIA France)
|
Strategies frequently occur in automated deduction and reasoning systems and more generally
are used to express complex designs for control in modeling, proof search, program
transformation, SAT solving or security policies. In these domains, deterministic rule-based
computations or deductions are often not sucient to capture complex computation or proof
development. A formal mechanism is needed, for instance, to sequentialize the search for
di erent solutions, to check context conditions, to request user input to instantiate variables,
to process subgoals in a particular order, etc. This is the place where the notion of
strategy comes in. In the communities of logic, verification and rewriting, definitions have
been given and progress has been made towards a deeper understanding of the nature of
strategies, their descriptions, their properties, and their usage.
Since the field is quite large, I will adopt in this talk the specific point of view of
rewriting. Rewriting logic and rewriting calculus are powerful formalisms to
express and study uniformly computations and deductions in automated deduction and
reasoning systems.
Based on rewriting concepts, several definitions of strategy will be reviewed and connected.
In order to catch the higher-order nature of strategies, a strategy is defined as a proof
term expressed in the rewriting calculus. To address in a coherent way deduction and
computation, a strategy is seen as a set of paths in a derivation tree whose reduction relation
is a one-step reduction. To recover the definition of strategy in sequential path-building
games or in functional programs, a strategy is considered as a partial function that associates
to a reduction-in-progress, the possible next steps in the reduction sequence.
The second part of the talk will address the specification of strategies by reviewing
several strategy languages that have been recently designed and studied on structures
like trees and graphs. Used for a long time in lambda-calculus, strategies are present in
programming languages such as Clean, Curry and Haskell, and can be explicitely defined
to rewrite terms in languages such as Elan, Stratego, Maude or Tom. They
are also present in graph transformation tools such as GP and PORGY. Based on
some of these approaches, we will identify useful constructs that are necessary to express
control on rules and structures.
|
Refinements and Search Strategies for Semantic
Tableaux with Blocking
|
|
Renate Schmidt
(The University of Manchester, UK)
|
A popular approach to developing decision procedures for non-classical logics including modal,
hybrid and description logics are ground semantic tableau calculi. Rules of ground semantic
tableau calculi perform inference steps in a way that closely follows the semantics of a logic.
This property means tableau derivations are easy to understand and easy to construct both by
hand and automatically.
Another reason for the popularity of ground semantic tableau calculi is the ease with which
they can be devised for semantically defined logics. We recently developed a tableau synthesis
framework, which shows that it is in fact possible to obtain sound and complete calculi semi-
automatically from the specification of the semantics of a logic. There are also effective and
general ways to obtain terminating tableau calculi. For example, adding the unrestricted blocking
mechanism to sound and complete ground semantic calculus gives a terminating calculus
for the logic, when the logic has the finite model property.
Because the rules of a tableau calculus provide the basis for a non-deterministic deduction procedure,
there is essentially complete flexibility in how tableau derivations may be constructed.
In particular, the calculus does not give instructions of which branch to select for
expansion, it does not tell which rule to apply next and does not specify which of many possible
formulae to apply a rule to or which of many terms to use for instantiation. This means
the search space is generally huge. There are however standard principles for containing the
search space and tackling the challenges of obtaining effective implementations while inheriting
soundness, completeness and termination from the tableau calculus.
In this talk we are particularly interested in ways of making it easier to achieve an efficient
implementation of a tableau calculus. We emphasise techniques to refine tableau calculi, rule
simplification and redundancy, and in general principles to develop more effective tableau
calculi. We discuss ways of dealing with the various forms of non-determinism, including efficient
and fair application of rules with universal extent. Particularly challenging is the realisation of
blocking mechanisms to obtain decision procedures.
|
WRS 2011
The Maude strategy language and some of its
applications
|
|
Narciso Martí-Oliet
(U. Complutense, Spain)
|
Maude is a declarative specification and programming language based on rewriting logic.
A Maude rewrite theory essentially consists of a signature, a set of equations, and a set
of (conditional) rewrite rules. While the set of equations is assumed to be confluent and
terminating, so that every term has a normal form with respect to equational reduction,
rewrite rules can be nonconfluent or nonterminating.
A strategy is described as an operation that, when applied to a given term, produces a set
of terms as a result, given that the process is nondeterministic in general. The basic strategies
consist of the application of a rule to a given term, but rules can be conditional with respect
to some rewrite conditions which in turn can also be controlled by means of strategies. Those
basic strategies are combined by means of several combinators, including: regular expression
constructions (concatenation, union, and iteration), if-then-else, combinators to control the
way subterms of a given term are rewritten, and recursion. Furthermore, strategies can also
be generic.
This strategy language has been endowed with both a simple set-theoretic semantics and
a rewriting semantics, which are sound and complete with respect to the controlled rewrites.
Moreover, the rewriting semantics also enjoys properties of monotonicity and persistence.
The first applications of the strategy language included the operational semantics of
process algebras such as CCS and the ambient calculus. The same ideas were later applied
to the two-level operational semantics of the parallel functional programming language Eden
and to modular structural operational semantics. It has also been used in the implementation
of basic Knuth-Bendix completion algorithms and of congruence closure algorithms. Other
applications include a sudoku solver, neural networks, membrane systems, hierarchical design
graphs, and a representation of BPMN.
|
|
Graph Programs: Semantics, Verification and Implementation
|
|
Detlef Plump
(University of York, UK)
|
GP is a rule-based, nondeterministic programming language for high-level problem solving
in the domain of graphs, freeing programmers from handling low-level data structures. The
language has a simple syntax and semantics, to facilitate formal reasoning about programs.
In this talk, I will introduce GP by a number of example programs and discuss its structural
operational semantics. A special feature of this semantics is the use of failing computations to
de ne branching and iteration. I will then present proof rules for Hoare-style veri cation of
graph programs, and demonstrate their use by verifying a simple colouring program. Finally,
I will brie
y describe GP's current implementation.
|
IWS 2010
|
Game Strategies and Rule-Based Systems/font>
|
|
Dan Dougherty
(Worcester Polytechnic Institute, USA)
|
The classical notion of term-rewriting strategy has in recent years been expanded to find application
in a wide variety of rule-based computing scenarios, including proof-search, program transformation, and
planning. In parallel with these developments, games played on graphs have been extensively studied in
the verification community, with game strategies as a central notion. It is natural to wonder whether the
use of the term "strategy" in both of these two contexts is more than a pun. In this talk we explore some
consequences of viewing strategies in rule-based systems as strategies in games, specifically sequential
games of perfect information. In a foundational vein, viewing rewriting strategies as game strategies
suggest a new approach to the semantics of rewriting strategies. As a second application we describe
how certain security policies can be profitably viewed as strategies, and report on nascent work on policy
synthesis via game-solving.
The talk will touch on ongoing projects that are joint work with Emilie Balland, Joshua Guttman,
Claude Kirchner, and Hélène Kirchner.
|
Organizing and Using Algebraic Structures in Large
Developments of Formalized Mathematics
|
|
Assia Mahboubi
(INRIA, France)
|
The Mathematical Component project, at the Inria Microsoft Research Joint Centre, investigates
how to design large and consistent bodies of formalized mathematics. The playground of these investigations
is a formalization in the Coq system of a finite group theory famous result: the proof of the
Feit-Thompson theorem (1962), so called the Odd Order theorem. This milestone of the classification
of finite simple groups is also by its length a historic publication in the story of mathematical literature.
From a formal point of view, this proof is a true challenge. Some difficulties are well-known pitfalls
of formal mathematics: set-theoretic versus type-theoretic definitions, catching the implicit content of
mathematical texts,. . . But this proof also has the particularity of relying on a wide variety of elementary
algebraic structures and theories: while local analysis has a combinatoric flavor, character theory
requires a full formalization of standard linear algebra, field extensions, Galois theory, . . . . Beside the
required background in group theory, half of the local analysis part of the proof is now formalized, plus
standard linear algebra and some elementary module theory. In this talk, we will try to abstract from the
specificities of the Feit-Thompson proof. We will review how the Coq system, and in particular both its
computational features and its type inference mechanisms proves a precious and efficient tool in solving
these compositionality and automation general issues.
|
WRS 2009
|
From Abstract Strategies to Strategic Rewriting
|
|
Hélène Kirchner
(INRIA Bordeaux, France)
|
Strategies are ubiquitous in automated deduction and reasoning
systems, yet only since about ten years have they been studied
in their own right. In the two communities of automated deduction and
rewriting, workshops have been launched to make progress towards a
deeper understanding of the nature of strategies, their descriptions, their
properties, and their usage. Recently strategies have come to be viewed
more generally as expressing complex designs for control in modeling,
proof search, program transformation, and access control.
In this talk, we are contributing to the theoretical foundations of strategies.
We first present a general definition of abstract strategies that allows
the convergence of different points of view, namely rewriting-based computations
on one hand, rule-based deduction and proof-search on the
other hand. This definition is extensional in the sense that a strategy
is taken there explicitly to be a set of paths of an abstract reduction
system. We then move to a more intensional definition compliant with
the abstract view but more operational in the sense that it describes a
means for determining such a set. This naturally leads to define strategic
reductions and their instances on terms, namely strategic rewritings.
We rely on previous works that are briefly described and on strategy
languages that have been recently designed and studied.
|
Programming with non-deterministic functions:
some rewriting and semantic issues
|
|
Francisco López-Fraguas
(U. Complutense, Spain)
|
Non-deterministic functions are a nice programming construct
that can compete in elegance, conciseness and even efficiency
with other high-level approaches to non-determinism, like the use of relations
in logic programming. Non-confluent constructor-based rewrite
systems are a very adequate formalism giving syntactic support to nondeterministic
functions. However, there are different options about the
kind of non-determinism to be realized, a major distinction being that
of run-time choice and call-time choice.
In this talk we revise some recent (and not so recent) advances in relation
to the description of different variants of non-determinism (and their
combination), at the operational level -by giving formal definitions of
the reduction process- and at the semantic level -by giving logical calculi
prescribing the possible results of computations-.
|
WRS 2008
|
Diagram Rewriting: Examples and Theory
|
|
Yves Lafont
(U. de la Méditerranée, France)
|
Diagrams are a natural 2-dimensional generalization of words. They are
used in many areas of mathematics, physics, and computer science. I
will present some fundamental examples of diagram rewriting, leading
to an algebraic theory of boolean circuits.
|
WRS 2007
|
On Term-Graph Rewrite Strategies
|
|
Rachid Echahed
(IMAG Grenoble, France)
|
Graph rewriting is being investigated in various areas nowadays.
In this talk, we consider term-graph rewriting as the underlying
operational semantics of rule-based (functional or logic)
programming languages
|
Rules and Strategies in Java
|
|
Pierre-Etienne Moreau
(INRIA and LORIA Nancy, France)
|
In this talk we present the essential feature we have considered when
designing a new language based on rules and strategies.
Relying on the implementation of Tom, we explain how these ingredients can
be implemented and integrated in a Java environment.
|
WRS 2006
|
Programmed Strategies for Program Verification
|
|
Richard Kieburtz
(OGI Portland, OR, USA)
|
Plover is an automated property-verifier for Haskell programs that has been under
development for the past three years as a component of the Programatica
project. In Programatica, predicate definitions and property assertions written
in P-logic, a programming logic for Haskell, can be embedded in the text of a
Haskell program module. P-logic properties refine the type system of Haskell
but cannot be verified by type-checking alone; a more powerful logical verifier is
needed. Plover codes the proof rules of P-logic, and additionally, embeds strategies
and decision procedures for their application and discharge. It integrates a
reduction system that implements a rewriting semantics for Haskell terms with a
congruence-closure algorithm that supports reasoning with equality. It can employ
splitting strategies to explore alternative valuations of expressions of type
Bool or other finite data types, but these strategies lead to exponential growth
of terms and must be employed cautiously. Plover itself is written in Stratego,
which has proven to be a powerful language in which to write a verifier. This talk
will explain the design and implementation of some of the strategies that enable
Plover to comprehend Haskell and to discharge some valid property assertions.
|
Rewriting (your) Calculus
|
|
Claude Kirchner
(INRIA and LORIA Nancy, France)
|
Rewriting is clearly established as a general paradigm which agility eases to
express and reason about computation and deduction. The rewriting calculus,
generalizing the lambda calculus and the rewriting relation, provides us with a
theoretical and uniform foundation for this expressivity. Introduced in the late
nineties, the framework and its meta-properties are now better understood. We
will show why the calculus is well-suited to represent computation as well as
deduction, and therefore deduction modulo.
The rewriting calculus is therefore a good candidate to backup proof assistants
where the user can adapt the computation mechanism to its needs. But
furthermore, we want the next generation of proof assistants to provide the user
with the possibility to adapt also the deduction system to its needs. We will see
how this could be designed and how it can be used to get better higher-level
logical representation of user-defined theories.
|
WRS 2005
Implementing an evaluator for mini-ML in ATS: a case study of
combining programming with theorem proving
|
|
Hongwei Xi
(Boston, USA)
|
|
WRS 2004
|
Normalization by Evaluation
|
|
Olivier Danvy
(University of Aarhus, Denmark)
|
|
Reduction cycles
|
|
Jan Willem Klop
(Vrije Universiteit Amsterdam, The Netherlands)
|
|
WRS 2003
|
Strategies and User Interfaces in Maude
|
|
Manuel Clavel
(Universidad Complutense de Madrid, Spain)
|
Maude is a high-level language and a high-performance system supporting
executable specification and declarative programming in rewriting logic.
Rewriting logic is reflective, in the sense of being able to express
its own metalevel at the object level. Reflection is systematically
exploited in Maude endowing the language with powerful metaprogramming
capabilities. We explain and illustrate with examples two of
these reflective features: user-definable declarative strategies and user-definable
declarative interfaces. We conclude with an application, namely, an
inductive theorem prover, whose implementation effectively combines
both reflective features.
|
Rewrite Strategies in the Rewriting Calculus
|
|
Claude Kirchner (LORIA - INRIA Lorraine, France)
|
This talk presents an overview on the use of the rewriting
calculus to express rewrite strategies. We motivate first the use
of rewrite strategies by examples in the ELAN language. We
then show how this has be modelled in the initial version of the
rewriting calculus and how the matching power of this
framework facilitates the writing of powerful strategies.
|
WRS 2002
|
Approximations for Strategies and Termination
|
|
Aart Middeldorp
(Tsukuba University, Japan)
|
In the talk we illustrate the use of approximations and tree
automata techniques to define optimal normalizing strategies
for large classes of first-order rewrite systems. We further
show how the very same ideas can be used to improve the
dependency pair method for proving termination of rewrite
systems automatically. If time permits, we present a new and
computationally less expensive improvement for the latter.
|
Optimal Strategies in Higher-Order Rewriting
|
|
Vincent van Oostrom (Univ. of Utrecht, The Netherlands)
|
In a so-called optimal implementation of a term rewriting system,
only needed redexes are contracted and all redex-patterns in a term
which have the same history along the reduction,
are kept shared in the graph implementation of the term.
Such an implementation crucially relies on the notion of
`being the same along a reduction' of redex-patterns
in particular, and of parts of terms in general.
Lévy gave three ways to characterize this notion of sameness,
in the case of the lambda-calculus. Via:
- Labelling
- Extraction
- Zig-zag
We are performing a similar program for left-linear
(first- and higher-order) term rewriting systems.
This requires general notions of, among others,
permutation equivalence, labelling, residuals, and tracing.
We present and relate these for the case of term rewriting,
all based on the technical tool of proof terms
(witnessing proofs in Meseguer's rewriting logic).
We conclude by presenting an extension of the
lambda-calculus with an end-of-scope operator,
which came up naturally, while extending the optimal
first-order setting to higher-order.
The rough idea is that a role of the lambda is
to open a scope and it is only natural to introduce
an explicit operator to end a scope.
The nice thing is that (an extension of)
beta-reduction can be defined which is confluent
without alpha-reduction. Alpha reduction is
only needed when removing end-of-scopes.
(This calculus is halfway toward an optimal implementation of
the lambda calculus: for that also the explicit operators
for (un)sharing, the so-called fan-in and fan-out,
need to be introduced.)
The first part of the talk is based on Chapter 8, joint work with
Roel de Vrijer,
of the forthcoming book on
Term Rewriting Systems, by Terese.
The second part of the talk on the lambda calculus with scopes,
is based on joint work (in progress) with
Dimitri Hendriks
who's also working on a
formalization in Coq.
The extension to higher-order is joint work-in-progress
with Sander Bruggink.
|
WRS 2001
|
Evaluation Strategies for Functional Logic Programming
|
|
Sergio Antoy
(Portland State University, USA)
|
Recent advances in the foundations and the development of functional
logic programming languages originate from far-reaching results on narrowing
evaluation strategies. Narrowing is a computation similar to rewriting
which yields substitutions in addition to normal forms. In functional logic programming,
the classes of rewrite systems to which narrowing is applied are, for
the most part, subclasses of the constructor-based, possibly conditional, rewrite
systems. Many interesting narrowing strategies, particularly for the smallest subclasses
of the constructor-based rewrite systems, are generalizations of well-known
rewrite strategies. However, some strategies for larger non-confluent subclasses
have been developed just for functional logic computations. In this paper,
I will discuss the elements that play a relevant role in evaluation strategies for
functional logic programming, describe some important classes of rewrite systems
that model functional logic programs, show examples of the differences in
expressiveness provided by these classes, and review the characteristics of narrowing
strategies proposed for each class of rewrite systems.
|
Slides
|
A Survey of Strategies in Program Transformation Systems
|
|
Eelco Visser (Univ. of Utrecht, The Netherlands)
|
Program transformation is used in a wide range of applications including compiler
construction, optimization, program synthesis, refactoring, software renovation, and
reverse engineering. Complex program transformations are achieved through a number
of consecutive modifications of a program. Transformation rules define basic
modifications. A transformation strategy is an algorithm for choosing a path in
the rewrite relation induced by a set of rules. This paper surveys the support for
the definition of strategies in program transformation systems. After a discussion
of kinds of program transformation and choices in program representation, the basic
elements of a strategy system are discussed and the choices in the design of a
strategy language are considered. Several styles of strategy systems as provided in
existing languages are then analyzed.
|
|