Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 61 - 80 of about 247 ／ All the affair displays >>

Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems Reviewed

Naoki Nishida and Yuya Maeda

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs Vol. 108 page： 26:1-26:20 2018.6

Authorship：Lead author Language：English

A narrowing tree for a constructor term rewriting system and a pair of terms is a finite representation for the space of all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. Narrowing trees have grammar representations that can be considered regular tree grammars. Innermost narrowing is a counterpart of constructor-based rewriting, and thus, narrowing trees can be used in analyzing constructor-based rewriting to normal forms. In this paper, using grammar representations, we extend narrowing trees to syntactically deterministic conditional term rewriting systems that are constructor systems. We show that narrowing trees are useful to prove two properties of a normal conditional term rewriting system: one is infeasibility of conditional critical pairs and the other is quasi-reducibility.

DOI： 10.4230/LIPIcs.FSCD.2018.26

Confluence Competition 2018

Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs Vol. 108 page： 32:1-32:5 2018.6

CauDEr: A Causal-Consistent Reversible Debugger for Erlang Reviewed

Ivan Lanese, Naoki Nishida, Adrian Palacios, and German Vidal

Proceedings of the 14th International Conference on Functional and Logic Programming, Lecture Notes in Computer Scienc Vol. 10818 page： 247-263 2018.4

Language：English

Programming languages based on the actor model, such as Erlang, avoid some concurrency bugs by design. However, other concurrency bugs, such as message order violations and livelocks, can still show up in programs. These hard-to-find bugs can be more easily detected by using causal-consistent reversible debugging, a debugging technique that allows one to traverse a computation both forward and backward. Most notably, causal consistency implies that, when going backward, an action can only be undone provided that its consequences, if any, have been undone beforehand. To the best of our knowledge, we present the first causal-consistent reversible debugger for Erlang, which may help programmers to detect and fix various kinds of bugs, including message order violations and livelocks.

DOI： 10.1007/978-3-319-90686-7_16

Rewriting induction for constrained inequalities Reviewed

Takahiro Nagao and Naoki Nishida

Science of Computer Programming Vol. 155 page： 76-102 2018.4

Language：English Publishing type：Research paper (scientific journal)

Rewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities within such frameworks, one may reduce inequalities to equations. However, it is often hard to prove inductive validity of such reduced equations within the existing RI frameworks due to their indirect handling of inequalities. In this paper, we adapt the notion of inductive theorems to inequalities and propose an RI framework for directly proving inductive validity of inequalities of constrained term rewriting systems. Direct handling of inequalities enables us to utilize transitivity of binary predicates via application of induction hypotheses. Our framework succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations. For the sake of automated reasoning, we provide a strategy for applying inference rules and evaluate its performance by means of an implementation.

DOI： 10.1016/j.scico.2017.10.012

Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction Reviewed

Shinnosuke Mizutani and Naoki Nishida

Electronic Proceedings in Theoretical Computer Science Vol. 265 page： 35-51 2018.2

Language：English

A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of the program w.r.t. the Hoare triple. The transformation enables us to apply techniques for proving termination of constrained rewriting to proving total correctness of programs together with proof tableaux for partial correctness.

DOI： 10.4204/EPTCS.265.4

Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers Reviewed

Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama

Electronic Proceedings in Theoretical Computer Science Vol. 265 page： 83-97 2018.2

Language：English

In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences of integers, and they play an important role for the success of proving termination, especially for constrained rewriting systems. In this paper, we show sufficient conditions of linear polynomial interpretations for transforming dependency chains into bounded monotone (i.e., decreasing or increasing) sequences of integers. Such polynomial interpretations transform rewrite sequences of the original system into decreasing or increasing sequences independently of the transformation of dependency chains. When we transform rewrite sequences into increasing sequences, polynomial interpretations have non-positive coefficients for reducible positions of marked function symbols. We propose four DP processors parameterized by transforming dependency chains and rewrite sequences into either decreasing or increasing sequences of integers, respectively. We show that such polynomial interpretations make us succeed in proving termination of the McCarthy 91 function over the integers.

DOI： 10.4204/EPTCS.265.7

Reversible computation in term rewriting Reviewed

Naoki Nishida, Adrian Palacios, and German Vidal

Journal of Logical and Algebraic Methods in Programming Vol. 94 page： 128-149 2018.1

Language：English Publishing type：Research paper (scientific journal)

Essentially, in a reversible programming language, for each forward computation from state S to state S', there exists a constructive method to go backwards from state S' to state S. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few.

In this work, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step t1 -> t2, we do not always have a decidable method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define two transformations, injectivization and inversion, to make a rewrite system reversible using standard term rewriting. We illustrate the usefulness of our transformations in the context of bidirectional program transformation.

DOI： 10.1016/j.jlamp.2017.10.003

CO3 (Version 1.4)

Naoki Nishida, Yoshiaki Kanazawa,, and Karl Gmeiner

Proceedings of the 5th International Workshop on Confluence (IWC 2016) page： 73 2017.9

A Reversible Semantics for Erlang Reviewed

Naoki Nishida, Adrian Palacios, and German Vidal

Revised Selected Papers of the 26th International Conference on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science (LOPSTR 2016) Vol. 10184 page： 259-274 2017.7

Authorship：Lead author Language：English

In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for debugging and for enforcing fault-tolerance, among others. In this paper, we consider a subset of Erlang, a concurrent language based on the actor model, and formally introduce a semantics for reversible computation. To the best of our knowledge, this is the first attempt to define a reversible semantics for Erlang.

DOI： 10.1007/978-3-319-63139-4_15

A compiler that translates to Malbolge from a C-language subset containing recursive calls

Genki Sakanashi, Shohei Kobe, Masahiko Sakai, Naoki Nishida, and Kenji Hashimoto

IEICE Technical Rerport Vol. 117 ( 136 ) page： 145-150 2017.7

Language：Japanese

Malbolge is an esoteric programming language, which is promising to protect intellectual property rights due to its difficulty of analysis. It is, however, very difficult to program because of its peculiar instructions. Tackling this problem, pseudo-instruction sequences was developed as an intermediate language for generating Malbolge programs. Nevertheless it is still difficult to program compared with ordinary languages like C. In this article, we present how to implement a compiler that translates to Malbolge from a C-language subset containing the integer type, the Boolean type, basic control structures such as while statement, and recursive calls. In the implementation, we firstly added array syntax and function syntax to pseudo-instruction sequences, and strengthen existing tools for the extention to conform with it. We next propose a translation method from C-language subset to pseudo-instruction sequences.

Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Integers

Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama

IEICE Technical Rerport Vol. 117 ( 136 ) page： 139-144 2017.7

Language：Japanese

In dependency pair framework for proving termination of constrained term rewriting systems, polynomial interpretations that transform dependency chains representing sequences of relevant function calls into bounded decreasing sequences of integers play an important role for the success of proving termination. In this article, we propose polynomial interpretations that transform dependency chains into bounded decreasing sequences but transform rewrite sequences of the original system into increasing sequences.We also propose polynomial interpretations that transform dependency chains into bounded increasing sequences of integers.
We report empirical comparison results between the proposed polynomial interpretations.

Verifying Procedural Programs via Constrained Rewriting Induction Reviewed

Carsten Fuhs, Cynthia Kop, and Naoki Nishida

ACM Transactions on Computational Logic Vol. 18 ( 2 ) page： 14:1-14:50 2017.6

Language：English Publishing type：Research paper (scientific journal)

This article aims to develop a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend transformation methods based on integer term rewriting systems to handle arbitrary data types, global variables, function calls, and arrays, and to encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations; thus, in contrast to other works, we do not require an explicit specification in a separate specification language.

DOI： 10.1145/3060143

Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness

Takayuki Kuroda, Naoki Nishida, and Hiroyuki Seki

IEICE Technical Rerport Vol. 116 ( 512 ) page： 103-108 2017.3

Language：Japanese

A transformational approach to confluence proofs for conditional term rewriting systems (CTRS) has been investigated, but confluence of a CTRS defining sorting over natural numbers has not been proved yet by any existing confluence prover. Such a CTRS defines behavior of function symbols hierarchically, called a hierarchical CTRS, and is not sufficiently complete. In this article, we propose a method to prove confluence of hierarchical CTRSs that are not sufficiently complete. More precisely, we first extend rewriting induction for conditional equations to TRSs that are not sufficiently complete, and then we prove joinability of a conditional critical pair by inducing other conditions from the original conditional part. Next, we design a simplification order that takes conditional parts of rewrite rules into account, and propose a method to prove termination of hierarchical CTRSs by means of the designed simplification order.

Relative Termination via Dependency Pairs Reviewed

Jose Iborra, Naoki Nishida, German Vidal, and Akihisa Yamada

Journal of Automated Reasoning Vol. 58 ( 3 ) page： 391-411 2017.3

Language：English Publishing type：Research paper (scientific journal)

A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.

DOI： 10.1007/s10817-016-9373-5

Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems Reviewed

Ryota Nakayama, Naoki Nishida, and Masahiko Sakai

Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), Electronic Proceedings in Theoretical Computer Science Vol. 235 page： 62-77 2017.1

Language：English

In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is a sound structure-preserving transformation for weakly-left-linear deterministic conditional term rewriting systems. More precisely, we show that every weakly-left-linear deterministic conditional term rewriting system can be converted to an equivalent weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting system and prove that the SR transformation is sound for weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting systems. Here, soundness for a conditional term rewriting system means that reduction of the transformed unconditional term rewriting system creates no undesired reduction sequence for the conditional system.

DOI： 10.4204/EPTCS.235.5

arXiv

Notes on Confluence of Ultra-WLL SDCTRSs via a Structure-Preserving Transformation Reviewed

Naoki Nishida

Proceedings of the 5th International Workshop on Confluence (IWC 2016) page： 60-64 2016.9

Authorship：Lead author Language：English

A structure-preserving transformation proposed by Serbanuta and Rosu for strongly or syntactically deterministic conditional term rewriting systems (SDCTRSs) that are ultra-left-linear has been shown to be applicable to weakly-left-linear (WLL) and ultra-WLL SDCTRSs without any change, and sound for such DCTRSs even if they are not SDCTRSs. In this paper, we show a confluent, WLL, and ultra-WLL DCTRS that is not an SDCTRS such that the transformed TRS is not confluent. We also show that for a WLL and ultra-WLL SDCTRS, if the transformed TRS is confluent, then so is the SDCTRS.

CO3 (Version 1.3)

Naoki Nishida, Takayuki Kuroda, and Karl Gmeiner

Proceedings of the 5th International Workshop on Confluence (IWC 2016) page： 74 2016.9

Proving inductive validity of constrained inequalities Reviewed

Takahiro Nagao and Naoki Nishida

Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016) page： 50-61 2016.9

Language：English Publishing type：Research paper (scientific journal)

Rewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities within such frameworks, one may reduce inequalities to equations. However, it is often hard to prove inductive validity of such reduced equations within the existing RI frameworks due to their indirect handling of inequalities. In this paper, we adapt the notion of inductive theorems to inequalities and propose an RI framework for directly proving inductive validity of inequalities of constrained term rewriting systems. Within the framework, we handle inequalities that may contain function symbols defined in a given rewriting system but not necessarily interpreted by the built-in semantics. Direct handling of inequalities facilitates the utilization of transitivity of magnitude relations via inequalities obtained as induction hypotheses. Our approach succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations.

DOI： 10.1145/2967973.2968598

An intermediate language for a compiler generating highly obfuscated Malbolge codes

Shohei Kobe, Masahiko Sakai, Naoki Nishida, and Hiroyuki Seki

IEICE Technical Rerport Vol. 116 ( 127 ) page： 105-110 2016.7

Reversible Term Rewriting Reviewed

Naoki Nishida, Adrian Palacios, and German Vidal

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), LIPIcs Vol. 52 page： 28:1-28:18 2016.6

Language：English

Essentially, in a reversible programming language, for each forward computation step from state S to state S', there exists a constructive and deterministic method to go backwards from state S' to state S. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few. In this paper, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step t1 -> t2, we do not always have a decidable and deterministic method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define a transformation to make a rewrite system reversible using standard term rewriting.

DOI： 10.4230/LIPIcs.FSCD.2016.28

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki