12 citations · 17 across the 11 of their papers we have counts for
11 papers
Formalizing Termination Proofs under Polynomial Quasi-interpretations
Naohi Eguchi
Usual termination proofs for a functional program require to check all the possible reduction paths. Due to an exponential gap between the height and size of such the reduction tre…
Complexity Analysis of Precedence Terminating Infinite Graph Rewrite Systems
Naohi Eguchi
The general form of safe recursion (or ramified recurrence) can be expressed by an infinite graph rewrite system including unfolding graph rewrite rules introduced by Dal Lago, Mar…
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
Naohi Eguchi
In this paper we present a new termination proof and complexity analysis of unfolding graph rewriting which is a specific kind of infinite graph rewriting expressing the general fo…
A New Term Rewriting Characterisation of ETIME functions
Martin Avanzini, Naohi Eguchi
Adopting former term rewriting characterisations of polytime and exponential-time computable functions, we introduce a new reduction order, the Path Order for ETIME (POE* for short…
Predicative Lexicographic Path Orders: An Application of Term Rewriting to the Region of Primitive Recursive Functions
Naohi Eguchi
In this paper we present a novel termination order the {\em predicative lexicographic path order} (PLPO for short), a syntactic restriction of the lexicographic path order. As well…
Characterising Complexity Classes by Inductive Definitions in Bounded Arithmetic
Naohi Eguchi
Famous descriptive characterisations of P and PSPACE are restated in terms of the Cook-Nguyen style second order bounded arithmetic. We introduce an axiom of inductive definitions…