scholarly journals Critical Pair Analysis in Nominal Rewriting

10.29007/7q54 ◽  
2018 ◽  
Author(s):  
Takaki Suzuki ◽  
Kentaro Kikuchi ◽  
Takahito Aoto ◽  
Yoshihito Toyama
Keyword(s):  
Order Term ◽  
Term Rewriting ◽  
Critical Pair ◽  
Binding Mechanism ◽  
First Order ◽  
Rewrite Rules ◽  
Critical Pair Analysis ◽  
Orthogonal Systems ◽  
Pair Analysis ◽  
Critical Pairs

Nominal rewriting (Fernández, Gabbay & Mackie, 2004;Fernández & Gabbay, 2007) is a framework that extendsfirst-order term rewriting by a binding mechanismbased on the nominal approach (Gabbay & Pitts, 2002;Pitts, 2003). In this paper, we investigate confluenceproperties of nominal rewriting, following the study oforthogonal systems in (Suzuki et al., 2015), but herewe treat systems in which overlaps of the rewrite rulesexist. First we present an example where choice ofbound variables (atoms) of rules affects joinability ofthe induced critical pairs. Then we give a detailedproof of the critical pair lemma, and illustrate someof its applications including confluence results fornon-terminating systems.

scholarly journals A rewriting calculus for cyclic higher-order term graphs

2007 ◽  
Vol 17 (3) ◽  
pp. 363-406 ◽  
Author(s):  
PAOLO BALDAN ◽  
CLARA BERTOLISSI ◽  
HORATIU CIRSTEA ◽  
CLAUDE KIRCHNER
Keyword(s):  
Order Term ◽  
Equational Theory ◽  
Term Rewriting ◽  
Higher Order ◽  
Graph Representation ◽  
First Order ◽  
Rewrite Rules ◽  
Evaluation Mechanism ◽  
Matching Constraints ◽  
Higher Order Term

The Rewriting Calculus (ρ-calculus, for short) was introduced at the end of the 1990s and fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the structured results obtained are first class objects of the calculus. The evaluation mechanism, which is a generalisation of beta-reduction, relies strongly on term matching in various theories.In this paper we propose an extension of the ρ-calculus, called ρg-calculus, that handles structures with cycles and sharing rather than simple terms. This is obtained by using recursion constraints in addition to the standard ρ-calculus matching constraints, which leads to a term-graph representation in an equational style. Like in the ρ-calculus, the transformations are performed by explicit application of rewrite rules as first-class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.We show that the ρg-calculus, under suitable linearity conditions, is confluent. The proof of this result is quite elaborate, due to the non-termination of the system and the fact that ρg-calculus-terms are considered modulo an equational theory. We also show that the ρg-calculus is expressive enough to simulate first-order (equational) left-linear term-graph rewriting and α-calculus with explicit recursion (modelled using a letrec-like construct).

Modularity of strong normalization in the algebraic-λ-cube

1997 ◽  
Vol 7 (6) ◽  
pp. 613-660 ◽  
Author(s):  
FRANCO BARBANERA ◽  
MARIBEL FERNÁNDEZ ◽  
HERMAN GEUVERS
Keyword(s):  
Higher Order ◽  
Strong Normalization ◽  
First Order ◽  
Order Algebraic ◽  
General Schema ◽  
Rewrite Rules ◽  
Modular Property ◽  
Critical Pairs

In this paper we present the algebraic-λ-cube, an extension of Barendregt's λ-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all the systems in the algebraic-λ-cube, provided that the first-order rewrite rules are non-duplicating and the higher-order rules satisfy the general schema of Jouannaud and Okada. We also prove that local confluence is a modular property of all the systems in the algebraic-λ-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence.

Term graph narrowing

1996 ◽  
Vol 6 (6) ◽  
pp. 649-676 ◽  
Author(s):  
Annegret Habel ◽  
Detlef Plump
Keyword(s):  
General Solution ◽  
Order Term ◽  
Term Rewriting ◽  
Term Rewriting Systems ◽  
Graph Rewriting ◽  
First Order ◽  
Improve Efficiency ◽  
Rewriting Systems ◽  
Solving Equations

We introduce term graph narrowing as an approach for solving equations by transformations on term graphs. Term graph narrowing combines term graph rewriting with first-order term unification. Our main result is that this mechanism is complete for all term rewriting systems over which term graph rewriting is normalizing and confluent. This includes, in particular, all convergent term rewriting systems. Completeness means that for every solution of a given equation, term graph narrowing can find a more general solution. The general motivation for using term graphs instead of terms is to improve efficiency: sharing common subterms saves space and avoids the repetition of computations.

Cut rules and explicit substitutions

2001 ◽  
Vol 11 (1) ◽  
pp. 131-168 ◽  
Author(s):  
RENÉ VESTERGAARD ◽  
JOE WELLS
Keyword(s):  
Order Term ◽  
Term Rewriting ◽  
Cut Elimination ◽  
Cut Rule ◽  
Logical Deduction ◽  
Rewriting Systems ◽  
Explicit Substitution ◽  
Explicit Substitutions ◽  
Rewrite Rules ◽  
De Bruijn Indices

We introduce a method to associate calculi of proof terms and rewrite rules with cut elimination procedures for logical deduction systems (i.e., Gentzen-style sequent calculi) in the case of intuitionistic logic. We illustrate this method using two different versions of the cut rule for a variant of the intuitionistic fragment of Kleene's logical deduction system G3.Our systems are in fact calculi of explicit substitution, where the cut rule introduces an explicit substitution and the left-→ rule introduces a binding of the result of a function application. Cut propagation steps of cut elimination correspond to propagation of explicit substitutions, and propagation of weakening (to eliminate it) corresponds to propagation of index-updating operations. We prove various subject reduction, termination, and confluence properties for our calculi.Our calculi improve on some earlier calculi for logical deduction systems in a number of ways. By using de Bruijn indices, our calculi qualify as first-order term rewriting systems (TRS's), allowing us to use correctly certain results for TRS's about termination. Unlike in some other calculi, each of our calculi has only one cut rule and we do not need unusual features of sequents.We show that the substitution and index-updating mechanisms of our calculi work the same way as the substitution and index-updating mechanisms of Kamareddine and Ríos' λs and λt, two well-known systems of explicit substitution for the standard λ-calculus. By a change in the format of sequents, we obtain similar results for a known λ-calculus with variables and explicit substitutions, Rose's λbxgc.

Sign in / Sign up

Export Citation Format

Share Document