arXiv subjects

Keisuke Nakano

Publications and source records attributed to Keisuke Nakano.

8 recordsLinked to original sources

arXiv2024

Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)

We study the termination of sole combinatory calculus, which consists of only one combinator. Specifically, the termination for non-erasing combinators is disproven by finding a desirable tree automaton with a SAT solver as done for term rewriting systems by Endrullis and Zantema. We improved their technique to apply to non-erasing sole combinatory calculus, in which it suffices to search for tree automata with a final sink state. Our method succeeds in disproving the termination of 8 combinators, whose termination has been an open problem.

cs.LO↗

arXiv2024

Deciding Linear Height and Linear Size-to-Height Increase for Macro Tree Transducers

We present a novel normal form for (total deterministic) macro tree transducers (mtts), called depth proper normal form. If an mtt is in this normal form, then it is guaranteed that each parameter of each state of the mtt appears at arbitrary depth in the output trees of that state. Intuitively, if some parameter only appears at certain bounded depths in the output trees of a state, then this parameter can be removed by in-lining the corresponding output paths at each call site of that state. We use regular look-ahead in order to determine which of the paths should be in-lined. As a consequence of changing the lookahead, a parameter that was previously appearing at unbounded depths, may be appearing at bounded depths for some new look-ahead; for this reason, our construction has be iterated in order to obtain an mtt in depth-normal form. Using the normal form, we can decide whether the translation of an mtt has linear height increase or has linear size-to-height increase.

cs.FL↗

arXiv2020

On properties of $B$-terms

$B$-terms are built from the $B$ combinator alone defined by $B\equivλfgx. f(g~x)$, which is well known as a function composition operator. This paper investigates an interesting property of $B$-terms, that is, whether repetitive right applications of a $B$-term cycles or not. We discuss conditions for $B$-terms to have and not to have the property through a sound and complete equational axiomatization. Specifically, we give examples of $B$-terms which have the cyclic property and show that there are infinitely many $B$-terms which do not have the property. Also, we introduce another interesting property about a canonical representation of $B$-terms that is useful to detect cycles, or equivalently, to prove the cyclic property, with an efficient algorithm.

cs.LO↗

arXiv2019

Towards a Complete Picture of Lens Laws

Bidirectional transformation, also called lens, has played important roles in maintaining consistency in many fields of applications. A lens is specified by a pair of forward and backward functions which relate to each other in a consistent manner. The relation is formalized as a set of equations called lens laws. This report investigates precise dependencies among lens laws: which law implies another and which combination of laws implies another. The set of such implications forms a complicated graph structure. It would be helpful to check a well-definedness of bidirectional transformation in a lightweight way.

cs.PL↗

arXiv2018

Making View Update Strategies Programmable - Toward Controlling and Sharing Distributed Data -

Views are known mechanisms for controlling access of data and for sharing data of different schemas. Despite long and intensive research on views in both the database community and the programming language community, we are facing difficulties to use views in practice. The main reason is that we lack ways to directly describe view update strategies to deal with the inherent ambiguity of view updating. This paper aims to provide a new language-based approach to controlling and sharing distributed data based on views, and establish a software foundation for systematic construction of such data management systems. Our key observation is that a view should be defined through a view update strategy rather than a view definition. We show that Datalog can be used for specifying view update strategies whose unique view definition can be automatically derived, present a novel P2P-based programmable architecture for distributed data management where updatable views are fully utilized for controlling and sharing distributed data, and demonstrate its usefulness through the development of a privacy-preserving ride-sharing alliance system.

cs.DB↗

arXiv2018

A View-based Programmable Architecture for Controlling and Integrating Decentralized Data

The view and the view update are known mechanism for controlling access of data and for integrating data of different schemas. Despite intensive and long research on them in both the database community and the programming language community, we are facing difficulties to use them in practice. The main reason is that we are lacking of control over the view update strategy to deal with inherited ambiguity of view update for a given view. This vision paper aims to provide a new language-based approach to controlling and integrating decentralized data based on the view, and establish a software foundation for systematic construction of such data management systems. Our key observation is that a view should be defined through a view update strategy rather than a query. In other words, the view definition should be extracted from the view update strategy, which is in sharp contrast to the traditional approaches where the view update strategy is derived from the view definition. In this paper, we present the first programmable architecture with a declarative language for specifying update strategies over views, whose unique view definition can be automatically derived, and show how it can be effectively used to control data access, integrate data generally allowing coexistence of GAV (global as view) and LAV (local as view), and perform both analysis and updates on the integrated data. We demonstrate its usefulness through development of a privacy-preserving ride-sharing alliance system, discuss its application scope, and highlight future challenges.

cs.DB↗

arXiv2017

On repetitive right application of B-terms

B-terms are built from the B combinator alone defined by B f g x = f (g x), which is well-known as a function composition operator. This paper investigates an interesting property of B-terms, that is, whether repetitive right applications of a B-term circulates or not. We discuss conditions for B-terms to and not to have the property through a sound and complete equational axiomatization. Specifically, we give examples of B-terms which have the property and show that there are infinitely many B-terms which does not have the property. Also, we introduce a canonical representation of B-terms that is useful to detect cycles, or equivalently, to prove the property, with an efficient algorithm.

cs.LO↗

arXiv2013

XQuery Streaming by Forest Transducers

Streaming of XML transformations is a challenging task and only very few systems support streaming. Research approaches generally define custom fragments of XQuery and XPath that are amenable to streaming, and then design custom algorithms for each fragment. These languages have several shortcomings. Here we take a more principles approach to the problem of streaming XQuery-based transformations. We start with an elegant transducer model for which many static analysis problems are well-understood: the Macro Forest Transducer (MFT). We show that a large fragment of XQuery can be translated into MFTs --- indeed, a fragment of XQuery, that can express important features that are missing from other XQuery stream engines, such as GCX: our fragment of XQuery supports XPath predicates and let-statements. We then rely on a streaming execution engine for MFTs, one which uses a well-founded set of optimizations from functional programming, such as strictness analysis and deforestation. Our prototype achieves time and memory efficiency comparable to the fastest known engine for XQuery streaming, GCX. This is surprising because our engine relies on the OCaml built in garbage collector and does not use any specialized buffer management, while GCX's efficiency is due to clever and explicit buffer management.

cs.DB↗