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

I wanna draw like you: Inter-and intra-individual differences in orang-utan drawings

Authors: Marie Pelé, Gwendoline Thomas, Alaïs Liénard, Nagi Eguchi, Masaki Shimada, Cédric Sueur

Abstract: Recently discovered, the oldest human abstract drawing is around 73,000 years. Although the origins of drawing behaviour have remained an enigma to this day, light may be shone on the subject through its study among our closest neighbours, the great apes. This study analyses 749 drawings of five female Bornean orang-utans (Pongo pygmaeus) at Tama Zoological Park in Japan. We searched for differenc… ▽ More Recently discovered, the oldest human abstract drawing is around 73,000 years. Although the origins of drawing behaviour have remained an enigma to this day, light may be shone on the subject through its study among our closest neighbours, the great apes. This study analyses 749 drawings of five female Bornean orang-utans (Pongo pygmaeus) at Tama Zoological Park in Japan. We searched for differences between individuals but also tried to identify possible temporal changes among the drawings of one individual, Molly, who drew almost 1,300 drawings from 2006 to 2016. A classical analysis of the drawings was carried out after collecting quantitative and qualitative variables. Our findings reveal evidence of differences in the drawing style of the five individuals as well as creative changes in Molly's drawing style throughout her lifetime. Individuals differed in terms of the colours used, the space they filled but also the shapes (fan patterns, circles or loops) they drew. Molly drew less and less as she grew older, and we found a significant difference between drawings produced in winter, when orang-utans were kept inside and had less activity, and those produced during other seasons. Our results suggest that the drawing behaviour of these five orangutans is not random and that differences among individuals might reflect differences of styles, states of mind but also motivation to draw. These novel results are a significant contribution to our understanding of how drawing behaviour evolved in hominids. △ Less

Submitted 14 September, 2021; originally announced September 2021.

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

Characterising Complexity Classes by Inductive Definitions in Bounded Arithmetic

Authors: Naohi Eguchi

Abstract: 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 over second order bounded arithmetic. We show that P can be captured by the axiom of inflationary inductive definitions whereas PSPACE can be captured by the axiom of non-inflationary inductive definitions. 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 over second order bounded arithmetic. We show that P can be captured by the axiom of inflationary inductive definitions whereas PSPACE can be captured by the axiom of non-inflationary inductive definitions. △ Less

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

Comments: Technical report

Synthesis of New Layered Oxypnictides Sr2CrO2(FeAs)2

Authors: Naoya Eguchi, Fumihiro Ishikawa, Michihiro Kodama, Takeshi Wakabayashi, Atsuko Nakayama, Ayako Ohmura, Yuh Yamada

Abstract: We successfully synthesized new layered iron oxypnictide Sr2CrO2(FeAs)2 by solid-state-reaction techniques. This is the first report on the Fe-substituted Sr2Mn3As2O2-type oxypnictides to our knowledge. A pellet of stoichiometric mixtures of SrO, Cr and FeAs wrapped with tantalum foil was sintered at 900°C for 96 h. Results of x-ray diffraction measurement and Rietveld refinements show that the st… ▽ More We successfully synthesized new layered iron oxypnictide Sr2CrO2(FeAs)2 by solid-state-reaction techniques. This is the first report on the Fe-substituted Sr2Mn3As2O2-type oxypnictides to our knowledge. A pellet of stoichiometric mixtures of SrO, Cr and FeAs wrapped with tantalum foil was sintered at 900°C for 96 h. Results of x-ray diffraction measurement and Rietveld refinements show that the structure of the sample belongs to the space group of I4/mmm with the lattice constants of a = 3.9948(1) Å and c = 18.447(1) Å. Temperature dependence of the resistivity for Sr2CrO2(FeAs)2 shows semiconductor-like behavior. Additionally, the sample does not exhibit superconducting transition in measurements of resistivity and magnetization even in the low temperature down to 3 K. △ Less

Submitted 28 February, 2013; originally announced February 2013.

Comments: 6 pages, 4 figures, accepted for publication in Journal of the Physical Society of Japan

Journal ref: J. Phys. Soc. Jpn., Vol.82, No.4, p.045002 (2013)

A Simplified Characterisation of Provably Computable Functions of the System ID_1 of Inductive Definitions

Authors: Naohi Eguchi, Andreas Weiermann

Abstract: We present a simplified and streamlined characterisation of provably total computable functions of the theory ID_1 of non-iterated inductive definitions. The idea of the simplification is to employ the method of operator-controlled derivations that was originally introduced by Wilfried Buchholz and afterwards applied by the second author to a characterisation of provably total computable functions… ▽ More We present a simplified and streamlined characterisation of provably total computable functions of the theory ID_1 of non-iterated inductive definitions. The idea of the simplification is to employ the method of operator-controlled derivations that was originally introduced by Wilfried Buchholz and afterwards applied by the second author to a characterisation of provably total computable functions of Peano arithmetic PA. △ Less

Submitted 13 May, 2012; originally announced May 2012.

Comments: Technical Report

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

NMR and Neutron Scattering Studies of Quasi One-Dimensional Magnet CuV_2O_6

Authors: Jun Kikuchi, Kazuhiro Ishiguchi, Kiyoichiro Motoya, Masayuki Itoh, Kazunori Inari, Naotoshi Eguchi, Jun Akimitsu

Abstract: Magnetic properties of a quasi one-dimensional magnet CuV_2O_6 have been studied by means of susceptibility measurement, NMR and powder neutron diffraction. Cu^{2+} spins (S=1/2) order antiferromagnetically below 22.6 K, and the saturation moment is about 0.70 μ_{B} at 0 K. The magnetic structure determined in the present study indicates that in CuV_2O_6 one-dimensional antiferromagnetic spin ch… ▽ More Magnetic properties of a quasi one-dimensional magnet CuV_2O_6 have been studied by means of susceptibility measurement, NMR and powder neutron diffraction. Cu^{2+} spins (S=1/2) order antiferromagnetically below 22.6 K, and the saturation moment is about 0.70 μ_{B} at 0 K. The magnetic structure determined in the present study indicates that in CuV_2O_6 one-dimensional antiferromagnetic spin chains are along [110], suggesting a dominant antiferromagnetic exchange interaction between the next-nearest-neighbor spins rather than the nearest-neighbor ones. △ Less

Submitted 26 May, 2000; v1 submitted 13 April, 2000; originally announced April 2000.

Comments: 9 pages, 12 embedded eps figures uses JPSJ.sty, accepted for publication in J. Phys. Soc. Jpn

Journal ref: J. Phys. Soc. Jpn. 69, 2660 (2000)