Weak Reduction and Garbage Collection in
Interaction Nets
Jorge Sousa Pinto
(Universidade do Minho, Braga, Portugal)
This paper presents an implementation device for the
weak reduction of interaction nets to interface normal form.
The results produced by running several benchmarks are given,
suggesting that weak reduction greatly improves the performance
of the interaction combinators-based implementation of the
$\lambda$-calculus.
Simulating Liveness by Reduction Strategies
Jürgen Giesl
(RWTH Aachen, Germany)
Hans Zantema
(Eindhoven University of Technology, The Netherlands)
In this paper we define a general framework to handle liveness and
related properties by appropriate reduction strategies in abstract
reduction and term rewriting. Classically, reduction strategies in
rewriting are used to simulate the evaluation process in
programming languages. The aim of our work is to use reduction
strategies to also study liveness questions which are of high
importance in practice (e.g., in protocal verification for
distributed processes). In particular, we show how the problem of
verifying liveness properties is related to termination of term
rewrite systems (TRSs). Using our results, techniques for proving
termination of TRSs can be used to verify liveness properties.
Innermost Reductions Find All Normal Forms
on Right-Linear Terminating Overlay TRSs
Masahiko Sakai
(Nagoya University, Japan)
Koji Okamoto
(Nagoya University, Japan)
Toshiki Sakabe
(Nagoya University, Japan)
A strategy of TRSs is said to be complete if all normal forms
of a given term are reachable from the term. We show the innermost
strategy is complete for terminating, right-linear and overlay
TRSs. This strategy is fairly efficient to calculate all normal forms
of a given term by searching reduction trees.
Call-by-value, call-by-name, and strong normalization for the
classical sequent calculus
Stéphane Lengrand
(ENS Lyon, France)
We present a typed calculus $\lambda\xi$ isomorphic to the
implicational fragment of the classical calculus LK. Reductions in
LK eliminate the cut-rule by local rewriting steps, which
correspond to the computation of explicit substitutions. This
bridges the gap between Curien and Herbelin's
$\bar{\lambda}\mu\bar{\mu}$-calculus and Urban's rewriting system
for proofs. Encodings of one into the other are defined, and from
them we derive the strong normalization of
$\bar{\lambda}\mu\bar{\mu}$, as well as a denotational semantics
of continuations for two strategies CBV and CBN that we have
identified in Urban's rewriting system.
A Rewriting Strategy for Protocol Verification
(Extended Abstract)
Monica Nesi
(Università degli Studi di L'Aquila, Italy)
Giuseppina Rucci
(Università degli Studi di L'Aquila, Italy)
Massimo Verdesca
(Università degli Studi di L'Aquila, Italy)
This paper presents a rewriting strategy for the analysis and verification
of communication protocols. In a way similar to the approximation technique
defined by Genet and Klay, a rewrite system R specifies the protocol
and a tree automaton A describes the initial set of communication
requests. Given a term t that represents a property to be proved,
a rewriting strategy is defined that suitably expands and reduces t
using the rules in R and the transitions in A to derive whether or not
t is recognized by the intruder.
This is done by simulating a completion process in a bottom-up manner
starting from t and trying to derive a transition t -> q_f from
critical pairs, where q_f is a final state of the tree automaton.
The rewriting strategy is defined by means of a set of inference rules
and used for reasoning about the authentication and secrecy properties
of the Needham-Schroeder public-key protocol.
Call-by-Need Reductions for Membership
Conditional Term Rewriting Systems
Mizuhito Ogawa
(Japan Science and Technology Corporation, Tokyo, Japan)
This paper proves that, for a membership
conditional
term rewriting system R,
(1) a reducible term has a needed redex if R is
nonoverlapping,
and (2) whether a redex is nv-needed is decidable.
An Abstract Concept of Optimal Implementation
Zurab Khasidashvili
(Intel, IDC, Haifa, Israel)
John Glauert
(School of Information Systems, UEA, Norwich, England)
In previous works, we introduced \emph{Stable Deterministic
Residual Structures} (SDRSs), Abstract Reduction Systems with an
axiomatized residual relation which model orthogonal term and
graph rewriting systems, and \emph{Deterministic Family
Structures} (DFSs), which add an axiomatized notion of
\emph{redex-family} to capture known \emph{sharing} concepts in
the \lc\ and other orthogonal rewrite systems. In this paper, we
introduce and study a concept of \emph{implementation} of DFSs. We
show that for any DFS $\cal F$, its implementation ${\cal F}_I$ is
a non-duplicating DFSs with zig-zag as the family relation, where
zig-zag is simply the symmetric and transitive closure of the
residual relation on redexes with histories. Further, we show that
sharing is compositional: the sharing in a DFS $\calF$ can be
decomposed into a weaker sharing $\calF'$ (such as zig-zag) and a
sharing in the implementation $\calF'_I$ of $\calF'$ stronger than
zig-zag. These results require study of the family relation in
non-duplicating SDRSs. We show that zig-zag forms a
family-relation in every non-duplicating SDRS, and that it is the
only \emph{separable} family relation in such SDRSs.