酒井 正彦 SAKAI Masahiko

ID:1000050215597

名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University (2015年 CiNii収録論文より)

Search authors sharing the same name

Articles:  1-20 of 149

  • Heuristics for Automatically Proving Commutativity of Function Composition for Constrained Term Rewriting Systems  [in Japanese]

    KURIKI Ryutaro , NISHIDA Naoki , SAKAI Masahiko , SAKABE Toshiki

    制約付き項書換え系における帰納的定理を書換え帰納法で検証するには,適切な補題等式を与える必要がある場合が多い.制約付き項書換え系における既存の補題生成法では,関数合成の可換性を表すような等式に対して適切な補題を生成できない.本稿では,そのような等式の自動証明に向けて2種類の補題生成法を提案する.それぞれの手法に関するヒューリスティックを提案し,既存手法で証明できない例題を本手法で自動証明できること …

    Technical report of IEICE. SS 114(510), 91-96, 2015-03-09

  • A Heuristic to Solve Inverse Unfolding Problem for Functions Dealing with Tree Structure Data  [in Japanese]

    KATO Tomofumi , NAGASHIMA Masanori , SAKAI Masahiko , NISHIDA Naoki , SAKABE Toshiki

    Unfold/Fold変換はプログラム変換や定理証明などに広く利用されている.Unfold変換とFold変換はそれぞれの逆変換の関係にはなく,多くの場合において一方の変換結果を他方の変換で元に戻すことはできない.そのため,Unfold変換の逆変換を行うことを目的とすることは意味があり,逆Unfold問題とその発見的解法が提案された.しかし,この発見的解法では自然数やリストなどの線形なデータ構造を引 …

    Technical report of IEICE. SS 114(510), 85-90, 2015-03-09

  • Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling  [in Japanese]

    OTA Koichi , HAMAGUCHI Takeshi , SAKAI Masahiko , YAMADA Akihisa , NISHIDA Naoki , SAKABE Tohiki

    本論文では,例外処理を含む関数型プログラムの停止性証明法のひとつである条件付き依存対法の実現について議論する.この手法の実現に必要となる依存対に付帯する制約の充足不能性判定は決定不能問題であるため,本論文ではその充足不能性の十分条件を示す.具体的には,制約中に用いられる組込み関数を定義する書換え規則の集合が合流性と停止性を持つことを利用して十分条件を設計する.また,提案手法を項書換え系の停止性証明 …

    Technical report of IEICE. SS 114(416), 55-60, 2015-01-26

  • Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling  [in Japanese]

    OTA Koichi , HAMAGUCHI Takeshi , SAKAI Masahiko , YAMADA Akihisa , NISHIDA Naoki , SAKABE Tohiki

    本論文では,例外処理を含む関数型プログラムの停止性証明法のひとつである条件付き依存対法の実現について議論する.この手法の実現に必要となる依存対に付帯する制約の充足不能性判定は決定不能問題であるため,本論文ではその充足不能性の十分条件を示す.具体的には,制約中に用いられる組込み関数を定義する書換え規則の集合が合流性と停止性を持つことを利用して十分条件を設計する.また,提案手法を項書換え系の停止性証明 …

    Mathematical Systems Science and its Applications : IEICE technical report 114(415), 55-60, 2015-01-26

  • On Detecting Useless Transition Rules of Constrained Tree Automata  [in Japanese]

    NAKANO Yasuhiro , NISHIDA Naoki , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou , HASHIMOTO Kenji

    項の書換え完全性は,制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に何回も証明を試みられる性質である.また,対象の制約付き項書換え系についての解釈可能な項に関する十分完全性は,定理自動証明中の推論規則の適用条件を緩和させる.これらの性質は書換え可能な項の集合に関する積集合空問題に帰着でき,制約付き本オートマトンを用いた十分条件による証明法が既に提案されている.しかし,既存手法では構成さ …

    Technical report of IEICE. SS 113(489), 31-36, 2014-03-11

  • Malbolge with 20trits word length and its programming  [in Japanese]

    KATO Tatsuki , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou , NISHIDA Naoki

    Malbolgeは最も難解なプログラミング言語として知られている.近年,Malbolgeのための中間言語として低級アセンブリ言語が設計され,そのプログラムからMalbolgeプログラムを生成する低級アセンブラが構築された.しかし,低級アセンブリ言語を用いてプログラミングを行う際,メモリ不足という事態が度々発生していた.例えば,低級アセンブラを利用した数値のインクリメントを行うMalbolgeプログ …

    Technical report of IEICE. KBSE 113(160), 73-78, 2013-07-25

    IR 

  • Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling  [in Japanese]

    HAMAGUCHI Takeshi , SAKAI Masahiko

    先に提案した文脈依存項書換え系(CS-TRS)への変換による例外処理を持つ先行評価に基づく関数型プログラムの停止性・非停止性証明法では,変換で得られるCS-TRSの停止性・非停止性証明に汎用の停止性証明ツールを利用すると非常に短いプログラムしか証明に成功しない.そこで,本論文では例外処理を持つ関数型プログラムから変換されたCS-TRSの停止性証明のための新しい手法を提案する.まず,項書換え系(TR …

    Technical report of IEICE. KBSE 113(160), 61-66, 2013-07-25

    IR 

  • Malbolge with 20trits word length and its programming  [in Japanese]

    KATO Tatsuki , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou , NISHIDA Naoki

    Malbolgeは最も難解なプログラミング言語として知られている.近年,Malbolgeのための中間言語として低級アセンブリ言語が設計され,そのプログラムからMalbolgeプログラムを生成する低級アセンブラが構築された.しかし,低級アセンブリ言語を用いてプログラミングを行う際,メモリ不足という事態が度々発生していた.例えば,低級アセンブラを利用した数値のインクリメントを行うMalbolgeプログ …

    Technical report of IEICE. SS 113(159), 73-78, 2013-07-25

  • Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling  [in Japanese]

    HAMAGUCHI Takeshi , SAKAI Masahiko

    先に提案した文脈依存項書換え系(CS-TRS)への変換による例外処理を持つ先行評価に基づく関数型プログラムの停止性・非停止性証明法では,変換で得られるCS-TRSの停止性・非停止性証明に汎用の停止性証明ツールを利用すると非常に短いプログラムしか証明に成功しない.そこで,本論文では例外処理を持つ関数型プログラムから変換されたCS-TRSの停止性証明のための新しい手法を提案する.まず,項書換え系(TR …

    Technical report of IEICE. SS 113(159), 61-66, 2013-07-25

  • On Composing the Simplex Method and Gomory Cut for Deriving Integer Assignments  [in Japanese]

    FUSHIMI Masaaki , NISHIDA Naoki , SAKAI Masahiko , KUSAKARI Keiichirou , SAKABE Toshiki

    与えられた有理数上の線形制約を充足する割り当てを求める手法として単体法がある.また,有理数解を求める手法と,ゴモリーカットをはじめとする切除平面法を組み合わせることで整数解を求められることが知られている.しかし,単体法を適用した後,必ずしもゴモリーカットが適用可能であるとは限らない.本稿では,ゴモリーカットの合成に必要な単体法における不変条件を示し,単体法とゴモリーカットを合成した手続きを示す.ま …

    Technical report of IEICE. SS 112(458), 109-114, 2013-03-06

  • On Composing the Simplex Method and Gomory Cut for Deriving Integer Assignments  [in Japanese]

    FUSHIMI Masaaki , NISHIDA Naoki , SAKAI Masahiko , KUSAKARI Keiichirou , SAKABE Toshiki

    与えられた有理数上の線形制約を充足する割り当てを求める手法として単体法がある.また,有理数解を求める手法と,ゴモリーカットをはじめとする切除平面法を組み合わせることで整数解を求められることが知られている.しかし,単体法を適用した後,必ずしもゴモリーカットが適用可能であるとは限らない.本稿では,ゴモリーカットの合成に必要な単体法における不変条件を示し,単体法とゴモリーカットを合成した手続きを示す.ま …

    Mathematical Systems Science and its Applications : IEICE technical report 112(457), 109-114, 2013-03-06

    IR 

  • Using SAT Solvers for Solving Control-Instruction Layout Problems in Low-Level Assembly Programming for Malbolge  [in Japanese]

    ANDO Satoshi , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou , NISHIDA Naoki

    Malbolgeは最も難解なプログラミング言語として知られている。低級アセンブリ言語の開発によりMalbolgeのループプログラムの作成が可能になったものの、低級アセンブリプログラムでは変数を引数とする命令はその変数宣言の直前に記述しなければならず実行制御が必要不可欠なことと、制御命令には無条件ジャンプとアクセスの度にジャンプとスルーが入れ替わるフリップフロップジャンプしか存在しないことから、低級 …

    Technical report of IEICE. SS 112(373), 25-30, 2013-01-10

    IR 

  • Construction of Constrained Tree Automata Recognizing Ground Instances of Constrained Terms  [in Japanese]

    NAKANO Yasuhiro , NISHIDA Naoki , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou

    制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に、制約付き項書換え系のR完全性の判定手続きが必要である。また、対象の制約付き項書換え系が十分完全性を持つ場合に、定理自動証明中の推論規則の適用条件を緩和することができる。これらの性質は、制約付き項のインスタンスの集合に関する積集合空問題に帰着できる。本論文では、制約付き項のインスタンスを受理する制約付き木オートマトンの構成法を提案する。さ …

    Technical report of IEICE. SS 112(373), 7-12, 2013-01-10

    IR 

  • A SAT Encoding for Finding Operation Sequences of Malbolge that Implement Trit-wise Functions  [in Japanese]

    ANDO Satoshi , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou , NISHIDA Naoki

    Malbolgeは最も難解なプログラミング言語として知られている.低級アセンブリ言語の開発によりMalbolgeのループプログラムの作成が可能になったものの,低級アセンブリ言語には通常のプログラミング言語が持つような演算命令がなく,Malbolge特有の演算を行う命令のみであるため,低級アセンブリ言語でのプログラミングにも困難が伴う.低級アセンブリプログラミングにおいては,目的のプログラムに必要な …

    Technical report of IEICE. SS 112(275), 7-12, 2012-10-25

    IR  References (12)

  • A SAT Encoding for Finding Operation Sequences of Malbolge that Implement Trit-wise Functions  [in Japanese]

    Satoshi Ando , Masahiko Sakai , Toshiki Sakabe , Keiichirou Kusakari , Naoki Nishida

    Malbolge は最も難解なプログラミング言語として知られている.低級アセンブリ言語の開発により Malbolge のループプログラムの作成が可能になったものの,低級アセンブリ言語には通常のプログラミング言語が持つような演算命令がなく, Malbolge 特有の演算を行う命令のみであるため,低級アセンブリ言語でのプログラミングにも困難が伴う.低級アセンブリプログラミングにおいては,目的のプログラ …

    IPSJ SIG Notes 2012-SE-178(2), 1-6, 2012-10-25

  • On Extending Matching Operation in Grammar Programs for Program Inversion

    NIWA Minami , NISHIDA Naoki , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou

    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 …

    Technical report of IEICE. KBSE 112(165), 103-108, 2012-07-20

    References (12)

  • On Extending Matching Operation in Grammar Programs for Program Inversion

    NIWA Minami , NISHIDA Naoki , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou

    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 …

    Technical report of IEICE. SS 112(164), 103-108, 2012-07-20

    IR  References (12)

  • Introducing Array Mechanism into High-Level Assembly Language for Malbolge  [in Japanese]

    ANDO Satoshi , SAKAI Masahiko , SAKABE Toshiki , KUSAKARI Keiichirou , NISHIDA Naoki

    Malbolgeは最も難解なプログラミング言語として知られている.高級アセンブリ言語の開発によりMalbolgeプログラムの作成が可能になっているものの,プログラム中で使用できる変数の値の最大値が固定されておりゲーデルコーディングが不可能であるため,配列機能がないのは記述力不足であった.本論文ではこの問題を解決するため,高級アセンブラに用いられている実現手法を整理し,これに配列機能のための命令であ …

    Technical report of IEICE. SS 112(23), 43-48, 2012-05-03

    IR  References (8)

  • Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls  [in Japanese]

    SUZUKI Eiichi , SAKABE Toshiki , SAKAI Masahiko , KUSAKARI Keiichirou , NISHIDA Naoki

    プログラム検証において,ループ実行中に常に成り立つ論理式である不変式が重要な役割を持っている.しかし,検証に有効なループ不変式を自動的に発見することは一般には困難である.本稿では,プログラム変数と関数呼び出し項に関する非線形の不等式で表されるループ不変式を,線形計画法などで利用されるFarkasの補題を拡張した定理に基づいて自動生成する手法を示す.

    Technical report of IEICE. SS 111(406), 39-44, 2012-01-26

  • On Usable Rules under Argument Filterings in Higher-Order Rewrite Systems  [in Japanese]

    OOI Kazuhiro , KUSAKARI Keiichirou , SAKAI Masahiko , SAKABE Toshiki , NISHIDA Naoki

    高階書換え系(HRS)での強力な停止性証明手法として静的依存対法が知られている.この手法は静的な再帰構造解析を行い,静的再帰成分と呼ばれる解析結果の非循環性を示すことで証明を行う.この際に,非循環性を示すために考慮すべき規則を絞り込む実効規則と呼ばれる概念が提案されているが,高階変数を介した依存解析が困難であるため規則を絞り込めない場合がある.一方,一階の書換え系ではより考慮すべき規則を絞り込む, …

    Mathematical Systems Science and its Applications : IEICE technical report 111(405), 57-62, 2012-01-26

Page Top