Claude Kirchner

TCS Journal 2010 Journal Article

On the confluence of lambda-calculus with conditional rewriting

• Frédéric Blanqui
• Claude Kirchner
• Colin Riba

The confluence of untyped λ -calculus with unconditional rewriting is now well un- derstood. In this paper, we investigate the confluence of λ -calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether β -reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty’s result is improved from the assumption of strongly normalizing β -reduction to weakly normalizing β -reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.

I&C Journal 2010 Journal Article

Regaining cut admissibility in deduction modulo using abstract completion

• Guillaume Burel
• Claude Kirchner

Deduction modulo is a way to combine computation and deduction in proofs, by applying the inference rules of a deductive system (e. g. natural deduction or sequent calculus) modulo some congruence that we assume here to be presented by a set of rewrite rules. Using deduction modulo is equivalent to proving in a theory corresponding to the rewrite rules, and leads to proofs that are often shorter and more readable. However, cuts may be not admissible anymore. We define a new system, the unfolding sequent calculus, and prove its equivalence with the sequent calculus modulo, especially w. r. t. cut-free proofs. It permits to show that it is even undecidable to know if cuts can be eliminated in the sequent calculus modulo a given rewrite system. Then, to recover the cut admissibility, we propose a procedure to complete the rewrite system such that the sequent calculus modulo the resulting system admits cuts. This is done by generalizing the Knuth–Bendix completion in a non-trivial way, using the framework of abstract canonical systems. These results enlighten the entanglement between computation and deduction, and the power of abstract completion procedures. They also provide an effective way to obtain systems admitting cuts, therefore extending the applicability of deduction modulo in automated theorem proving.

TCS Journal 2006 Journal Article

Abstract canonical presentations

• Nachum Dershowitz
• Claude Kirchner

Solving goals—like proving properties, deciding word problems or resolving constraints—is much easier with some presentations of the underlying theory than with others. Typically, what have been called “completion processes”, in particular in the study of equational logic, involve finding appropriate presentations of a given theory to more easily solve a given class of problems. We provide a general proof-theoretic setting that relies directly on the fundamental concept of “good”, that is, normal-form, proofs, itself defined using well-founded orderings on proof objects. This foundational framework allows for abstract definitions of canonical presentations and very general characterizations of saturation and redundancy criteria.

LPAR Conference 2002 Conference Paper

Binding Logic: Proofs and Models

• Gilles Dowek
• Thérèse Hardin
• Claude Kirchner

Abstract We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there.

TCS Journal 2002 Journal Article

ELAN from a rewriting logic point of view

• Peter Borovanský
• Claude Kirchner
• Hélène Kirchner
• Pierre-Etienne Moreau

ELAN implements computational systems, a concept that combines two first class entities: rewrite rules and rewriting strategies. ELAN can be used either as a logical framework or to describe and execute deterministic as well as non-deterministic rule-based processes. With the general goal to make precise a rewriting logic-based semantics of ELAN, this paper has three contributions: a presentation of the concepts of rules and strategies available in ELAN, an expression of rewrite rules with matching conditions in conditional rewriting logic, and finally an enrichment mechanism of a rewrite theory into a strategy theory in conditional rewriting logic.

I&C Journal 2000 Journal Article

Higher Order Unification via Explicit Substitutions

• Gilles Dowek
• Thérèse Hardin
• Claude Kirchner

Higher order unification is equational unification for βη-conversion. But it is not first order equational unification, as substitution has to avoid capture. Thus, the methods for equational unification (such as narrowing) built upon grafting (i. e. , substitution without renaming) cannot be used for higher order unification, which needs specific algorithms. Our goal in this paper is to reduce higher order unification to first order equational unification in a suitable theory. This is achieved by replacing substitution by grafting, but this replacement is not straightforward as it raises two major problems. First, some unification problems have solutions with grafting but no solution with substitution. Then equational unification algorithms rest upon the fact that grafting and reduction commute. But grafting and βη-reduction do not commute in λ-calculus and reducing an equation may change the set of its solutions. This difficulty comes from the interaction between the substitutions initiated by βη-reduction and the ones initiated by the unification process. Two kinds of variables are involved: those of βη-conversion and those of unification. So, we need to set up a calculus which distinguishes between these two kinds of variables and such that reduction and grafting commute. For this purpose, the application of a substitution of a reduction variable to a unification one must be delayed until this variable is instantiated. Such a separation and delay are provided by a calculus of explicit substitutions. Unification in such a calculus can be performed by well-known algorithms such as narrowing, but we present a specialised algorithm for greater efficiency. At last we show how to relate unification in λ-calculus and in a calculus with explicit substitutions. Thus, we come up with a new higher order unification algorithm which eliminates some burdens of the previous algorithms, in particular the functional handling of scopes. Huet's algorithm can be seen as a specific strategy for our algorithm, since each of its steps can be decomposed into elementary ones, leading to a more atomic description of the unification process. Also, solved forms in λ-calculus can easily be computed from solved forms in λσ-calculus.

TCS Journal 1995 Journal Article

Editorial

• Claude Kirchner

TCS Journal 1991 Journal Article

Completion for unification

• Narjes Doggaz
• Claude Kirchner

Syntactic theories have the nice property that a unification algorithm may be computed directly from the form of the axioms of a specific presentation, called resolvent, of the theory. In this work we present and prove a completion algorithm that, for a given presentation, returns a resolvent set of axioms whenever it terminates.

TCS Journal 1990 Journal Article

Equational completion in order-sorted algebras

• Isabelle Gnaedig
• Claude Kirchner
• Héléne Kirchner

We describe and prove completion procedures for equational term rewriting systems in order-sorted algebras, using the technique of proof orderings. Problems specific to order-sorted equational logic are emphasized.