Language：English   Publishing type：Research paper (scientific journal)   Publisher：Elsevier BV  

During the past decade reversible programming languages have been formalized using various established semantics frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, even including the central question of whether the defined language is reversible. In this paper, we build a metalanguage foundation for reversible languages from categorical principles, based on the category of sets and partial injective functions. We exemplify our approach by a step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. The use of the metalanguage leads to a formalization of the reversible semantics. A language defined in the metalanguage is guaranteed to have reversibility and inverse semantics. Also, program inverters for this language are obtained for free. We further discuss applications and directions for reversible semantics.

DOI： 10.1016/j.tcs.2022.02.024

Web of Science

researchmap

Language：Japanese   Publishing type：Research paper (bulletin of university, research institution)  

DOI： 10.15119/00003946

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：World Scientific Pub Co Pte Lt  

We study the transition graph of generic Hamiltonian surface flows, whose vertices are the topological equivalence classes of generic Hamiltonian surface flows and whose edges are the generic transitions. Using the transition graph, we can describe time evaluations of generic Hamiltonian surface flows (e.g., fluid phenomena) as walks on the graph. We propose a method for constructing the complete transition graph of all generic Hamiltonian flows. In fact, we construct two complete transition graphs of Hamiltonian surface flows having three and four genus elements. Moreover, we demonstrate that a lower bound on the transition distance between two Hamiltonian surface flows with any number of genus elements can be calculated by solving an integer programming problem using vector representations of Hamiltonian surface flows.

File： ws20201028.pdf

DOI： 10.1142/S1793830921500233

Web of Science

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Springer International Publishing  

During the past decade, reversible programming languages have been formalized using various established semantic frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, and even neglect the central question of whether the defined language is reversible. In this paper, we build on a metalanguage foundation for reversible languages based on the category of sets and partial injective functions. We exemplify our approach through step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. This yields a formalization of the semantics in which the reversibility of the language and its inverse semantics are immediate, as well as the inversion of programs written in the language. We further discuss applications and future research directions for reversible semantics.

DOI： 10.1007/978-3-030-54997-8_26

researchmap

Other Link： https://dblp.uni-trier.de/db/conf/fm/fm2019w-2.html#GluckKY19

Publishing type：Research paper (international conference proceedings)  

DOI： 10.48550/arXiv.1910.10406

researchmap

Other Link： https://dblp.uni-trier.de/db/journals/corr/corr1910.html#abs-1910-10406

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

We cast two algorithms generating the inorder and preorder traversals of a binary tree in the context of reversible computing nearly three decades after they were first examined in the light of program inversion. The reversible traversals directly define the inverse algorithms that reconstruct the tree. They have the same linear time and space requirements as the traversals. A while-language is extended with reversible recursion.

DOI： 10.1016/j.ipl.2019.03.002

researchmap

Language：Japanese   Publisher：電子情報通信学会  

局所構造変換を繰り返し適用して，一般に観測される多重連結領域上の非圧縮流の全トポロジーを構成できることを示した．3種類の初期大域構造に対して，7種類の局所構造を置換するアプローチを取った．

DOI： 10.14923/transinfj.2018JDL8021

researchmap

Language：Japanese   Publisher：電子情報通信学会  

可逆システム上で非可逆プログラムの可逆シミュレーションを実現するとき，既知の一般解法を用いると，元の入出力の走査回数と，元の入出力用以外のメモリ使用量が増え，元の出力以外を出力してクリーンでなくなってしまうという問題が起こる．しかし，非可逆なアルゴリズムに対して，経験と勘を元に個別の非可逆プログラムの効率的なクリーン可逆シミュレーションが実現されてきている．本稿では，可逆計算システムで用いる可逆アルゴリズムとして，二分木の列挙，二分木の辞書順のランク計算，および辞書順における次の二分木の生成の効率的なクリーン可逆シミュレーションの構築をする．これらは基礎的な可逆アルゴリズムであるので，他の可逆アルゴリズムの一部として使用されたり，可逆アルゴリズムの構築法が利用されたりすることが期待される．また，二分木のランク計算に関する効率的な可逆プログラムの整備を進めることで類似するランク計算やさらには現時点では困難な一般の効率的可逆シミュレーションの自動導出が可能になることが期待される．本稿の可逆プログラムは全てオンラインインタプリタで実行して振る舞いを確かめることが可能である．

DOI： 10.14923/transinfj.2018PDP0021

researchmap

Language：Japanese   Publisher：電子情報通信学会  

任意の可逆プログラミング言語のプログラムで計算できるものが，可逆なR-WHILEプログラムによって計算できることを示す．

DOI： 10.14923/transinfj.2018JDL8008

researchmap

Language：Japanese   Publisher：電子情報通信学会  

ハミルトン曲面流を表す流れの向きを考慮した極大語の表現法，任意の長さの極大語をもれなく重複無く列挙するアルゴリズム，及びステートチャートによる極大語の生成方法の簡潔な表現を示した．本手法で向きを考慮した流れの総数を見積もれる．

DOI： 10.14923/transinfj.2018JDL8002

researchmap

Language：English   Publishing type：Part of collection (book)   Publisher：Springer  

We propose clean reversible simulations of ranking binary trees and unranking as reversible algorithms for reversible computing systems, which are useful for enumerating and randomly generating binary trees. Algorithms for ranking binary trees and their inverses have been studied since the 1970s. Each of these algorithms can be converted into a reversible simulation by saving all data and control information otherwise lost, and each pair of ranking and unranking reversible pro- grams can be combined to realize a clean reversible simulation by using the Bennett method. However, such a clean reversible simulation requires multiple traversal of the given data and/or intermediate data as well as additional storage proportional to the length of the computation. We show that for Knott's ranking and unranking algorithms, additional storage usage can be reduced by using the proper assertions of reversible loops in embedded reversible simulations. We also show a clean reversible simulation that involves only one traversal. The running time and memory usage of the proposed clean reversible simulations are asymptotically equivalent to those of the original programs by Knott with intermediate garbage of constant size. In general, the derivation strategy of efficient reversible programs from irreversible ones has not yet been established, and this study can be seen as one of the case studies. All the reversible programs presented in this paper can be run on an interpreter of the reversible programming language Janus.

DOI： 10.1007/978-3-319-73216-9_11

researchmap

Other Link： https://dblp.uni-trier.de/db/conf/birthday/morita2018.html#OhkuboYK18

Language：Japanese   Publisher：電子情報通信学会  

非比較ソートであるビンソートの可逆シミュレーションを示し，効率的な非可逆ビンソートに対して時間/空間計算量が共に線形で出力ゴミが入力データと漸近的に同じ大きさの置換を表す配列になることを示す．

DOI： 10.14923/transinfj.2017JDL8021

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer Science and Business Media LLC  

DOI： 10.1007/s00354-018-0035-5

researchmap

Other Link： https://dblp.uni-trier.de/db/journals/ngc/ngc36.html#GluckY18

Language：Japanese   Publisher：電子情報通信学会  

メモ化アルゴリズムの可逆版を提案する．本手法により得られるクリーン可逆プログラムは，可逆二進計数器を抽象解釈とする．単射な隣接2項間漸化式で表される任意の数列に対して償却定数時間で定数ゴミ使用量の可逆プログラムを得る方法を示す．

DOI： 10.14923/transinfj.2017JDL8010

researchmap

Authorship：Lead author,　Corresponding author   Language：Japanese  

ハミルトン曲面流に関する極大語の自然な分類が有限個であることを示し，その各分類のもとでの全ての極大語の列挙アルゴリズムの構成法を明らかにした．また，各分類において極大語の総数を求める方法を形式言語理論を応用して示した．

DOI： 10.14923/transinfj.2017JDL8009

researchmap

Authorship：Last author   Language：English   Publishing type：Research paper (scientific journal)  

The paper presents a small reversible language R-CORE, a structured imperative programming language with symbolic tree-structured data (S-expressions). The language is reduced to the core of a reversible language, with a single command for reversibly updating the store, a single reversible control-flow operator, a limited number of variables, and data with a single atom and a single constructor. Despite its extreme simplicity, the language is reversibly universal, which means that it is as powerful as any reversible language can be, while it is linear-time self-interpretable, and it allows reversible programming with dynamic data structures. The four-line program inverter for R-CORE is among the shortest existing program inverters, which demonstrates the conciseness of the language. The translator to R-CORE, which is used to show the formal properties of the language, is clean and modular, and it may serve as a model for related reversible translation problems. The goal is to provide a language that is sufficiently concise for theoretical investigations. Owing to its simplicity, the language may also be used for educational purposes.

DOI： 10.1587/transinf.2016EDP7274

researchmap

Other Link： https://www.wikidata.org/entity/Q62038207

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

A linear-time reversible self-interpreter in an r-Turing complete reversible imperative language is presented. The proposed imperative language has reversible structured control flow operators and symbolic tree-structured data (S-expressions). The latter data structures are dynamically allocated and enable reversible simulation of programs of arbitrary size and space consumption. As self-interpreters are used to show a number of fundamental properties in classic computability and complexity theory, the present study of an efficient reversible self-interpreter is intended as a basis for future work on reversible computability and complexity theory as well as programming language theory for reversible computing. Although the proposed reversible interpreter consumes superlinear space, the restriction of the number of variables in the source language leads to linear-time reversible simulation.

DOI： 10.11309/jssst.33.3_108

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer International Publishing  

A common approach to reversible programming is to reversibly simulate an irreversible program with the desired functionality, which in general puts additional pressure on the computational resources (time, space.) If the same running time is required, ensuring a minimal space overhead is a significant programming challenge.

We introduce criteria for the optimality of reversible simulation: A reversible simulation is faithful if it incurs no asymptotic time overhead and bounds the space overhead (the garbage) by some function g(n), and hygienic if g is (asymptotically) optimal for faithful simulation.

We demonstrate the programming techniques used to develop faithful and hygienic reversible simulations of several well-known comparison sorts, e.g. insertion sort and quicksort, using representations of permutations in both the output and intermediate additional space required.

DOI： 10.1007/978-3-319-26529-2_22

Web of Science

researchmap

Discrete linear transformations are important tools in information processing. Many such transforms are injective and therefore prime candidates for a physically reversible implementation into hardware. We present here reversible integer cosine transformations on n input integers. The resulting reversible circuit is able to perform both the forward transform and the inverse transform. The detailed structure of such a reversible design strongly depends on the odd prime factors of the determinant of the transform: whether those are of the form 2k ± 1 or of the form 2k ± 2l ± 1 or neither of these forms.

Authorship：Last author,　Corresponding author   Language：Japanese   Publishing type：Research paper (scientific journal)  

The extended pass-by-reference parameter passing mechanism of reversible programming language Janus is presented and its reversibility is shown. The states used in the memory model of the existing Janus cannot directly deal with the multiple variables sharing the same memory locations. To remedy this, the state model is replaced with the environment-store model and the semantics of the language is refined. In the extended language, we can pass not only local variables and local array variables to the arguments of procedures but the references of global variables, indexed array variables and such syntactic objects that have the same references. We make the extended Janus reversible by imposing restrictions on the updates of environments and stores. The extended language also preserves several properties of Janus; any sentences and procedure calls can be inversely executed, and the inverse sentences for any sentences exist and can be constructed by simple program transformation. Furthermore, we relax the restrictions on the syntax of reversible assignments. The invalid store updates because of the extension can be efficiently detected during the execution without the necessity of global program analysis. The refined semantics is a simple extension to the existing one in the sense that the programs in the existing syntax have the same meaning under both semantics.

researchmap

Other Link： https://cir.nii.ac.jp/crid/1050564287857987584

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Association for Computing Machinery (ACM)  

Discrete linear transformations are important tools in information processing. Many such transforms are injective and therefore prime candidates for a physically reversible implementation into hardware. We present here reversible integer cosine transformations on n input integers. The resulting reversible circuit is able to perform both the forward transform and the inverse transform. The detailed structure of such a reversible design strongly depends on the odd prime factors of the determinant of the transform: whether those are of the form 2 ^k ± 1 or of the form 2 ^k ± 2 ^l ± 1 or neither of these forms.

DOI： 10.1145/2629532

researchmap

Other Link： https://dblp.uni-trier.de/db/journals/jetc/jetc11.html#VosBGMATRY14

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Springer  

DOI： 10.1007/978-3-642-36315-3

researchmap

Language：Japanese   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE Computer Society  

Reversible simulations can realize any irreversible computation on any r-Turing complete reversible computation model at the expense of additional garbage output. The problem of minimizing the garbage size is an important issue in reversible simulations. We discuss the notion of the minimal garbage size of reversible simulations. Then, we propose a three-stage reversible simulation for minimizing garbage size, the first stage generates specialized irreversible programs, the second translates them into reversible simulations, and the third performs reversible simulation using the generated reversible programs. Two case studies on sorting algorithms suggest that the proposed method generates solutions with minimal garbage size.

DOI： 10.1109/ICNC.2012.73

researchmap

Other Link： https://dblp.uni-trier.de/conf/ic-nc/2012

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)   Publisher：Old City Publishing  

Bennett showed that a clean reversible simulation of injective programs is possible without returning the input of a program as additional output. His method involves two computation and two uncomputation phases. This paper proposes an optimization of Bennett’s simulation that requires only half of the computation and uncomputation steps for a class of injective programs. A practical consequence is that the reversible simulation runs twice as fast as Bennett’s simulation. The proposed method is demonstrated by developing lossless encoders and decoders for run-length encoding and range coding. The range-coding program is further optimized by conserving the model over the text-generation phase. This paper may thus provide a newviewon developing efficient reversible simulations for a certain class of injective functions.

Keywords: Reversible computing, reversible simulation, Janus, Bennett’s method, lossless data encoding, reversibilization

researchmap

Other Link： https://dblp.uni-trier.de/db/journals/mvl/mvl18.html#YokoyamaAG12

Authorship：Lead author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Springer  

We identify concepts of reversibility for a functional language by means of a set of semantic rules with specific properties. These properties include injectivity along with local backward determinism, an important operational property for an efficient reversible language. We define a concise reversible first-order functional language in which access to the backward semantics is provided to the programmer by inverse function calls. Reversibility guarantees that in this language a backward run (inverse interpretation) is as fast as the corresponding forward run itself. By adopting a symmetric first-match policy for case expressions, we can write overlapping patterns in case branches, as is customary in ordinary functional languages, and also in leaf expressions, unlike existing inverse interpreter methods, which enables concise programs. In patterns, the use of a duplication/equality operator also simplifies inverse computation and program inversion. We discuss the advantages of a reversible functional language using example programs, including run-length encoding. Program inversion is seen to be as lightweight as for imperative reversible languages and realized by recursive descent. Finally, we show that the proposed language is r-Turing complete.

DOI： 10.1007/978-3-642-29517-1_2

researchmap

Other Link： https://dblp.uni-trier.de/conf/rc/2011

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)  

The principles for good design of battery-aware voltage scheduling algorithms for both aperiodic and periodic task sets on dynamic voltage scaling (DVS) systems are presented. The proposed algorithms are based on greedy heuristics suggested by several battery characteristics and Lagrange multipliers. To construct the proposed algorithms, we use the battery characteristics in the early stage of scheduling more properly. As a consequence, the proposed algorithms show superior results on synthetic examples of periodic and aperiodic tasks from the task sets which are excerpted from the comparative work, on uni- and multi-processor platforms, respectively. In particular, for some large task sets, the proposed algorithms enable previously unschedulable task sets due to battery exhaustion to be schedulable.

DOI： 10.1587/transinf.E93.D.2737

researchmap

Other Link： https://dblp.uni-trier.de/db/journals/ieicet/ieicet93d.html#YokoyamaZTT10

Publishing type：Research paper (scientific journal)  

DOI： 10.1016/j.entcs.2010.02.007

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE  

Energy-aware real-time multiprocessor scheduling has been studied extensively so far. However, some of the constraints associated with the practical DVS applications have been ignored for simplicity. These constraints include discrete speed, idle power, inefficient speed, and application-specific power characteristics etc. This work targets energy-aware scheduling of periodic real-time tasks on the DVS-equipped multiprocessor systems with practical constraints. An adaptive minimal bound first-fit (AMBFF) algorithm with consideration of these realistic constraints is proposed for both dynamic-priority and fixed-priority multiprocessor scheduling. Simulation results on three commercial processor models show that our algorithm can save significantly more energy than existing algorithms.

DOI： 10.1109/rtcsa.2009.47

researchmap

Authorship：Lead author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE  

The principles for good design of battery-aware voltage scheduling algorithms for both a periodic and periodic task sets on dynamic voltage scaling (DVS) systems are presented. The proposed algorithms are based on greedy heuristics suggested by several battery characteristics and Lagrange multipliers. To construct the proposed algorithms,we use the battery characteristics in the early stage of scheduling more properly. As a consequence, the proposed algorithms show superior results on synthetic examples of periodic and a periodic tasks from the task sets which are excerpted from the comparative work, on uniprocessor platforms. Especially, for some large task sets,the proposed algorithms enable previously unschedulable task sets due to battery exhaustion to be schedulable.

DOI： 10.1109/icess.2009.19

researchmap

Language：Japanese  

CiNii Books

researchmap

Other Link： http://id.nii.ac.jp/1001/00060628/

Authorship：Lead author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE  

The energy efficiency at the algorithmic level on DVS systems and its analysis and optimization methods are presented. Given a problem the most energy efficient algorithm is not uniquely determined but dependend on multiple factors, including intratask dynamic voltage scaling (IntraDVS) policies, the size of intermediate data structure, and the size of inputs. We show that at the algorithmic level principles behind energy optimization and performance optimization are not identical. We propose a metric for evaluating optimal energy efficiency of static voltage scaling (SVS) and a few new effective IntraDVS policies employing data flow information. Experimental results on sorting algorithms show the existence of several tradeoffs in terms of energy consumption. Transforming algorithms by employing problem specific knowledge and data flow information successfully improves their energy efficiency.

DOI： 10.1109/ASPDAC.2009.4796566

researchmap

Other Link： https://dblp.uni-trier.de/conf/aspdac/2009

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE  

A generalized dynamic energy performance scaling (DEPS) framework is proposed for exploring application-specific energy-saving potential in multiprocessor systems. This software-centric framework takes advantage of possible power control mechanisms to trade off performance for energy savings. Three existing technologies, i.e., dynamic hardware resource configuration (DHRC), dynamic voltage frequency scaling (DVFS), and dynamic power management (DPM), have been employed in this framework to achieve the maximal energy savings. The problem of determining the optimal task allocation and DEPS configurations is formulated as an integer linear programming (ILP) problem. Several practical issues such as how to reduce measurement and computation time and how to reduce the configuration overhead are also addressed. The effectiveness of DEPS is validated through a case study.

DOI： 10.1109/socdc.2008.4815570

researchmap

Authorship：Lead author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Springer  

Many irreversible computation models have reversible counterparts, but these are poorly understood at present. We introduce reversible flowcharts with an assertion operator and show that any reversible flowchart can be simulated by a structured reversible flowchart using only three control flow operators. Reversible flowcharts are r- Turing-complete, meaning that they can simuluate reversible Turing machines without garbage data. We also demonstrate the injectivization of classical flowcharts into reversible flowcharts. The reversible flowchart computation model provides a theoretical justification for low-level machine code for reversible microprocessors as well as high-level block-structured reversible languages. We give examples for both such languages and illustrate them with a lossless encoder for permutations given by Dijkstra.

DOI： 10.1007/978-3-540-70583-3_22

researchmap

Other Link： https://dblp.uni-trier.de/conf/icalp/2008-2

Authorship：Lead author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：ACM  

The principles of reversible programming languages are explicated and illustrated with reference to the design of a high-level imperative language, Janus. The fundamental properties for such languages include backward as well as forward determinism and reversible updates of data. The unique design features of the language include explicit post-condition assertions, direct access to an inverse semantics and the possibility of clean ({\ie}, garbage-free) computation of injective functions. We suggest the clean simulation of reversible Turing machines as a criterion for computing strength of reversible languages, and demonstrate this for Janus. We show the practicality of the language by implementation of a reversible fast Fourier transform. Our results indicate that the reversible programming paradigm has fundamental properties that are relevant to many different areas of computer science.

DOI： 10.1145/1366230.1366239

researchmap

Other Link： https://dblp.uni-trier.de/conf/cf/2008

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer Berlin Heidelberg  

A reversible abstract machine architecture and its reversible machine code are presented and formalized. For machine code to be reversible, both the underlying control logic and each instruction must be reversible. A general class of machine instruction sets was proven to be reversible, building on our concept of reversible updates. The presentation is abstract and can serve as a guideline for a family of reversible processor designs. By example, we illustrate programming principles for the abstract machine architecture formalized in this paper.

DOI： 10.1007/978-3-540-74510-5_9

Web of Science

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)  

A reversible programming language supports deterministic forward and backward computation. We formalize the programming language Janus and prove its reversibility. We provide a program inverter for the language and implement a self-interpreter that achieves deterministic forward and backward interpretation of Janus programs without using a computation history. As the self-interpreter is implemented in a reversible language, it is invertible using local program inversion. Many physical phenomena are reversible and we demonstrate the power of Janus by implementing a reversible program for discrete simulation of the Schrödinger wave equation that can be inverted as well as run forward and backward. Copyright © 2007 ACM.

DOI： 10.1145/1244381.1244404

Scopus

researchmap

Authorship：Lead author   Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer Berlin Heidelberg  

The world of program optimization and transformation takes on a new fascination when viewed through the lens of program calculation. Unlike the traditional fold/unfold approach to program transformation on arbitrary programs, the calculational approach imposes restrictions on program structures, resulting in some suitable calculational forms such as homomorphisms and mutumorphisms that enjoy a collection of generic algebraic laws for program manipulation. In this tutorial, we will explain the basic idea of program calculation, demonstrate that many program optimizations and transformations, such as the optimization technique known as loop fusion and the parallelization transformation, can be concisely reformalized in calculational form, and show that program transformation in calculational forms is of higher modularity and more suitable for efficient implementation.

DOI： 10.1007/11877028_5

Web of Science

researchmap

Authorship：Lead author   Language：Japanese  

Second-order patterns and second-order matching play an important role in program transformation, but the second-order matching algorithm is known to be NP-hard and real efficient, implementation is out of Question. To resolve this problem, we introduced a class of deterministic second-order patterns, and proposed an efficient matching algorithm. In this paper, we further extend this class to cove more deterministic second-order patterns, discuss both sufficient and necessary conditions for a second-order pattern to be deterministic, and demonstrate its usefulness in program transformation.

DOI： 10.11309/jssst.21.403

CiNii Books

researchmap

Other Link： https://projects.repo.nii.ac.jp/?action=repository_uri&item_id=288606

Language：English   Publishing type：Part of collection (book)   Publisher：Springer Berlin Heidelberg  

Higher-order patterns, together with higher-order matching, enable concise specification of program transformation, and have been implemented in several program transformation systems. However,higher-order matching in general is nondeterministic, and the matching algorithm is so expensive that even second-order matching is NP-complete. It is orthodox to impose constraint on the form of patterns to obtain the desirable matches satisfying certain properties such as decidability and finiteness. In the context of unification, Miller’s higher-order patterns have a single most general unifier. We relax the restrictions in his patterns without changing determinism within the context of matching instead of unification. As a consequence, the new class of patterns covers a wide class of useful patterns for program transformation. The time-complexity of the matching algorithm is linear for the size of a term for a fixed pattern.

DOI： 10.1007/978-3-540-25938-1_12

researchmap

Publisher：Springer  

Higher-order patterns, together with higher-order matching, enable concise specification of program transformation, and have been implemented in several program transformation systems. However,higher-order matching in general is nondeterministic, and the matching algorithm is so expensive that even second-order matching is NP-complete. It is orthodox to impose constraint on the form of patterns to obtain the desirable matches satisfying certain properties such as decidability and finiteness. In the context of unification, Miller’s higher-order patterns have a single most general unifier. We relax the restrictions in his patterns without changing determinism within the context of matching instead of unification. As a consequence, the new class of patterns covers a wide class of useful patterns for program transformation. The time-complexity of the matching algorithm is linear for the size of a term for a fixed pattern.

Authorship：Lead author   Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Elsevier BV  

Second-order patterns, together with second-order matching, enable concise specification of program transformation, and have been implemented in several program transformation systems. However, second-order matching in general is nondeterministic, and the matching algorithm is so expensive that the matching is NP-complete. It is orthodox to impose constraints on the form of higher-order patterns so as to obtain the desirable matches satisfying certain properties such as decidability and finiteness. In the context of unification, Miller's higher-order patterns have a single most-general unifier. In this paper, we relax the restriction of his patterns without changing determinism in the context of matching instead of unification. As a consequence, our deterministic second-order patterns cover a wide class of useful patterns for program transformation. The time-complexity of our deterministic matching algorithm is linear in the size of a term for a fixed pattern.

DOI： 10.1016/j.ipl.2003.12.008

researchmap

Publisher：Japan Society for Software Science and Technology  

We present an embedded domain specific language for specifyingprogram transformations. The language is implemented as a monadic combinatorlibrary in Haskell. The transformations are done at compile time using themechanism of Template Haskell. The library provides a modular way to structureabstract and intuitive transformation strategies by higher-order matching andmonadic programming.

DOI： 10.11309/jssstconference.21.0.19.0

researchmap

Language：Japanese  

2階パターンと2階マッチングを用いると高度なプログラム変換を記述することができることが知られている．しかし2階マッチングはNP完全であるため効率がよい実装が望めず，また非決定論的であるため，セマンティクスが複雑であるという問題点がある．われわれは，2階パターンの形を制限することで，どのような項とも高々1つのマッチしか得られないようなパターンのクラスを決定論的2階パターンとして定め，またこのマッチを得るための効率の良いアルゴリズムを開発した．本論文では，このような決定論的2階パターンのクラスを拡張し，また決定論的線形2階パターンであるための必要十分条件を与える．このパターンのクラスを用いる幅広い応用が可能であると考えられる．

DOI： 10.11309/jssstconference.2003.0.32.0

researchmap

Language：Japanese   Publishing type：Research paper (bulletin of university, research institution)  

researchmap

Authorship：Lead author   Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Information Processing Society of Japan (IPSJ)  

To relax the tension between clarity and efficiency in programming, we have proposed a theoretical framework called calculation carrying program, which accompanies straightforward specification with calculation specifying the intention (strategy) in a highly abstract way. In this paper, we give its first implementation, showing the system which not only automatically derives efficient programs from initial inefficient specification, but also interactively helps programmers to debug derivation steps. Furthermore, to show its power, we demonstrate how to use our system to generate efficient programs for solving maximum marking problems.

CiNii Books

researchmap

Publisher：一般社団法人情報処理学会  

プログラミング言語の選択による情報通信端末の消費エネルギーの変化を定量的に評価する試みについて報告する．本稿では，アプリケーションの実装プログラミング言語ごとの消費電力への影響を，実情報端末において電力計で実測することにより確かめた．その結果，インタープリタ言語では消費電力の大きな揺れが観測されたが，コンパイル言語と同様の平均消費電力を示し，電池に与える影響の変化は限られた．われわれが実験を行った範囲では，プログラミング言語およびアプリケーションを変化させたときの1秒ごとの平均消費電力の変化は高々20%未満であり，その影響は軽微であることが確かめられた．われわれの知る範囲では，プログラミング言語ごとに消費電力/消費エネルギーの比較を行った報告は限られており，本研究で得られた基礎データは低消費エネルギーアルゴリズムや低消費エネルギープログラミングの研究を行う上での参考データとして貴重である．The trial of finding the programming language effects of energy consumption on a battery-powered system is presented. By means of a digital power meter, we measured the energy consumption of an information device on which different applications implemented in various programming languages run. While the power consumption fluctuated substantially when an interpretive language run on the device, the average power consumption of an interpretive language was not much different from that of a compiler language. The experimental results showed that the effects of what programming languages to use were limited; The change of the power consumption was up to approximately 20%. To the best of our knowledge the report on power/energy consumption of each programming language implementation has been limited and the result data is useful for studying the theoretical model of energy consumption and exploring energy efficient algorithms and programming.

本稿では，ハードウェア独立な Dalvik バイトコードトレースから得られる情報を活用し，Android プラットフォームにおける CPU 負荷量の解析を行う．各 Dalvik バイトコードの CPU 負荷量を正確に精度良く解析するため，マイクロベンチマークの生成方法および実施方法を提示する．マイクロベンチマークの CPU 負荷量は，バイトコードの種類により最大 67 倍，引数のレジスタ値により最大 10 倍の差が存在した．したがって，アプリケーションの CPU 負荷量の正確なモデル化を行うためには，バイトコードの発行数のみならず，種類・引数を考慮する必要があることが明らかになった．以上により確立された解析手法を用いて，アプリケーション開発者に改善を提案するケーススタディを行った．実際に CPU 負荷量の削減方法を示唆できたことから，本解析手法の有効性が示された．We present a CPU load analysis method on Android platform by using hardware-independent trace information of Dalvik bytecodes. For the purpose of analysis, methods for generating and executing micro-benchmarks which issue the sequence of each Dalvik bytecode are introduced. The experimental results showed that the CPU load of micro-benchmarks was largely affected by the types arguments of bytecodes. Specifically, the variation of CPU load was up to 67 times over the types and 10 times over the arguments of given bytecodes. Therefore, not only the number of issued bytecode but also the types of bytecode and given arguments should be considered to construct an accurate CPU load model. Through a case study, the effectiveness of our approach for reducing CPU load has been validated.

情報通信端末において，データ受信と可逆データ解凍を逐次的に行うよりも，パイプライン化した方が消費エネルギーの最適化が実現されるケースが存在することが明らかになった．パイプライン化によって，マルチパスの圧縮コマンド bunzip2 では消費エネルギーは悪化してしまったが，ストリーム処理が可能な LZ(Lempel-Ziv) 系のアルゴリズムの場合，顕著なエネルギー最適化が達成された．データ受信が安定的に行える環境下で，情報通信端末の消費電力を電力測定器によって計測したところ，逐次処理と比較してパイプライン処理は最大 22.8% の消費エネルギー削減が達成された．It has been shown that there is a certain case in which the pipeline processing is more energy efficient than the sequential processing. Because of pipelining processes, LZ (Lempel-Ziv) family algorithms achieved significant energy savings while multi-path compression command bunzip2 suffered energy degradation. The experimentation has been performed on a commercial data transmission device connected to a digital power meter under the stable data transmission. A pipelining processing outperformed a sequential processing by 22.8% in terms of energy consumption.

Publisher：IEEE  

We propose a novel system level power estimation method for wireless communication devices. The method estimates the power consumption of a processor and external devices by only using OS level profile information (i.e., the system call information), and is applicable to both off-line and online power optimizations. Evaluations on a commercial wireless communication device showed that the method achieves an estimation error of less than 10%.

Publisher：電子通信情報学会  

通信端末のシステムレベルの消費電力予測を行う手法を提案する．本手法はプロセッサと周辺デバイスの消費電力を OS レベルのプロファイル情報のみを用いて予測するため，オフラインとオンラインの両者に適応可能である．商用の通信端末において通信を伴うアプリケーションを実行した評価では，本手法による予測消費電力の実測値に対するフィッティング誤差は 10% 以内に収まった．We propose a novel system level power estimation method for wireless communication devices. The method estimates the power consumption of processors and external devices by only using OS level profile information provided by system calls. The proposed method is applicable to on-line power estimation as well as off-line power estimation. Evaluations on a commercial wireless communication device showed that the method achieved an estimation error of less than 10 %.

Publisher：情報処理学会  

Publisher：情報処理学会  

Publisher：ACM Press  

Publisher：日本ソフトウェア科学会  

Publisher：情報処理学会  

消費エネルギー最適化や量子コンピュータの実現に用いられる可逆計算法が研究されている．可逆計算法は計算の全過程の単射化により実現される．ハフマン符号化法と漸近的に同じ時間及び空間計算量でゴミ出力量Θ(n lg n) の可逆アルゴリズムが報告されている．ゴミ出力は，計算を単射化するために出力される情報であり，問題の本質的な解決に関わらない．本稿では，整列された頻度表を入力とするハフマン木構築法を基礎とする，ゴミ出力がなく1パスの可逆ハフマン木構築法を提案する．

線形時間かつ入力以外の空間使用量のオーバーヘッドが定数に収まるような木構造に対する可逆優先探索法を提案した。

During the past decade reversible programming languages have been formalized using various established semantics frameworks. Common to these semantics is that they are weak at specifying the distinct properties of reversible languages at the metalevel, even including the central question whether the defined language is reversible. In this paper, we build upon a metalanguage foundation for reversible languages based on the category of sets and partial injective functions. We exemplify our approach by a step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. This leads to a formalization of the semantics in which the reversibility of the language and its inverse semantics are immediate, as well as the inversion of programs written in the language. We discuss further applications and directions for reversible semantics.

理工系学部の学生に求められる理系文章作成能力の向上を目的として2017年度に取り組んだピアフィードバックの多様化に加えて，実習科目における課題解決の検討，レポート作成，相互評価，自己評価，次回に向けての改善の手順をPDCAサイクルとして構築する試みに取り組んだ．他者のレポートを閲覧・評価することで評価者としての視点を得ることができ，その後に他者からの評価を確認して自分のレポートを見直し自己評価することでレポートの問題点や改善点に気付き，次回のレポート作成に繋げることができる環境を整えた．

Minecraftは，立方体のマス目に区切られた3次元空間にブロックを設置したり破壊したりしてものづくりを楽しむゲームである．本稿では，Minecraftの計算モデルの計算能力を調べる．具体的には，Minecraftの世界をセル・オートマトンとして抽象化し，論理ゲートを模倣するブロックの組合せをいくつか示し，論理ゲートの集合が完全系になる条件を述べる．また，計算万能であることが知られている機械を構成するための条件とその構成法を示す．

円板上の非圧縮流は，血管などのパイプ流や医療機器における軸対称流の近似となっており，医学分野において重要な解析対象である．最外境界部をもつ単連結領域上の非圧縮流の反転をトポロジーにのみ着目することで解析を行う．トポロジーにのみ着目することで少量の計算資源でそのダイナミクスの解析が可能である一方で，流体の特性をどの程度表せるかは未知数である．本研究では，形式言語理論で広く使われている木文法の拡張を用いて，木表現で流線図のトポロジーを表現し，木表現の列で流線図の時間発展を表現する．本アプローチによって，ランダム外力駆動の2次元反転流の数値流体計算における反転現象をどの程度解析できるかを評価する．

理工系学部の学生に求められる理系文書作成能力を向上させ，その技術を定着させるための手法として実習科目におけるレポート作成，成果発表，ピアレビュー等のピアフィードバック(PF)の多様化に取り組んだ．PFの多様化には資料提供やレポート提出に使用してきたLMSを用いることで学生，教員の負担を増すことなく効率的な導入を実現した．アンケート調査やピアレビューの結果から本実践の有効性を確認した．

可逆プログラミング言語R-WHILEの計算モデルは，万能可逆チューリング機械と同じ計算能力があるとされている．しかし，筆者の知る限りにおいて，その具体的な証明についてはこれまで報告が無かった．本稿では任意の可逆チューリング機械を，意味が同じR-WHILEプログラムに変換できることを示す．このことにより，可逆万能チューリング機械のR-WHILEプログラムが構成できることを示す．

We propose clean reversible simulations of ranking binary trees and unranking as reversible algorithms for reversible computing systems, which are useful for enumerating and randomly generating binary trees. Algorithms for ranking binary trees and their inverses have been studied since the 1970s. Each of them can be made to be a reversible simulation by saving all the data and control information otherwise lost, and each pair of ranking and unranking reversible programs can be combined to realize a clean reversible simulation. However, such a clean reversible simulation requires multiple traversal of the given data and/or intermediate data as well as additional storage proportional to the length of the computation. We show that for Knott's ranking and unranking algorithms the additional storage usage can be reduced by using the proper assertions of reversible loops in embedded reversible simulations. We also show a clean reversible simulation that involves only one traversal. The running time and memory usage of the proposed clean reversible simulations are asymptotically equivalent to those of the original programs by Knott. All the reversible programs presented in this paper can be run on an interpreter of the reversible programming language Janus.

可逆計算システムで用いる可逆アルゴリズムのひとつとして，二分木の列挙やランダム生成に有用な二分木のランク・アンランク計算のクリーン可逆シミュレーションを提案する．二分木のランク計算やその逆計算を行う非可逆アルゴリズムは1970年代から研究が行われてきており，これらの成果を用いてランク計算の関数とその逆関数のそれぞれの可逆シミュレーションを組み合わせてクリーン可逆シミュレーションを行うことはできる．しかし，こうした可逆シミュレーションでは，複数回のパスおよびに実行時間に比例した大きさのメモリが必要である．これに対してわれわれの可逆シミュレーションは，1パスで，漸近的な実行時間とメモリ使用量が元のアルゴリズムと同じである．本稿中の可逆プログラムは，可逆言語Janusの処理系で動作を確認できる．

Flowcharts are a fundamental tool used pervasively in computer science. In this talk, we survey the fundamental properties of reversible flowcharts, which are classical flowcharts with restrictions on join points and atomic step operators. Reversible flowcharts are as expressive as any reversible computation models such as reversible Turing machines and are able to simulate any irreversible computation. The theoretical basis of structured programming in high-level reversible languages is provided by a reversible version of the Structured Program Theorem. We illustrate the design of high-level and low-level reversible programming languages and their translators, based on the reversible flowchart model. We highlight their features by demonstrating a reversible version of Dijkstra's permutation-to-code algorithm.

This paper explores a novel combination of language features in re- versible programming languages. The two imperative languages that we introduce have reversible structured control flow operators and symbolic tree-structured data (S-expressions). The latter allows to model many familiar data structures in an easy way, which is more difficult in existing reversible imperative languages, which so far only provide integers, stacks and arrays as data types. Most importantly, it is shown for the first time in a most expressive reversible imperative language that tree-structured data enable efficient self-interpretation in the sense of Jones. We prove that the languages are r-Turing complete (most expressive), i.e. they are computationally as powerful as any reversible language can get, and cleanly reversible, i.e. programs can run backward without first tracing a forward computation. The languages presented here are two new versatile instances of our structured reversible flowchart paradigm, and intended to serve as a basis for future studies of reversible programming languages, transformation and algorithms.

本稿では，可逆プログラミング言語Janus の引数渡し機構を拡張して，その拡張言語が可逆であることを示す．参照渡しのモデル化には，同一の参照をもつかもしれない複数の変数名が同じ記憶場所を指せるメモリモデルが必要である．これは既存のJanus で用いられていた状態モデルでは直接には扱うことができない．この問題を解決するために，われわれは，環境・記憶域モデルを導入して意味論を改良した．この結果，プロシージャの実引数には，局所変数や局所配列変数だけでなく大域変数や添字付き配列変数の参照，および同一の参照をもつ複数の構文対象も渡せるようになった．拡張言語が可逆であることの保証には，環境と記憶域の更新が可逆であることの保証が必要がある．これらの更新は，制限された可逆操作のみ用いて実現することで，可逆であることを保証する．われわれは，拡張言語が他にも既存のJanusの良い性質を保っていることを示す．すなわち，任意の文やプロシージャ呼び出しの逆実行ができること，および任意の文に対して逆文が存在してそれを求めるプログラム逆変換器が構成できることを示す．さらに，われわれは，プログラミング言語を可逆にするために課されていた代入の構文上の制限を緩和する．このことが原因で起こる記憶域の不正な更新は，大域のプログラム解析をせずとも，効率的に検知することができる．われわれが新たに定義した意味論は，既存の構文では同一の意味が与えられるという点で，既存言語からの単純な拡張となっている．

本論文では文献[1] におけるゴミ情報の生成・マージの手法を応用し，より一般性の高い手法を提案する．文献[1] では，ゴミ情報量が最適なリストの可逆分割アルゴリズムを提案している．ここではさらに提案したアルゴリズムを利用してクイックソートを生成し，分割の際のゴミ情報量が最適であること，再帰呼び出しの際にゴミ情報の最適な伝播が実現できていることの2 点を示している．しかし，この手法はクイックソートに特有のサブプロシージャに対して最適なゴミ情報の生成を保証することにより実現されており，この手法をそのまま他のアルゴリズムに応用することが難しい．そこで，本研究ではアルゴリズムのより小さな構成要素に最適なゴミ情報を生成させ，それらの最適性を保ったままより大きな構成要素へとマージを行う手法を提案し，既存の手法の応用性を高める．なお，ここではゴミ情報とは非可逆アルゴリズムを可逆化する際に記録する必要があり，可逆化する前の非可逆アルゴリズムにおいては記録する必要のない情報を表す．

計算過程が可逆とは，任意の状態でその直前と直後の状態が存在すればそれぞれ必ず一意に定まることをいう．可逆プログラミング言語とは，そのプログラムの実行過程が必ず可逆になるような言語設計がなされているプログラミング言語であり，可逆論理回路の設計[1] やプログラミング言語理論の研究対象[2] として使われている．そうした言語のひとつであるJanusでは，構文規則や意味規則における制限によって可逆性を実現しており，その結果，可逆プログラムでのみ可能な逆実行をするための機構を備えている．現在のJanus[3] は，引数機構が未整備のために可読性や簡潔性が欠如していると考えられる点がある．原因のひとつとして，状態モデルによって識別子のみを渡すことのできる引数渡し機構が用いられていることが挙げられる．このため，識別子以外の式の評価値や参照を渡すことが困難であった．そこで，我々は左辺値を意味領域に含むことのできる環境・記憶域モデルを採用し，可逆性をもつ値渡しと参照渡しの機構を実現する．Janus では，複合代入演算の左辺に出現した識別子が右辺に出現してはならないという制約があるが，この拡張により，プログラム全域のプログラム解析をしなくてもその複合代入演算文の実行時にその文の情報だけからこの制約の確認ができるようになる．また，引数を伴うプロシージャ呼出しが，より読みやすく簡潔に記述できるようになる．本稿では，引数渡し機構を拡張して表現力の増したJanus が可逆性をもつことの説明の概略を示す．