Showing 1–9 of 9 results for author: Eguchi, N

Formalizing Termination Proofs under Polynomial Quasi-interpretations

Authors: Naohi Eguchi

Abstract: 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 tree, no naive formalization of termination proofs yields a connection to the polynomial complexity of the given program. We solve this problem employing the notion of minimal function graph, a set of pairs of a term and it… ▽ More 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 tree, no naive formalization of termination proofs yields a connection to the polynomial complexity of the given program. We solve this problem employing the notion of minimal function graph, a set of pairs of a term and its normal form, which is defined as the least fixed point of a monotone operator. We show that termination proofs for programs reducing under lexicographic path orders (LPOs for short) and polynomially quasi-interpretable can be optimally performed in a weak fragment of Peano arithmetic. This yields an alternative proof of the fact that every function computed by an LPO-terminating, polynomially quasi-interpretable program is computable in polynomial space. The formalization is indeed optimal since every polynomial-space computable function can be computed by such a program. The crucial observation is that inductive definitions of minimal function graphs under LPO-terminating programs can be approximated with transfinite induction along LPOs. △ Less

Submitted 10 September, 2015; originally announced September 2015.

Comments: In Proceedings FICS 2015, arXiv:1509.02826

Journal ref: EPTCS 191, 2015, pp. 33-47

Complexity Analysis of Precedence Terminating Infinite Graph Rewrite Systems

Authors: Naohi Eguchi

Abstract: 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, Martini and Zorzi, in which the size of every normal form by innermost rewriting is polynomially bounded. Every unfolding graph rewrite rule is precedence terminating in the sense of Middeldorp, Ohsaki and Zantema. Although… ▽ More 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, Martini and Zorzi, in which the size of every normal form by innermost rewriting is polynomially bounded. Every unfolding graph rewrite rule is precedence terminating in the sense of Middeldorp, Ohsaki and Zantema. Although precedence terminating infinite rewrite systems cover all the primitive recursive functions, in this paper we consider graph rewrite systems precedence terminating with argument separation, which form a subclass of precedence terminating graph rewrite systems. We show that for any precedence terminating infinite graph rewrite system G with a specific argument separation, both the runtime complexity of G and the size of every normal form in G can be polynomially bounded. As a corollary, we obtain an alternative proof of the original result by Dal Lago et al. △ Less

Submitted 26 May, 2015; originally announced May 2015.

Comments: In Proceedings TERMGRAPH 2014, arXiv:1505.06818. arXiv admin note: text overlap with arXiv:1404.6196

ACM Class: I.2.2; F.1.1; F.1.3; F.4.1;

Journal ref: EPTCS 183, 2015, pp. 33-47

Proving Termination of Unfolding Graph Rewriting for General Safe Recursion

Authors: Naohi Eguchi

Abstract: 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 form of safe recursion. We introduce a termination order over sequences of terms together with an interpretation of term graphs into sequences of terms. Unfolding graph rewrite rules expressing general safe recursion can b… ▽ More 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 form of safe recursion. We introduce a termination order over sequences of terms together with an interpretation of term graphs into sequences of terms. Unfolding graph rewrite rules expressing general safe recursion can be successfully embedded into the termination order by the interpretation, yielding the polynomial runtime complexity. Moreover, generalising the definition of unfolding graph rewrite rules for general safe recursion, we propose a new criterion for the polynomial runtime complexity of infinite GRSs and for the polynomial size of normal forms in infinite GRSs. △ Less

Submitted 20 June, 2014; v1 submitted 24 April, 2014; originally announced April 2014.

Comments: Technical report

A New Term Rewriting Characterisation of ETIME functions

Authors: Martin Avanzini, Naohi Eguchi

Abstract: 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), that is sound and complete for ETIME computable functions. The proposed reduction order for ETIME makes contrasts to those related complexity classes clear. 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), that is sound and complete for ETIME computable functions. The proposed reduction order for ETIME makes contrasts to those related complexity classes clear. △ Less

Submitted 30 December, 2013; v1 submitted 27 December, 2013; originally announced December 2013.

Comments: Technical report

Predicative Lexicographic Path Orders: An Application of Term Rewriting to the Region of Primitive Recursive Functions

Authors: Naohi Eguchi

Abstract: 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 as lexicographic path orders, several non-trivial primitive recursive equations, e.g., primitive recursion with parameter substitution, unnested multiple recursion, or simple nested recursion, can be oriented with PLPOs… ▽ More 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 as lexicographic path orders, several non-trivial primitive recursive equations, e.g., primitive recursion with parameter substitution, unnested multiple recursion, or simple nested recursion, can be oriented with PLPOs. It can be shown that the PLPO however only induces primitive recursive upper bounds on derivation lengths of compatible rewrite systems. This yields an alternative proof of a classical fact that the class of primitive recursive functions is closed under those non-trivial primitive recursive equations. △ Less

Submitted 2 June, 2014; v1 submitted 1 August, 2013; originally announced August 2013.

Comments: Technical Report

ACM Class: F.4.1; F.3.3

A New Order-theoretic Characterisation of the Polytime Computable Functions

Authors: Martin Avanzini, Naohi Eguchi, Georg Moser

Abstract: We propose a new order, the small polynomial path order (sPOP* for short). The order sPOP* provides a characterisation of the class of polynomial time computable function via term rewrite systems. Any polynomial time computable function gives rise to a rewrite system that is compatible with sPOP*. On the other hand any function defined by a rewrite system compatible with sPOP* is polynomial time c… ▽ More We propose a new order, the small polynomial path order (sPOP* for short). The order sPOP* provides a characterisation of the class of polynomial time computable function via term rewrite systems. Any polynomial time computable function gives rise to a rewrite system that is compatible with sPOP*. On the other hand any function defined by a rewrite system compatible with sPOP* is polynomial time computable. Technically sPOP* is a tamed recursive path order with product status. Its distinctive feature is the precise control provided. For any rewrite system that is compatible with sPOP* that makes use of recursion up to depth d, the (innermost) runtime complexity is bounded from above by a polynomial of degree d. △ Less

Submitted 16 January, 2012; v1 submitted 12 January, 2012; originally announced January 2012.

Comments: Technical Report

ACM Class: F.2.2; F.4.1; F.4.2; D.2.4; D.2.8

A term-rewriting characterization of PSPACE

Authors: Naohi Eguchi

Abstract: Isabel Oitavem has introduced a term rewriting system (TRS) which captures the class FPS of polynomial-space computable functions. We propose an alternative TRS for FPS. As a consequence, it is obtained that FPS is the smallest class containing certain initial functions and closed under specific operations. It turns out that our characterization is relatively simple and suggests an uniform approac… ▽ More Isabel Oitavem has introduced a term rewriting system (TRS) which captures the class FPS of polynomial-space computable functions. We propose an alternative TRS for FPS. As a consequence, it is obtained that FPS is the smallest class containing certain initial functions and closed under specific operations. It turns out that our characterization is relatively simple and suggests an uniform approach to the space-complexity. △ Less

Submitted 2 January, 2012; originally announced January 2012.

Comments: In: T. Arai, C. T. Chong, R. Downey, J. Brendle, Q. Feng, H. Kikyo and H. Ono, editors, Proceedings of the 10th Asian Logic Conference 2008, World Scientific, 2010

A Path Order for Rewrite Systems that Compute Exponential Time Functions (Technical Report)

Authors: Martin Avanzini, Naohi Eguchi, Georg Moser

Abstract: In this paper we present a new path order for rewrite systems, the exponential path order EPOSTAR. Suppose a term rewrite system is compatible with EPOSTAR, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPOSTAR equals the class of functions computable in exponentia… ▽ More In this paper we present a new path order for rewrite systems, the exponential path order EPOSTAR. Suppose a term rewrite system is compatible with EPOSTAR, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPOSTAR equals the class of functions computable in exponential time on a Turing maschine. △ Less

Submitted 9 June, 2011; v1 submitted 6 October, 2010; originally announced October 2010.

Comments: Technical Report

MSC Class: 03D15

A new function algebra of EXPTIME functions by safe nested recursion

Authors: Toshiyasu Arai, Naohi Eguchi

Abstract: Bellantoni and Cook have given a function-algebra characterization of the polynomial-time computable functions via an unbounded recursion scheme which is called safe recursion. Inspired by their work, we characterize the exponential-time computable functions with the use of a safe variant of nested recursion. Bellantoni and Cook have given a function-algebra characterization of the polynomial-time computable functions via an unbounded recursion scheme which is called safe recursion. Inspired by their work, we characterize the exponential-time computable functions with the use of a safe variant of nested recursion. △ Less

Submitted 5 March, 2008; v1 submitted 27 July, 2006; originally announced July 2006.

ACM Class: F.4.1; F.1.1; F.1.3