Rewriting and Typed Lambda Calculi

We demonstrate a tight relationship between linearly typed

π

-calculi and typed

λ

-calculi by giving a type-preserving translation from the call-by-value

λμ

-calculus into a typed

π

-calculus. The

λμ

-calculus has a particularly simple representation as typed mobile processes. The target calculus is a simple variant of the linear

π

-calculus. We establish full abstraction up to maximally consistent observational congruences in source and target calculi using techniques from games semantics and process calculi.

The focus will be a presentation of new results and successes of semantic analyses of concurrent programs. These are accomplished by contextual equivalence, observing may- and should-convergence, and by adapting known techniques from deterministic programs to non-determinism and concurrency. The techniques are context lemmata, diagram techniques, applicative similarities, infinite tree reductions, and translations. The results are equivalences, correctness of program transformations, correctness of implementations and translations.

Inductive data such as finite lists and trees can elegantly be defined by constructors which allow programmers to analyze and manipulate finite data via pattern matching. Dually, coinductive data such as streams can be defined by observations such as head and tail and programmers can synthesize infinite data via copattern matching. This leads to a symmetric language where finite and infinite data can be nested. In this paper, we compile nested pattern and copattern matching into a core language which only supports simple non-nested (co)pattern matching. This core language may serve as an intermediate language of a compiler. We show that this translation is conservative, i.e. the multi-step reduction relation in both languages coincides for terms of the original language. Furthermore, we show that the translation preserves strong and weak normalisation: a term of the original language is strongly/weakly normalising in one language if and only if it is so in the other. In the proof we develop more general criteria which guarantee that extensions of abstract reduction systems are conservative and preserve strong or weak normalisation.

The decreasing diagrams technique (van Oostrom, 1994) has been successfully used to prove confluence of rewrite systems in various ways; using rule-labelling (van Oostrom, 2008), it can also be applied directly to prove confluence of some linear term rewriting systems (TRSs) automatically. Some efforts for extending the rule-labelling are known, but non-left-linear TRSs are left beyond the scope. Two methods for automatically proving confluence of non-(left-)linear TRSs with the rule-labelling are given. The key idea of our methods is to combine the decreasing diagrams technique with persistency of confluence (Aoto & Toyama, 1997).

For an infinite-state concurrent system

$\mathcal{S}$

with a set

AP

of state predicates, its

predicate abstraction

defines a finite-state system whose states are subsets of

AP

, and its transitions

s

 → 

s

′ are witnessed by concrete transitions between states in

$\mathcal{S}$

satisfying the respective sets of predicates

s

and

s

′. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems

$\mathcal{S}$

described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method—based on rewriting, semantic unification, and variant narrowing—to automatically generate a predicate abstraction when the formal specification of

$\mathcal{S}$

is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.

We present an algebraic characterization of the complexity classes

Logspace

and

NLogspace

, using an algebra with a composition law based on unification. This new bridge between unification and complexity classes is inspired from proof theory and more specifically linear logic and Geometry of Interaction.

We show how unification can be used to build a model of computation by means of specific subalgebras associated to finite permutation groups.

We then prove that whether an observation (the algebraic counterpart of a program) accepts a word can be decided within logarithmic space. We also show that the construction can naturally encode pointer machines, an intuitive way of understanding logarithmic space computing.

Ramsey Theorem for pairs is a combinatorial result that cannot be intuitionistically proved. In this paper we present a new form of Ramsey Theorem for pairs we call

H

-closure Theorem.

H

-closure is a property of well-founded relations, intuitionistically provable, informative, and simple to use in intuitionistic proofs. Using our intuitionistic version of Ramsey Theorem we intuitionistically prove the Termination Theorem by Poldenski and Rybalchenko. This theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using an intuitionistic version of Ramsey Theorem different from our one. Our long-term goal is to extract effective bounds for the while-programs from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal.

We show how to construct a logical relation for countable nondeterminism in a guarded type theory, corresponding to the internal logic of the topos

Sh

ω

1

of sheaves over

ω

1

. In contrast to earlier work on abstract step-indexed models, we not only construct the logical relations in the guarded type theory, but also give an internal proof of the adequacy of the model with respect to standard contextual equivalence. To state and prove adequacy of the logical relation, we introduce a new propositional modality. In connection with this modality we show why it is necessary to work in the logic of bf Sh

ω

1

.

Deduction modulo is a framework in which theories are integrated into proof systems such as natural deduction or sequent calculus by presenting them using rewriting rules. When only terms are rewritten, cut admissibility in those systems is equivalent to the confluence of the rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This is no longer true when considering rewriting rules involving propositions. In this paper, we show that, in the same way that it is possible to recover confluence using Knuth-Bendix completion, one can regain cut admissibility in the general case using standard saturation techniques. This work relies on a view of proposition rewriting rules as oriented clauses, like term rewriting rules can be seen as oriented equations. This also leads us to introduce an extension of deduction modulo with

conditional

term rewriting rules.

We implement an online judge for context-free grammars. Our system contains a list of problems describing formal languages, and asking for grammars generating them. A submitted proposal grammar receives a verdict of acceptance or rejection depending on whether the judge determines that it is equivalent to the reference solution grammar provided by the problem setter. Since equivalence of context-free grammars is an undecidable problem, we consider a maximum length ℓ and only test equivalence of the generated languages up to words of length ℓ. This length restriction is very often sufficient for the well-meant submissions. Since this restricted problem is still NP-complete, we design and implement methods based on hashing, SAT, and automata that perform well in practice.

We define the tree automata with height constraints between brothers (

TACBB

H

). Constraints of equalities and inequalities between heights of siblings that restrict the applicability of the rules are allowed in

TACBB

H

. These constraints allow to express natural tree languages like complete or balanced (like AVL) trees. We prove decidability of emptiness and finiteness for

TACBB

H

, and also for a more general class that additionally allows to combine equality and disequality constraints between brothers.

We give a coinductive proof of confluence, up to equivalence of root-active subterms, of infinitary lambda-calculus. We also show confluence of Böhm reduction (with respect to root-active terms) in infinitary lambda-calculus. In contrast to previous proofs, our proof makes heavy use of coinduction and does not employ the notion of descendants.

We define the class of

constrained cons-free

rewriting systems and show that this class characterizes

P

, the set of languages decidable in polynomial time on a deterministic Turing machine. The main novelty of the characterization is that it allows very liberal properties of term rewriting, in particular non-deterministic evaluation: no reduction strategy is enforced, and systems are allowed to be non-confluent.

The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected.

We propose a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We then prove soundness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.

We propose an abstract datatype for a closed interval of real numbers to type theory, providing a representation-independent approach to programming with real numbers. The abstract datatype requires only function types and a natural numbers type for its formulation, and so can be added to any type theory that extends Gödel’s System T. Our main result establishes that programming with the abstract datatype is equivalent in power to programming intensionally with representations of real numbers. We also consider representing arbitrary real numbers using a mantissa-exponent representation in which the mantissa is taken from the abstract interval.

We revisit lambda encodings of data, proposing new solutions to several old problems, in particular dependent elimination with lambda encodings. We start with a type-assignment form of the Calculus of Constructions, restricted recursive definitions and Miquel’s implicit product. We add a type construct

ιx

.

T

, called a

self type

, which allows

T

to refer to the subject of typing. We show how the resulting System

S

with this novel form of dependency supports dependent elimination with lambda encodings, including induction principles. Strong normalization of

S

is established by defining an erasure from

S

to a version of

F

ω

with positive recursive type definitions, which we analyze. We also prove type preservation for

S

.

This paper discusses the method of

formative rules

for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known

usable rules

, formative rules allow dropping some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the technique.

In this paper we present a simple technique for analysing the runtime complexity of rewrite systems. In complexity analysis many techniques are based on reduction orders. We show how the monotonicity condition for orders can be weakened by using the notion of context-sensitive rewriting. The presented technique is very easy to implement, even in a modular setting, and has been integrated in the Tyrolean Complexity Tool. We provide ample experimental data for assessing the viability of our method.

We introduce a novel resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the innermost runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system

$\mathcal R$

can be well-typed, then there exists a polynomial interpretation that orients

$\mathcal R$

. For this we adequately adapt the standard notion of polynomial interpretations to the typed setting.

Knuth and Bendix showed that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. We show that this is still true of a rewrite system

${R_{\textit{T}}} \cup{R_{\textit{NT}}} $

such that

$R_{\textit{T}}$

is terminating and

$R_{\textit{NT}}$

is a left-linear, rank non-increasing, possibly non-terminating rewrite system. Confluence can then be reduced to the joinability of the critical pairs of

$R_{\textit{T}}$

and to the existence of decreasing diagrams for the critical pairs of

$R_{\textit{T}}$

inside

$R_{\textit{NT}}$

as well as for the rigid parallel critical pairs of

$R_{\textit{NT}}$

.

We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. Transfinite reductions can be faithfully represented as infinitary proof terms, unique up to infinitary associativity. We use proof terms to define equivalence of transfinite reductions on the basis of permutation equations. A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.

In this work we present a paradigm of focusing proof search based on an incremental construction of

retractile

(i.e,

correct

or

sequentializable

) proof structures of the pure (units free) multiplicative and additive fragment of linear logic. The correctness of proof construction steps (or expansion steps) is ensured by means of a system of graph retraction rules; this graph rewriting system is shown to be convergent, that is, terminating and confluent. Moreover, the proposed proof construction follows an optimal (parsimonious, indeed) retraction strategy that, at each expansion step, allows to take into account (abstract) graphs that are ”smaller” (w.r.t. the size) than the starting proof structures.

We establish that the local state monad introduced by Plotkin and Power is a monad with graded arities in the category [

Inj

,

Set

]. From this, we deduce that the local state monad is associated to a graded Lawvere theory

which is presented by generators and relations, depicted in the graphical language of string diagrams.

The Λ

μ

-calculus is an extension of Parigot’s

λμ

-calculus. For the untyped Λ

μ

-calculus, Saurin proved some fundamental properties such as the standardization and the separation theorem. Nakazawa and Katsumata gave extensional models, called stream models, in which terms are represented as functions on streams. This paper introduces a conservative extension of the Λ

μ

-calculus, called Λ

μ

cons

, from which the open term model is straightforwardly constructed as a stream model, and for which we can define a reduction system satisfying several fundamental properties such as confluence, subject reduction, and strong normalization.

We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union

$\mathcal{P}+\mathcal{Q}$

of two PTSs

$\mathcal{P}$

and

$\mathcal{Q}$

, the PTS

$\forall\mathcal{P}.\mathcal{Q}$

which intuitively captures the “

$\mathcal{Q}$

-logic of

$\mathcal{P}$

-terms” and poly

${\mathcal{P}}$

which intuitively denotes the predicative polymorphism extension of

$\mathcal{P}$

.

These results suggest a new approach to the study of the meta-theory of PTSs, by examination of the relationships between different calculi and predicative extensions which allow more expressiveness with equivalent logical strength.

Motivated by the question whether sound and expressive applicative similarities for program calculi with should-convergence exist, this paper investigates expressive applicative similarities for the untyped call-by-value lambda-calculus extended with McCarthy’s ambiguous choice operator amb. Soundness of the applicative similarities w.r.t. contextual equivalence based on may- and should-convergence is proved by adapting Howe’s method to should-convergence. As usual for nondeterministic calculi, similarity is not complete w.r.t. contextual equivalence which requires a rather complex counter example as a witness. Also the call-by-value lambda-calculus with the weaker nondeterministic construct erratic choice is analyzed and sound applicative similarities are provided. This justifies the expectation that also for more expressive and call-by-need higher-order calculi there are sound and powerful similarities for should-convergence.

We show that provability in the implicational fragment of relevance logic is complete for doubly exponential time, using reductions to and from coverability in branching vector addition systems.

A connection between lambda calculus and the algebra of near semi-rings is discussed. Among the results is the following completeness theorem.

A first-order equation in the language of binary associative distributive algebras is true in all such algebras if and only if the interpretations of the first order terms as lambda terms beta-eta convert to one another. A similar result holds for equations containing free variables.

This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g. concurrent) languages, referred to as

all-path reachability logic

. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized (Coq). This approach is implemented in a tool for semantics-based verification as part of the

$\mathbb K$

framework.

Monotone algebras are frequently used to generate reduction orders in automated termination and complexity proofs. To be able to certify these proofs, we formalized several kinds of interpretations in the proof assistant Isabelle/HOL. We report on our integration of matrix interpretations, arctic interpretations, and nonlinear polynomial interpretations over various domains, including the reals.

This paper describes the

Con

ditional

Con

fluence tool, a fully automatic confluence checker for first-order conditional term rewrite systems. The tool implements various confluence criteria that have been proposed in the literature. A simple technique is presented to test conditional critical pairs for infeasibility, which makes conditional confluence criteria more useful. Detailed experimental data is presented.

This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the strong cooperation with external SMT solvers. We present some new ideas that contribute to the efficiency and power of the tool.

String rewriting can not only be applied on strings, but also on cycles and even on general graphs. In this paper we investigate termination of string rewriting applied on cycles, shortly denoted as cycle rewriting, which is a strictly stronger requirement than termination on strings. Most techniques for proving termination of string rewriting fail for proving termination of cycle rewriting, but match bounds and some variants of matrix interpretations can be applied. Further we show how any terminating string rewriting system can be transformed to a terminating cycle rewriting system, preserving derivational complexity.