Search

Malbolgeは最も難解なプログラミング言語として知られている.近年,Malbolgeのための中間言語として低級アセンブリ言語が設計され,そのプログラムからMalbolgeプログラムを生成する低級アセンブラが構築された.しかし,低級アセンブリ言語を用いてプログラミングを行う際,メモリ不足という事態が度々発生していた.例えば,低級アセンブラを利用した数値のインクリメントを行うMalbolgeプログラム生成は,それだけでメモリ空間59049ワードのうち10分の1も消費する.本稿では,この問題の解決のためにMalbolgeのワード長を10tritsから20tritsに拡大し,3^ワードのメモリを持つMalbolge20を提案する.Malbolge20では,3^ワードという膨大の量のメモリを扱うため,メモリの管理方法を大きく変更する.また,Malbolgeを対象としている低級アセンブラ及びMalbolgeデバッガをMalbolge20に対応させ,Malbolge20のプログラミング環境を整備する., Malbolge is known to be one of the most esoteric programming languages. Recently a low-level assembly language (LA-language) has been designed as an intermediate language for Malbolge programming and a low-level assembler (LA-assembler) has been constructed that generates a Malbolge program from a low-level assembly program.We have a problem that the LA-assembler often fails because the size of generated Malbolge program exceeds the limit. For example, the size of an incrementation program produced by the LA-assembler is one-tenth of the allowed size. In order to solve this problem, this paper proposes a variant of Malbolge, named Malbolge20, whose word length is extended to 20trits from the original size 10trits.We enhanced the memory management by introducing cash mechanism. We modify the existing LA-assembler and debugger of Malbolge for Malbolge20 as a programming environment of Malbolge20., IEICE Technical Report;SS2013-25,IEICE Technical Report;KBSE2013-25

与えられた有理数上の線形制約を充足する割り当てを求める手法として単体法がある.また,有理数解を求める手法と,ゴモリーカットをはじめとする切除平面法を組み合わせることで整数解を求められることが知られている.しかし,単体法を適用した後,必ずしもゴモリーカットが適用可能であるとは限らない.本稿では,ゴモリーカットの合成に必要な単体法における不変条件を示し,単体法とゴモリーカットを合成した手続きを示す.また,ゴモリーカットで追加する制約について,より単純な実装を行うための制約の形式を述べる.これらに基づいて,上記2つの手法を合成したソルバを実装し,評価する., The simplex method is one of the methods to derive rational assignments from linear constraints on ra- tiolals. It is known that we can derive integer assignments by composing the methods to derive rational assignments and cutting plane methods such as Gomory cut. However, Gomory cut is not applicable to all formulas resulted from the simplex method. In this paper, we first reveal an invariant property of the internal state of the simplex method in order to compose the simplex method and Gomory cut. Then we show a procedure of the composition of these methods, and we propose the form of constraints that are added into the initial constraint by applying Gomory cut so as to implement more simply. Finally, we compare our implemented solver with other solvers, IEICE Technical Report;MSS2012-78,IEICE Technical Report;SS2012-78

制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に、制約付き項書換え系のR完全性の判定手続きが必要である。また、対象の制約付き項書換え系が十分完全性を持つ場合に、定理自動証明中の推論規則の適用条件を緩和することができる。これらの性質は、制約付き項のインスタンスの集合に関する積集合空問題に帰着できる。本論文では、制約付き項のインスタンスを受理する制約付き木オートマトンの構成法を提案する。さらに、制約付き木オートマトン中でどの入力基底項も到達することのない状態を削除する手法を提案することで、R完全性や十分完全性の判定の精度向上と効率化をめざす。, A theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for R-completeness of constrained term rewriting systems. In addition, sufficient completeness of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties of constrained term rewriting systems can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms. In this paper, we propose a method to construct constrained tree automata recognizing ground instances of constrained terms. We also propose a method to remove states from a constrained tree automaton, to which no ground term transitions, thus improving the accuracy for the judgements of R-completeness and sufficient completeness., IEICE Technical Report;SS2012-47

Malbolgeは最も難解なプログラミング言語として知られている。低級アセンブリ言語の開発によりMalbolgeのループプログラムの作成が可能になったものの、低級アセンブリプログラムでは変数を引数とする命令はその変数宣言の直前に記述しなければならず実行制御が必要不可欠なことと、制御命令には無条件ジャンプとアクセスの度にジャンプとスルーが入れ替わるフリップフロップジャンプしか存在しないことから、低級アセンブリ言語でのプログラミングにも困難が伴う。これまで制御命令の配置設計は手作業により行われており、実行トレーサを利用しているものの、非常に困難であった。本稿では、Malbolgeの低級アセンブリプログラミングにおける制御命令の配置設計にSATソルバを利用した手法を提案することで、この問題の解決を試みる。そのため、制御命令の配置問題を定式化し、その問題のSATエンコーディングを提案する。実験により、提案手法を利用した制御命令配置設計ツールの性能を評価する。, Malbolge is known as one of the most esoteric programming languages. Although it became possible to write programs in Malbolge due to the development of the low-level assembly language, we still have a problem that the programming in the low-level assembly language is difficult. This is because for each variable, instructions that take the variable in their arguments are allowed to be placed just above of the variable in the low-level assembly programs, and control-instructions in the low-level assembly language are only unconditional jumps and flip-flop jumps, where the latter alternate jump and no-operations. So far we have to design control structures, i.e., layout of control-instructions, by hand, which is very difficult even if we have an execution tracer for low-level assembly programs. In this paper, to solve this problem, we propose a method to design layout of control-instructions of the low-level assembly language efficiently by using state-of-art SAT solvers. We define a control-instruction layout problem, and propose a SAT encoding for this problem. We also evaluate the performance of control-instruction layout tools based on our method., IEICE Technical Report;SS2012-50

Malbolgeは最も難解なプログラミング言語として知られている.低級アセンブリ言語の開発によりMalbolgeのループプログラムの作成が可能になったものの,低級アセンブリ言語には通常のプログラミング言語が持つような演算命令がなく,Malbolge特有の演算を行う命令のみであるため,低級アセンブリ言語でのプログラミングにも困難が伴う.低級アセンブリプログラミングにおいては,目的のプログラムに必要な二引数三値関数を実現するMalbolge特有の演算命令列の発見が求められる.しかしこれまで,そのような命令列を発見するための手法は網羅的な探索に限られており,低級アセンブリプログラミング上の制限となっていた.本稿では,二引数三値関数を実現するMalbolge命令列の発見にSATソルバを利用した手法を提案することで,この問題の解決を試みる.そのため,二引数三値関数を実現するMalbolge命令列を発見する問題を定式化し,その問題のSATエンコーディングを提案する.実験により,既存手法より高速に,かつ,長い命令列が発見できることが分かった., Malbolge is known to be one of the most esoteric programming languages. Although it becomes possible to write programs in Malbolge language due to the development of the low-level assembly language, the programming in the low-level assembly language is difficult. This is because the arithmetic instructions of the low-level assembly language are not those of ordinary programming languages, but the same as the ones of Malbolge. To construct a program in low-level assembly language, it is necessary to find instruction sequences of Malbolge that implement binary trit-wise functions. For finding such instruction sequences, however, an inefficient exhaustive search is the only known method, which is one of limitations in developing programs in the low-level assembly language. In this paper, to solve this problem, we propose a method to find instruction sequences of Malbolge that implement binary trit-wise functions, which is more efficient due to the use of state-of-art SAT solvers. We formalize a problem that finds an instruction sequence of Malbolge that implements a given binary trit-wise function, and propose a SAT encoding for this problem. Experiments shows that our method is able to find instruction sequences faster than the existing method and hence essentially longer ones., IEICE Technical Report;SS2012-37

The inversion method proposed by Gliick and Kawabe uses grammar programs as intermediate results, that comprise sequences of operations (data generation, matching, etc.). The semantics of the grammar programs is denned as a stack machine where data terms are stored in the stack. The matching operation for a constructor symbol pops up the topmost term of the stack and pushes its direct subterms to the stack if the topmost term is rooted by the constructor. This paper strengthens the matching operation by augmenting a parameter that specifies what position the matching operation can look into from the top of the stack. This extension is sometimes effective to avoid the failure execution of the determinization method based on LR parsing described in the latter half of the inversion method., IEICE Technical Report;SS2012-27,IEICE Technical Report;KBSE2012-29

Malbolgeは最も難解なプログラミング言語として知られている.高級アセンブリ言語の開発によりMalbolgeプログラムの作成が可能になっているものの,プログラム中で使用できる変数の値の最大値が固定されておりゲーデルコーディングが不可能であるため,配列機能がないのは記述力不足であった.本論文ではこの問題を解決するため,高級アセンブラに用いられている実現手法を整理し,これに配列機能のための命令である領域確保命令と間接参照命令を追加する方法を提案する., Malbolge is known to be one of the most esoteric programming languages. Although it is possible to write programs in Malbolge by the development of a high-level assembly language, lack of facility to manage individual data in a group of data like an array in language causes problem because Godel-coding is impossible in a program due to bounded values in variables. In this paper, in order to solve this problem, we show implementation issues used in the assembler in well-organized manner and propose a method for implementing a memory allocation instruction and an indirect reference instruction for array facility into the assembler., IEICE Technical Report;SS2012-8

書換え帰納法は,与えられた等式が帰納的定理であるかどうかを推論規則を用いた導出により判定する原理であり,項書換え系上で提案され様々な拡張がなされてきた.本論文では、書換え帰納法を単純型付き項書換え系上へ拡張することにより,高階関数を含む等式に対しての書換え帰納法による帰納的定理の自動証明法を実現する.また,書換え帰納法の推論規則が満たすべき性質を定式化し,この定式化に基づいて各推論規則を適切に設計する., Rewriting induction is a principle of proving inductive theorems by means of derivations obtained by applying inference rules. The principle was first proposed on term rewriting systems, and was extended variously. In this paper, we extend the rewriting induction to simply-typed term rewriting systems, implementing an automated inductive theorem proving for higher-order equations. In order to design inference rules suitably, we also formulize properties which inference rules should satisfy., IEICE Technical Report;MSS2011-63,IEICE Technical Report;SS2011-48

高階書換え系(HRS)での強力な停止性証明手法として静的依存対法が知られている.この手法は静的な再帰構造解析を行い,静的再帰成分と呼ばれる解析結果の非循環性を示すことで証明を行う.この際に,非循環性を示すために考慮すべき規則を絞り込む実効規則と呼ばれる概念が提案されているが,高階変数を介した依存解析が困難であるため規則を絞り込めない場合がある.一方,一階の書換え系ではより考慮すべき規則を絞り込む,引数切り落とし関数の下での実効規則が提案されている.本研究ではこの成果をHRS上に拡張する.高階変数から始まる部分項を切り落とすことにより高階変数を介した依存解析を考慮せずにすむため,証明力を飛躍的に向上させることができる., The static dependency pair method is known as a powerful method for proving termination of higher-order rewrite systems (HRSs). The method proves the termination by showing the non-loopingness of all the static recursion components respectively that are obtained by some static recursion analysis. The notion of usable rules has been proposed to reduce the number of rewrite rules considered in showing the non-loogingness. However, we sometimes fail to reduce rewrite rules by reason of some dependency analysis through higher-order variables. In first-order term rewriting, the notion of usable rules under argument filterings has also been proposed, which can reduce more rewrite rules in general. In this paper, we extend the notion to HRSs. By filtering subterms rooted by a higher-order variable, we can avoid analyzing dependencies through higher-order variables., IEICE Technical Report;MSS2011-64,IEICE Technical Report;SS2011-49

等式集合の語問題は,2つの項を与えたときに,等式集合のもとで2つの項が等しいかどうかを決定する問題である.本論文では線形,シャロー,変数非消去かつ非崩壊な規則からなる等式集合の語問題が,等式集合と2つの項から定められる基底項を各等式に代入する変換を用いることにより,変数を持たない等式集合の語問題へ帰着可能であることを示す.この結果より,変数を持たない等式集合の語問題判定アルゴリズムを用いて,目的の語問題を解くことが可能となる., The word problem of an equation set is to decide, given two terms, whether the two terms are equivalent under the equations. In this paper, we show that word problems of linear, shallow, non-erasing and non-collapsing equation sets are reducible to those of equation sets having no variables, where we use a transformation that substitutes ground terms determined from the equation set and the given two terms into each equation. This result allows us to use decision algorithms for the word problem of an equation set without variables to solve the target problem., IEICE Technical Report;MSS2011-62,IEICE Technical Report;SS2011-47

プログラム検証において,ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている.しかし,検証に有効なループ不変式を自動的に発見することは一般には困難である.本稿では,プログラム変数と関数呼び出し項に関する非線形の不等式で表されるループ不変式を,線形計画法などで利用されるFarkasの補題を拡張した定理に基づいて自動生成する手法を示す., Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automatically find meaningful loop invariants. In this report, we present a method for automatically generating loop invariants in the form of extended polynomial inequality, in which function instances may be included, over program variables. The method is based on the extended polynomial lemma which is improved to Farkas' Lemma., IEICE Technical Report;MSS2011-61,IEICE Technical Report;SS2011-46

論理式の充足可能性判定問題(SAT問題)を解くSATソルバの高速化の一手法として,馬野らは2010年にCNFへの基本対称節の導入を提案した.彼らのSATソルバは,節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある.そこで, Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法(2リテラル監視法)に基づく実現が可能であれば,バックトラックが軽くなるため更なる高速化が期待できる.しかしながら,基本対称節の性質から二つのリテラルのみの監視では十分でなく,そのままでは高速化が期待できない.本論文では,通常の節(OR節)は二つのリテラルを監視し,基本対称節については節中のリテラルをすべて監視する方法を提案する,実際にこれをMinisatに組み込むことで,本手法の有効性を評価する., Umano et al. introduced elementary symmetric clauses (ES-clauses) into CNF formula in 2010 as a method for improving SAT-solver efficiency. Since their experimental SAT solver is implemented based on two counters that maintain the number of true (false, respectively) literals, it has a drawback that backtracks are heavy. Thus much faster solvers are expected due to light backtracks if it is possible to implement them based on watching two literals for each clause, called two watched literals adopted by modern SAT solvers like Minisat. However, watching two literals for ES-clauses are not enough for efficiency. This paper proposes a method watching two literals for each ordinary clause and watching all literals for each ES-clause, and evaluates this by incorporating it into Minisat., IEICE Technical Report;SS2011-38

The reachability problem for an initial term, a goal term, and a rewrite system is to decide whether the initial term is reachable to goal one by the rewrite system or not. The innermost reachability problem is to decide whether the initial term is reachable to goal one by innermost reductions of the rewrite system or not. A context-sensitive term rewriting system (CS-TRS) is a pair of a term rewriting system and a mapping that specifies arguments of function symbols and determines rewritable positions of terms. In this paper, we show that both reachability for right-linear right-shallow CS-TRSs and innermost reachability for shallow CS-TRSs are decidable. We prove these claims by presenting algorithms to construct a tree automaton accepting the set of terms reachable from a given term by (innermost) reductions of a given CS-TRS.

近年，帰納的定理の証明原理の1つである書換え帰納法が制約付き項書換え系に対応するように拡張され，命令型プログラムの等価性検証に応用するための枠組みが提案された．帰納的定理の証明のためには適切な補題等式を与える必要がある場合が多いが，項書換え系においてこれまで研究が進んでいる補題生成の手法を制約付き項書換え系に対して利用するためには制約部分を扱うための拡張が必要である．本論文では，書換え規則から項の関係を定式化し，その関係に基づいて等式をより一般的な等式に変換する枠組みを提案する．さらに，制約付き項書換え系の書換え帰納法による証明手続きにその枠組みを利用した補題等式の生成・追加機能を組み込むことで，補題等式を予め記述せずに定理自動証明を試み，その有効性を検証する．, Recently, the rewriting induction, which is one of induction principles for proving inductive theorems of an equational theory, has been extended to deal with constrained term rewriting systems. It has been applied to developing a method for proving equivalence of imperative programs. For proving inductive theorem, there are many cases where appropriate lemmas need to be added. To this end, several methods for lemma generation in term rewriting have been studied. However, these existing methods are not effective for cases in constrained term rewriting. In this paper, we propose a framework of lemma generation for constrained term rewriting systems, in which we formalize the correspondences of terms in divergent equations by means of given constrained rewrite rules. We also show an instance of the formalization, and show that due to the framework with the instance, there is no necessity to give lemmas in advance in the examples shown by the previous works.

木オートマトンは項を入力としたオートマトンであり,和集合・補集合・積集合演算に閉じていることや空判定問題が決定可能であることから,項書換え系の性質を調べることに有効である.また,近年,制約付き項書換え系に関する研究が行われており,特に定理自動証明の研究が注目されている.本稿では,等号不等号制約付き木オートマトンの制約を任意の制約系を指定できるように一般化した制約付き木オートマトンを提案し,任意の制約付き木オートマトンに対して決定性と完全性を持ち受理集合が等価である制約付き木オートマトンが存在することを示す.さらに,制約付き木オートマトンのクラスが和・積・補集合演算に閉じていることを示す., Tree automata are useful in analyzing properties of term rewriting systems since the class of recognizable tree languages is closed under union, intersection and complement and since the emptiness problem is decidable. Recently, constrained term rewriting systems are investigated and theorem proving methods of contrained systems attract attention. In this paper, by generalizing tree automata with equality and disequality constraints, we propose tree automata with constraints, for which one can specify structures that give an interpretation of predicate symbols and some function symbols. We also show that for every tree automaton with constraints there exists a deterministic and complete tree automaton with constraints, which recognizes the tree language recognized by the former one. In addition, we show that the class of recognized tree languages for tree automata with constraints is closed under union, intersection and complement., IEICE Technical Report;SS2010-63

Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound for every CTRS w.r.t. reduction, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch’s unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch’s unraveling., RTA 2011 - 22nd Rewriting Techniques and Applications (Monday, May 30, 2011 to Wednesday, June 1, 2011, Novi Sad) Part of RDP'11

Malbolgeは最も難解なプログラミング言語として知られている.本研究では,飯澤らが提案したプログラミング手法に基づいて,Malbolgeが弱チューリング完全性を持つこと示す.そのために,チューリング完全性を持つ正規形のNプログラムをMalbolgeコードに変換できることを示す.ここで,本稿で示す性質が弱チューリング完全性であるのは,Malbolgeが固定されたメモリ空間およびレジスタ長の仮想機械により意味が定められているためである., Malbolge is known as one of the most esoteric programming languages. In this paper, we prove that Malbolge is weakly Turing complete. The proof is based on the Malbolge programming method proposed by Iizawa, et al. We give a transformation from the normal form N-programs known to be Turing complete into Malbolge programs. Completeness that this paper shows is weak one due to the fact that the semantics of Malbolge is hard coded into a virtual machine of which memory space and register length are fixed.

SMTソルバは,指定された述語理論の下で論理式の充足可能性判定を行うツールであり,配列,リスト,キューなどの多くの理論を法として,論理式の充足可能性判定を行うことができる.しかし,利用者自身が定義した理論を法とする論理式の充足可能性判定を行うのは容易ではない.なぜならば,その理論に対する決定手続きを合わせて与えることが必要であるためである.本稿では,等式理論を法とする充足可能性判定手続きを状態遷移系DPLL(R)として定式化し,その実装方式を提案する.DPLL(R)は,与えられた等式理論から項書換え系の完備化手続きを用いて決定手続きを自動的に生成し,充足可能性判定を行う.従って,利用者は等式集合を等式理論として与えるだけでよく,決定手続きを与えなくてよい., SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so on. It is however not easy for users of SMT solvers to specify theories since the theories have to be associated with their decision procedures. In this paper, we formulate the procedure for solving the problem of satisfiability modulo an equational theory (SMET) as a state transition system DPLL(R), and propose its implementation scheme. DPLL(R) generates a decision procedure from a given equational theory and use it to solve the SMET problem. Thus, users can specify equational theories without giving decision procedures.

近年，高速な充足可能性判定ツール（SATソルバ）の開発が進んでいる．これらのツールでは，BCPと呼ばれる変数値の推論とそのバックトラックが実行時間の大半を占めていることが多く，その処理を効率化できればSATソルバの高速化が可能となる．本論文では，「n個の変数のうち，ちょうどk個が真」という基本対称関数に基づく節を導入することにより入力する論理式の大きさが減少することに注目し，SATソルバの効率化を目指す．実際にSATソルバでよく用いられるDPLLアルゴリズムを，基本対称関数に基づく節を導入したCNFを扱えるよう拡張し，その有効性を実験により確かめた．

依存対が右線形右シャローである項書換え系のクラスでは,停止性および最内停止性が決定可能であることが示されている(内山ら2008年).しかし,文脈依存停止性の決定可能性は同クラスのうち,さらに左シャローであるクラスでしか示されていない.文脈依存書換えでは依存鎖中に停止しない項が存在することが,その停止性の解析を困難にしている.本論文ではまず,内山らの決定手続きが働かない左シャローでない項書換え系を例示する.次に,この困難性をもたらす原因を取り除くための十分条件を追加し,このクラスで文脈依存停止性が決定可能となることを示す., It is known that termination and innermost termination are decidable for term rewriting systems (TRSs for short) whose dependency pairs are all right-linear and right-shallow (Uchiyama et al, 2008). However, decidability of context-sensitive termination requires left-shallow restriction to those TRSs. The difficulty of context-sensitive termination analysis is caused by existence of non-terminating terms in dependency chains. In this paper, we first show a left-non-shallow TRS as a counterexample against the decision procedure. Then, we give a sufficient condition to make the procedure work properly, and show that context-sensitive termination is decidable for the class.

以前に我々が提案したプログラム生成系GeneSysは,一階述語論理式で表現された仕様から実行可能なプログラムを生成するが,変換過程の論理式が複雑になりやすい欠点がある.本稿では,仕様の表現方法を条件付き等式(ホーン節)に制限し,単純かつ直観的なプログラム生成系の構築を目指す.その上で,プログラム生成のいくつかの実例を挙げる., Program-generation system GeneSys, which we have ever proposed, generates executable programs from first order equational specifications. The system is, however, apt to create complicated formulas during transformation. Instead, in this paper, we use conditional equations (Horn clauses) as specifications to try constructing a more simple and more intuitive system. On that basis, we give examples of program generation.

項書換え系(TRS)の拡張として高階関数を直接扱える単純型付き項書換え系(STRS)やさらにλ抽象も扱える高階書換え系(HRS)が提案されている.静的依存対法はこれら高階の系における非常に強力な停止性証明法である.静的依存対法で停止性を証明する際には引数切り落とし法や実効規則の概念が重要となる.これらはTRS上で提案されSTRS上に拡張されているが, HRS上では知られていない.本論文ではHRS上の引数切り落とし法と実効規則の概念を与える.さらに我々の成果は単なる拡張ではなく,引数切り落とし法で要求されていた適用条件を取り除き,実効規則の定義から高階変数を介した依存性を取り除くという改良も伴っている., Simply-typed term rewriting systems (STRSs) and higher-order rewrite systems (HRSs) have been proposed to extend term rewriting systems (TRSs). These systems can handle higher-order functions directly, and moreover HRSs are allowed to have a A-abstraction syntax. Static dependency pair methods are very powerful methods for proving termination of these higher-order systems. Notions of argument filtering and usable rules play important roles in proving termination by the static dependency pair method. These notions are proposed on TRSs, and extended to STRSs. However, we have not known these notions on HRSs. In this paper, we extend notions of argument filtering and usable rules onto HRSs. In addition, these extensions include some enhancements : removing an applicable condition demanded by existing argument filtering methods on STRSs, and removing a dependency through higher-order variables from the definition of usable rule.

手続き型プログラムの検証手法として，モデル検査やホーア論理に基づく検証手法が代表的である．一方，項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．本論文では，帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には，自然数上のwhile言語で定義された手続き型関数からプレスブルガー文を規則の制約として持つことが許された制約付き項書換え系への変換を与え，その変換により手続き型プログラムの等価性を書換え系の関数の等価性に帰着させ，潜在帰納法を用いて等価性検証を試みる．この手法を実現するために，合流性を保証するための危険対定理および完備化手続きを制約付き書換えに対応するように拡張する．, In the field of procedural programming, several verification methods based on model checking or Hoare logic have been proposed. On the other hand, in the field of term rewriting, implicit induction and rewriting induction have been widely studied as methods for proving inductive theorems. In this paper, we try to take advantages of methods for proving inductive theorems in verifying procedural functions written in a "while" language with natural number type. More precisely, we propose a transformation from procedural programs to constrained term rewriting systems whose constraints are in Presburger arithmetic, and show that the transformation reduces the equivalence of procedural programs to that of functions in rewrite systems. By verifying the equivalence between rewrite systems, we verify the equivalence between the corresponding procedural functions. To establish this approach, we extend Critical Pair Theorem and the basic completion procedure for constrained systems.

本論文では,例外処理機能をもつオブジェクト指向プログラムの安全性を情報流解析に基づいて検証するための型システムを提案する.例外処理による情報流は,スローされる例外とそれを捕そくする箇所に依存して変化する.この情報流を解析するためには,プログラム中の各文についてどの例外からの制御依存が存在するか把握しなければならない.我々は文がスローし得る例外の集合と文に出現する情報流のあるデータの機密度からなる安全型を導入する.この安全型に基づいて従来の型システムを拡張し,本型システムが非干渉性に対し健全であることを示す.健全性により型付け可能なプログラムは機密データを外部に漏えいしないことが保証される.

LISPのような動的型言語のための柔らかい型の表現力豊かな拡張を提案し,その健全性を示す.この拡張では特に,常に型エラーを起こす式を表す「エラー型」と言う特殊な型を導入する.エラー型を含まない型を持つ式では、実行時の型チェックを省くことが出来る.逆にエラー型そのものが付く式は必ずエラーを引き起こすことがわかるので,このような式はコンパイル時に排除することが出来る., We propose a rich extension of soft typing for dynamically-typed languages like LISP, and prove its soundness. This extension, for example, introduces a special type called "error-type", which denotes a type of such an expression whose evaluation always causes a type error. If an expression is typed without using the "error-type", it means that no runtime check is necessary. Conversely, "error-typed" expressions should be rejected at compile-time, since their evaluation always causes an error.

項書換え系(TRS)と等式集合から等価なTRSを得る変換手続きが様々な目的で提案されている.これらの手続きを活用するにはその停止性を明らかにすることが必要であるが,これまでに手続きの停止性に関する研究はほとんどなされていない.本稿では,TRSと等式集合の変換手続きに共通する特徴を捉えて,共通して適用できる停止性の十分条件を与える.具体的には,手続きの停止性をナローイング到達可能集合の有限性に帰着させる.そして,等式付き書換え系の等式数削減手続き[10]と正規化手続き[2]について停止性の十分条件を与える., Several procedures which transform pairs of term rewriting systems (TRSs, for short) and sets of equations into equivalent TRSs have been proposed so far for different purposes. There has been few works on termination of these procedures, while we need some criteria assuring termination in applying them. In this paper, we show a common sufficient condition for the termination of those procedures. We reduce the termination of the procedures to finiteness of sets of narrowing reachable terms. In particular, we discuss sufficient conditions for the termination of the equation elimination procedure [10] and the normalization procedure [2].

近年,論理式の充足可能性判定ツール(SATソルバ)の高速化が進み,これを利用した数独パズルの解法が提案されている.本稿では,この解法を応用して試作した,対話的に数独パズルの問題を作成するツールについて報告する.このツールでは,「セルに埋めても矛盾を生じない数字の表示」・「削除しても問題が一意性を保つセルの表示」・「問題を手筋のみで解ける範囲の図示」の三つの主要機能を実装している.前者二つの機能は,SATソルバを利用した解法を応用して問題め矛盾・解の一意性を高速に検出することにより実現している., In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulae, have been developed and used in solving Sudoku puzzles. In this paper, we present the interactive tool for designing Sudoku puzzles that we constructed experimentally by using a SAT solver. This tool contains three main functions: 'displaying numbers that can be filled in a cell without a contradiction', 'displaying cells without contributing the uniqueness', 'displaying a partial solution obtained by fundamental techniques.' The implementation of the former two functions relies on efficient checks of a contradiction or uniqueness of the given problem by using a SAT solver.

プログラム生成系GeneSysは一階述語論理で記述された仕様からの実行可能なプログラム生成を目的とした手法である.本論文では,GeneSysで否定記号を含む論理式を扱うために既存の変換規則を拡張し,否定記号を用いた仕様からのプログラム生成の例を示す.また,否定記号に関連する変換規則などを新たに追加し,これによりプログラムの生成が可能になる例を示す., Program-Generation System GeneSys has been proposed, which generated executable programs from first order equational specifications without negation. In this paper, we extend conversion rules of GeneSys in order to handle formulas with negation, and show a program-generation example from a specification with negation. We also propose new conversion rules related to negation and give a example that indicates benefits of the new rules.

本稿では,論理プログラムの非停止性を自動的に証明する手法を提案する.本手法では,与えられた質問パターンを代表する質問から起こり得る導出を木で構成し,その木の中からループを検出することにより質問パターンに対する非停止性を示す.具体的には,質問パターンの入力と出力を変数に置き換えた質問から導出木を構成するが,その導出やループ検出の際に入力に対応する変数を特別扱いすることにより健全性を確保する.実際に本手法を実現したツールを作成し,Termination Competition 2007の論理プログラム部門で与えられているサンプルプログラムを対象とした実験を行い,既存の研究との比較を行う., In this paper, we present a method for automatically proving non-termination of logic programs. Given a program and a question pattern, the method proves non-termination by detecting a loop in the derivation tree constructed from the question that represents an arbitrary questions for the question pattern. For soundness, we distinguish variables given as arguments of predicates, and we keep the distinction in the derivation. We also report an implementation of the method, and compare it with other tools by applying it to programs in LP category of Termination Competition 2007.

システムがどのように外部観測的に振舞うかを規定する振舞仕様の下で、観測を通してシステムの2つの状態が等しいことを振舞等価という。振舞等価性の自動証明法の一つに、潜在帰納法に基づく証明法が提案されている.しかし,この手法では簡約化順序で順序付けができない2つの項が存在するとき振舞等価性の証明に失敗する。本論文では、このような場合にも証明できるようにするために、等式付き書換えを用いた潜在帰納法に基づく証明法を提案する。さらに,完全な仕様の場合には手続き中の条件を判定可能な十分条件に置き換えられることを示す., A behavioral specification is a description of what is supposed to happen. Two states are said to be behaviourally equivalent on a behavioral specification if they are observationally indistinguishable. A proof method based on implicit induction principle have been proposed as an automatic proof method for behavioral equivalence. However it is a problem that the method sometimes fails to prove when two terms that represent states cannnot be ordered by the given reduction order. This paper proposes an implicit induction proof-method based on equational rewriting in order to solve the above problem. We also show a decidable sufficient condition for the context reducibility that used in the procedure.

項書換え系(TRS)の到達可能性問題とは,与えられた2つの項の一方からもう一方にTRSでの書換えにより到達できるか否かという問題であり,一般には決定不能である.そこで,到達可能な項集合(の近似集合)を認識する木オートマトンの生成法が広く研究されている.条件付きTRS(CTRS)に関しては,左線形な結合CTRSについて生成手続きが提案されているが,木オートマトンの自動生成の基準となる近似関数はCTRSについて提案されていない.本稿では,結合CTRSを含むクラスである定向CTRSに着目し,左線形な定向CTRSで到達可能な項集合の近似集合を認識する木オートマトンの生成手続きを提案する.さらに,結合CTRSと定向CTRSのための近似関数,結合CTRSを定向CTRSで表現する方法を提案し,結合CTRSについての生成手続きと比較する., The reachability problem for term rewriting systems (TRSs) is to decide whether one of two given terms is reachable to the other with respect to rewriting by a given TRS. Unfortunately, this problem is undecidable in general. Hence, several methods have been widely studied in order to construct a tree automaton that accepts all terms reachable from terms in a given recognizable set. In conditional rewriting, such methods have been proposed only for left-linear join conditional TRSs. However, the techniques of approximation functions used in automatically constructing tree automata have not been formalized. In this paper, we focus on oriented conditional TRSs since every join conditional TRS can be simulated completely by an oriented one. We first propose a method that, given a left-linear oriented conditional TRS and a recognizable set of terms, constructs a tree automaton recognizing an over-approximated set of reachable terms. Then, we formalize approximation functions for join conditional TRSs and oriented ones, respectively, and compare the constructions for join and oriented systems.