Showing 1–11 of 11 results for author: Hirokawa, N

Left-Linear Completion with AC Axioms

Authors: Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp

Abstract: We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction o… ▽ More We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process. △ Less

Submitted 28 April, 2025; v1 submitted 27 May, 2024; originally announced May 2024.

Journal ref: Logical Methods in Computer Science, Volume 21, Issue 2 (April 29, 2025) lmcs:13670

Hydra Battles and AC Termination

Authors: Nao Hirokawa, Aart Middeldorp

Abstract: We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-MPO, a new AC compatible reduction order that can be see… ▽ More We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-MPO, a new AC compatible reduction order that can be seen as a much weakened version of AC-RPO. △ Less

Submitted 25 June, 2025; v1 submitted 26 July, 2023; originally announced July 2023.

Journal ref: Logical Methods in Computer Science, Volume 21, Issue 2 (June 27, 2025) lmcs:13184

Generalizing Weighted Path Orders

Authors: Teppei Saito, Nao Hirokawa

Abstract: We show that weighted path orders are special instances of a variant of semantic path orders. Exploiting this fact, we introduce a generalization of weighted path orders that goes beyond the realm of simple termination. Experimental data show that generalized weighted path orders are viable. We show that weighted path orders are special instances of a variant of semantic path orders. Exploiting this fact, we introduce a generalization of weighted path orders that goes beyond the realm of simple termination. Experimental data show that generalized weighted path orders are viable. △ Less

Submitted 26 July, 2023; originally announced July 2023.

Comments: Presented at WST 2023

Compositional Confluence Criteria

Authors: Kiraku Shintani, Nao Hirokawa

Abstract: We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for co… ▽ More We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for confluence analysis. In addition to them, we prove that Toyama's parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem. △ Less

Submitted 22 January, 2024; v1 submitted 7 March, 2023; originally announced March 2023.

Journal ref: Logical Methods in Computer Science, Volume 20, Issue 1 (January 23, 2024) lmcs:11045

Confluence by Critical Pair Analysis Revisited (Extended Version)

Authors: Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi

Abstract: We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating. We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating. △ Less

Submitted 3 June, 2019; v1 submitted 28 May, 2019; originally announced May 2019.

Comments: Added a reference to the conference version

Abstract Completion, Formalized

Authors: Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler

Abstract: Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of… ▽ More Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL. △ Less

Submitted 20 August, 2019; v1 submitted 23 February, 2018; originally announced February 2018.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (August 21, 2019) lmcs:4314

Critical Peaks Redefined - $Φ\sqcup Ψ= \top$

Authors: Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi

Abstract: Let a cluster be a term with a number of patterns occurring in it. We give two accounts of clusters, a geometric one as sets of (node and edge) positions, and an inductive one as pairs of terms with gaps (2nd order variables) and pattern-substitutions for the gaps. We show both notions of cluster and the corresponding refinement/coarsening orders on them, to be isomorphic. This equips clusters wit… ▽ More Let a cluster be a term with a number of patterns occurring in it. We give two accounts of clusters, a geometric one as sets of (node and edge) positions, and an inductive one as pairs of terms with gaps (2nd order variables) and pattern-substitutions for the gaps. We show both notions of cluster and the corresponding refinement/coarsening orders on them, to be isomorphic. This equips clusters with a lattice structure which we lift to (parallel/multi) steps to yield an alternative account of the notion of critical peak. △ Less

Submitted 25 August, 2017; originally announced August 2017.

Comments: 6th International Workshop on Confluence

Journal ref: In Proceedings of the 6th International Workshop on Confluence, pages 33 - 37, 2017

AC-KBO Revisited

Authors: Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp

Abstract: Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this paper we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is e… ▽ More Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this paper we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful version, and we modify the latter to amend its lack of monotonicity on non-ground terms. We further present new complexity results. An extension reflecting the recent proposal of subterm coefficients in standard Knuth-Bendix orders is also given. The various orders are compared on problems in termination and completion. △ Less

Submitted 21 March, 2015; v1 submitted 3 March, 2014; originally announced March 2014.

Comments: 31 pages, To appear in Theory and Practice of Logic Programming (TPLP) special issue for the 12th International Symposium on Functional and Logic Programming (FLOPS 2014)

Journal ref: Theory and Practice of Logic Programming 16 (2016) 163-188

Uncurrying for Innermost Termination and Derivational Complexity

Authors: Harald Zankl, Nao Hirokawa, Aart Middeldorp

Abstract: First-order applicative term rewriting systems provide a natural framework for modeling higher-order aspects. In earlier work we introduced an uncurrying transformation which is termination preserving and reflecting. In this paper we investigate how this transformation behaves for innermost termination and (innermost) derivational complexity. We prove that it reflects innermost termination and i… ▽ More First-order applicative term rewriting systems provide a natural framework for modeling higher-order aspects. In earlier work we introduced an uncurrying transformation which is termination preserving and reflecting. In this paper we investigate how this transformation behaves for innermost termination and (innermost) derivational complexity. We prove that it reflects innermost termination and innermost derivational complexity and that it preserves and reflects polynomial derivational complexity. For the preservation of innermost termination and innermost derivational complexity we give counterexamples. Hence uncurrying may be used as a preprocessing transformation for innermost termination proofs and establishing polynomial upper and lower bounds on the derivational complexity. Additionally it may be used to establish upper bounds on the innermost derivational complexity while it neither is sound for proving innermost non-termination nor for obtaining lower bounds on the innermost derivational complexity. △ Less

Submitted 17 February, 2011; originally announced February 2011.

Comments: In Proceedings HOR 2010, arXiv:1102.3465

Journal ref: EPTCS 49, 2011, pp. 46-57

Automated Complexity Analysis Based on the Dependency Pair Method

Authors: Nao Hirokawa, Georg Moser

Abstract: This article is concerned with automated complexity analysis of term rewrite systems. Since these systems underlie much of declarative programming, time complexity of functions defined by rewrite systems is of particular interest. Among other results, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. The established results… ▽ More This article is concerned with automated complexity analysis of term rewrite systems. Since these systems underlie much of declarative programming, time complexity of functions defined by rewrite systems is of particular interest. Among other results, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. The established results significantly extent previously known techniques: we give examples of rewrite systems subject to our methods that could previously not been analysed automatically. Furthermore, the techniques have been implemented in the Tyrolean Complexity Tool. We provide ample numerical data for assessing the viability of the method. △ Less

Submitted 1 June, 2011; v1 submitted 15 February, 2011; originally announced February 2011.

Comments: 37 pages, submitted to Information & Computation

Decreasing Diagrams and Relative Termination

Authors: Nao Hirokawa, Aart Middeldorp

Abstract: In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system R is confluent if all its critical pairs are joinable and the critical pair steps are relatively terminating with respect to R. We further show how to encode the rule-labeling heuristic for decreasing diagrams as a satisfiability problem. Experimental data for both methods are presented. In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system R is confluent if all its critical pairs are joinable and the critical pair steps are relatively terminating with respect to R. We further show how to encode the rule-labeling heuristic for decreasing diagrams as a satisfiability problem. Experimental data for both methods are presented. △ Less

Submitted 30 October, 2009; v1 submitted 15 October, 2009; originally announced October 2009.

Comments: v3: missing references added