|
|
Rewriting is an important branch of theoretical
computer science which combines elements of logic and
mathematics. The Fourth International School on
Rewriting (ISR'09) will be held at Universidade de
Brasília, the week
before RDP'09, the
Federated Conference on Rewriting, Deduction, and
Programming. The school is organized for Master and
PhD students, researches and practitioners interested in
the study of rewriting concepts and applications. In
addition, the school is divided in two tracks (A and B)
in order to accommodate the different backgrounds of the
participants. The courses allocated on track A are for
the participants without previous exposure to rewriting,
while the courses on track B are advanced lectures on
recent developments and applications.
The lectures will be given by some of the
best experts on rewriting and applications.
The following
lecturers have been confirmed:
Franz
Baader (TU Dresden) - Introduction
to Term Rewriting (Track A)
Term rewriting systems can be used to compute in structures that are
defined by equations. They are thus an important tool in automated
deduction, algebraic specification, and functional programming. The
course introduces important properties such as termination and
confluence of term rewriting systems, describes methods for proving
termination and confluence, and shows how Knuth-Bendix completion can
(sometimes) be used to make non-confluent term rewriting systems
confluent. It can be used by the participants to acquaint or
re-acquaint themselves with the basic notions and results from the
area before taking more specialized or advanced courses.
Maribel
Fernandez (King's College London) -
Nominal Rewriting (Track B)
Nominal rewriting is a generalisation of first-order rewriting that
allows us to deal with terms involving binding operators in an elegant
and practical way. In the nominal approach, bound entities are
explicitly named (rather than using a nameless syntax such as de
Bruijn indices), yet we get a rewriting formalism that respects
alpha-equivalence and can be directly implemented. Nominal rewriting
can be seen as a form of higher-order rewriting with a first-order
syntax and built-in alpha-equivalence. Nominal systems maintain a
strict distinction between atoms (variables that may be bound by a
special abstraction operation) and meta-variables (or just variables)
which cannot be bound, giving the framework a pronounced first-order
character since substitution is not capture-avoiding. In the course,
we will introduce the nominal approach to the specification of systems
with binding operators, and we will show how good properties of
first-order rewriting are inherited by the nominal rewriting
framework. We will describe an efficient matching algorithm that has
been used to implement a nominal rewriting tool.
Bernhard
Gramlich (TU Wien) - Advanced
Course on Conditional Rewriting (Track B)
Conditional Term Rewriting Systems (CTRSs) extend ordinary Term
Rewriting Systems (TRSs) by allowing conditions in rewrite
rules. This is a very natural and conceptually adequate extension of
basic term rewriting. Although in many examples, from a purely
computational point of view, conditions in rewrite rules can be
avoided by an appropriate encoding within an unconditional framework,
the resulting encodings are not easy to understand and to analyze. For
that reason conditional term rewriting as such has been studied for a
long time, with the goal of extending the basic elegant and rich
theory of unconditional term rewriting to the conditional case as much
as possible. Yet, it has turned out that many results, approaches,
techniques and computational properties do not carry over easily, but
need to be carefully adapted to make sense. In the course, starting
with a thorough discussion of the basic notions and fundamental
problems in conditional rewriting, a selection of the following
topics will be covered (including exercises):
basic format, types, classes and notions of (first-order) CTRSs
fundamental differences/difficulties/problems as compared to TRSs
confluence and (effective) termination properties: notions,
(un)decidability, criteria, proof techniques
CTRSs and functional-logic programming
computatonal versus logical strength (logicality)
modularity in conditional rewriting
transformations from CTRSs to TRSs: soundness, completeness
expressiveness of CTRSs as compared to TRSs
Traditional and non Traditional Typed λ-calculi (Track A)
TBA
Extensions of Typed λ-calculi with
Applications in Logic, Programming Languages and Formalisation
of Mathematics (Track B)
TBA
Delia Kesner
(Université Paris Diderot (VII))
- Higher-order Rewriting with
Resources (Track B)
Higher-order rewriting can be understood as a formalism allowing the
transformation of terms with bound variables. Different formalisms
exist to specify such transformations, all of them are based on a
meta-level operation called higher-order substitution. This operation
has been deeply studied in the framework of the lambda-calculus
which can be seen as a paradigmatic example of higher-order rewriting system.
Different lambda-calculi with explicit resources (contraction,
weakening and substitution) were developed in order to
internalise/implement the complex notion of meta-level
substitution. The course will survey research in the area of calculi
with explicit resources, by putting emphasis on motivations, history,
formalisms and properties. A formal correspondence between
lambda-calculus with explicit substitutions and Multiplicative
Exponential Linear Logic Proof-Nets will be established.
Aart
Middeldorp (Universität Innsbruck) -
Advanced Topics in Termination (Track B)
The course aims to give an impression of the state of the art
in termination research. The focus will be on methods that are
implemented in modern termination tools. The following topics
will be covered:
polynomial interpretations over various domains
matrix and arctic interpretations
dependency pairs
match-bounds
semantic labeling
derivational complexity
decidable classes
Introduction to
Tree Automata (Track A) In 1960's tree automata
originated as tree acceptors branched from context-free grammar.
Over the decades since then, tree automata techniques have been
developed as a theoretical tool reasoning about questions over
trees in various areas, such as for protocol analysis, sub-typing
in programming language and formula manipulation of decidable
second-order logics. In the course, first we review the classical
(word) automata. We then introduce the concept of bottom-up tree
automata, as a natural extension of word automata, and as a
sub-class of ground rewriting, specifically, each of whose rewrite
rules is formed of either f(p1,...pn) -> q or p -> q, where f is a
function symbol and others are special constants, called "states."
Related properties including Pumping lemma, closure properties and
decidability are also explained as a counterpart of ones in word
automata. This lecture is based on Sections 1-3 in
my
lecture note.
Equational Tree Automata (Track
B) It is known that tree automata are closely
related to context-free grammar, in fact, the leaf language of
trees accepted by a regular tree automaton is a context-free
language, and conversely, the set of derivation trees generated by
a context-free grammar is a tree language accepted by a (regular)
tree automaton. But, therefore, tree encoding by tree automata is
no longer powerful enough to express commutative languages,
semi-linear sets or linear arithmetic. It turns out that in tree
languages, equational (for example, associative and/or
commutative) closure of regular tree languages are no longer
handled by tree automata. The course focuses on equational tree
languages (tree languages modulo equational theory) and related
topics. We learn the concept of equational tree automata, in
particular, in the two cases of AC theory and A theory. The course
also surveys the concept of commutative grammars and related
topics including Parikh's theorem for semi-linear sets. This
course is based on Sections 7 and 8 in
my
lecture note.
Luca Paolini
(Università di Torino) -
Parametric Lambda Calculus (Track B)
There is a gap between real functional programming languages and
lambda-calculus. The majority of real functional languages have a
"call-by-value" parameter passing policy, while the
reduction rule of lambda-calculus reflects a "call-by-name" policy.
In the folklore there was the idea that a call-by-value behavior could
be mimicked in lambda-calculus just by defining a suitable reduction
strategy.
Plotkin proved that this intuition was wrong and that lambda-calculus
is intrinsically call-by-name. So, in order to describe the
call-by-value evaluation, he proposed a different calculus, which has
the same syntax as lambda-calculus, but a different reduction rule.
The parametric lambda-calculus has the same syntax of lambda-calculus
and it is endowed by a reduction rule parametric with respect to a
subset Delta of lambda-terms (called the set of input values) that
enjoy some suitable conditions.
Different choices of Delta allow us to define different calculus,
in particular both classical and call-by-value lambda-calculus.
The most interesting feature of parametric
lambda-calculus is that it is possible to prove important properties
(like confluence) for a large class of languages in just one step.
Thus the parametric lambda-calculus can be seen
as the foundation of functional programming.
We present the parametric lambda-calculus together with some of its main
syntactical and semantic properties, on which their status of
paradigmatic programming languages is based.
Indicative Content Summary: parametric lambda-calculus, confluence,
standardization, operational semantics and theories,
other gadgets (computational power, separability, models).
Organizing
Committee
| Flávio L. C. de Moura |
Brasília, Brazil |
| Mauricio Ayala-Rincón |
Brasília, Brazil |
| Alberto Pardo |
Montevideo, Uruguay |
| Eduardo Bonelli |
Buenos Aires, Argentina |
Steering Committee
| Jürgen Giesl |
Aachen |
| Claude Kirchner |
Bordeaux |
| Pierre Lescanne |
Lyon |
| Christopher Lynch |
Potsdam |
| Aart Middeldorp |
Innsbruck |
| Femke van Raamsdonk |
Amsterdam |
| Yoshihito Toyama |
Sendai |
Previous editions of ISR
ISR'06
ISR'07
ISR'08
|
