科研費 - 中澤 巧爾
-
論理制約付き項書換えに関する余帰納法に基づくプログラム検証法の開発
研究課題/研究課題番号：24K02900 2024年4月 - 2029年3月
科学研究費助成事業 基盤研究(B)
西田 直樹, 松原 豊, 中澤 巧爾
担当区分：研究分担者
近年，論理制約付き項書換えシステム（LCTRS）を用いたプログラム検証の研究が盛んになっている．本研究では，検証したいプログラムと性質それぞれをLCTRSとその検証問題に変換および帰着し，帰納法に基づいてその問題を解くプログラム検証法を開発する．帰着する検証問題には等価性問題および全パス到達可能性問題を採用し，その成否の検証を試みる．開発のための具体的な課題として，「等価性問題および全パス到達可能性問題の両方を扱う証明系の形式化と実装」，「等価性・実行時エラー非発生・メモリ安全性など様々な性質からLCTRSの検証問題への帰着」，「検証問題が決定可能となるプログラムと性質の特徴づけ」に取り組む．
-
研究課題/研究課題番号：22K11901 2022年4月 - 2026年3月
日本学術振興会 科学研究費助成事業 基盤研究(C) 基盤研究(C)
中澤 巧爾, 木村 大輔, 木村 大輔
担当区分：研究代表者
配分額：4030000円 （ 直接経費：3100000円 、 間接経費：930000円 ）
循環証明体系は，帰納法に相当する原理を証明の循環構造によって表現する証明体系であり，自動証明との相性が良いことが知られている．本研究では，証明体系の重要な性質である「カット除去可能性」に注目する．カット規則は推論規則の一つであるが，カット規則の適用は自動証明においては不都合である．そのため，カット規則の有無で証明能力が不変であるという「カット除去可能性」が期待されるが，多くの循環証明体系ではカット除去可能性が成立しないことが分かっている．本研究では，論理に制限を課した上でのカット除去可能性や，自動証明の邪魔をしない程度までカット規則を制限できないか，などを明らかにする．
今年度は、不動点演算子を含む各種の命題論理と、分離論理に対する循環証明体系に関して、以下の成果を得た。
1. 証明木の各無限枝が有限種類のシーケントしか含まないような無限証明（このような無限証明を，擬有限性を満たす無限証明，と呼ぶ）は循環証明に変換できることを示した。不動点演算子を含む各種の命題論理（古典命題論理、時相論理、様相論理）の無限証明が常にこの擬有限性を満たすことにより、これらの論理については、常に無限証明から有限証明への変換が可能であることが分かる。とくに、この変換においてはカット規則が導入されることはないことから、無限証明体系と循環証明体系の証明能力が等しいこと、および、循環証明体系のカットなし完全性であることを証明した。
2. 有理数権限値をもつ並行分離論理のエンテイルメント（含意命題）判定のために、分離論理の証明体系が利用できることを示し、このエンテイルメント判定が決定可能であることを示した。より詳細には、Brotherstonらによって提案された、メモリアクセスの権限を有利数値で表現した並行分離論理体系に対し、論理式をシンボリック・ヒープに制限した体系を提案した。この体系におけるエンテイルメント判定問題を、権限値なしの分離論理のエンテイルメント判定問題に帰着し、これを循環証明体系における証明探索によって解くアルゴリズムを示すことにより、エンテイルメント判定問題の決定可能性を証明した。
当初の見込みはおおよそ達成できたが、一階述語論理の循環証明体系に関する予想の証明は想定よりも難航したため解決しなかった。現時点で証明の目処が立ったため、次年度前半までに解決する予定である。
引き続き、理論的な面では、一階述語論理の言語を制限した循環証明体系におけるカット除去性を調べる。「関数記号なしの場合、循環証明体系はカット除去可能である」ことを予想しているので、これを証明することを目指す。応用面では、とくに分離論理の循環証明体系においてカット論理式にある種の制限を課しても証明能力が変わらないことを示すことにより、自動証明探索に有用な証明体系を模索することを目指す。 -
データと時間を扱うオートマトンネットワークの合成的アクティブ学習に基づく設計手法
研究課題/研究課題番号：21H03415 2021年4月 - 2026年3月
日本学術振興会 科学研究費助成事業 基盤研究(B) 基盤研究(B)
結縁 祥治, 小川 瑞史, 今井 敬吾, 関 浩之, 中澤 巧爾
担当区分：研究分担者
実データを含むサブシステムの振舞いを拡張有限状態機械(EFSM)としてモデル化し振舞い合成と分解について、通信プロセスの形式化に基づいて振舞いの頑健性として振舞いの安定性を導く設計手法を確立する。この研究においては、システムの分解と合成の検証における抽象モデルと実現モデルとの関係に着目して研究を行う。それぞれのサブシステム自体が持つサンプリングやクロックドリフトに基づく誤差が全体システムの安定性を損なわないことを保証する。合成、分解においては、全体の設計情報に基づいて相互に可能な振舞いを自動的に学習して、効率的で現実的な検証およびテストのためのを設計モデルを導く。
-
研究課題/研究課題番号：21H03421 2021年4月 - 2024年3月
日本学術振興会 科学研究費助成事業 基盤研究(B) 基盤研究(B)
龍田 真, 中澤 巧爾, 木村 大輔, 中澤 巧爾, 木村 大輔
担当区分：研究分担者
ソフトウェア検証理論として近年よい理論(オハーン理論)が提案され理論的にも実用的にも成功しているが, 精度がまだ不十分である. 本研究の大目的は, オハーン理論を発展させることにより高精度なソフトウェア検証を可能にする新理論を構築することである. 本研究の目的は, オハーン理論に一般的述語, 配列, 算術を追加した論理体系に対して, 関数の再帰呼出しを追加し, 再帰データを追加し, また, 関数ポインタ呼出しを追加し, またそれらのアルゴリズムの効率を実装実験により証拠付けることである. この実装システムを用いてOpenSSLおよびgitのCコードのメモリー安全性を検証する.
-
研究課題/研究課題番号：23K20392 2020年4月 - 2025年3月
科学研究費助成事業 基盤研究(B)
酒井 正彦, 東条 敏, 中澤 巧爾
担当区分：研究分担者
演奏によって得られたMIDIデータからの品質の高い採譜手法の確立をめざす。演奏は楽譜以上の情報を持つため、演奏のリズムの推定など自動採譜における困難な課題がある。演奏のリズムの推定は、これまでMIDIのノートオン（音のなり始め）イベントの時刻から、（何拍目かという）楽譜上の時刻への対応関係のうち、誤差の少ない関係を出力していた、本研究では、MIDIのイベントの集まりをトークンと呼ぶ塊に分け、その時刻から楽譜上の時刻への対応関係を予測する。これに加えて、リズムを表す重み付き木文法を考慮することで、得られる楽譜の読みやすさをも考慮した自然でリズムが得られることを目指す。
本研究は、リズムの構造を考慮し自然言語の解析手法の応用により、MIDIデータからの自動採譜手法の確立を目指すことを主な目的としている。
本年度は主に和音を含む単旋律のリズム量子化について研究を進め、以下の成果が得られた。入力となるmidiイベント列の部分列（トークンと呼ぶ）を、同一時刻に起こる楽譜の単位とみなすことで、MIDI入力と楽譜の要素を対応付ける手法を考案した。具体的にイベントの部分列がトークンとみなせるかどうかを表すいくつかの条件について検討を行い、これをシステムに組み込んで実験を行うことで課題を整理した。このシステムは https://git.trs.css.i.nagoya-u.ac.jp/transcription/qparselib/-/tree/mono2 で公開している。その結果、各イベントが発生した時点で鳴っている音の数を前処理によりあらかじめ計算しておくことによって、処理中に入力のMIDIイベントを参照する範囲が限定でき、その結果効率よくトークンであるかどうかの判定ができることが分かった。また、各イベントを楽譜上の時刻に対応させる際の評価値の計算においてリズムの密度の単旋律における定義の拡張が必要であることが判明した。この評価値は出力の精度に大きく影響があると予想されるため注意が必要である。その他、音楽生成理論に基づく自動演奏に対する表情付アルゴリズムを改良し、それらの実験のためのプラットフォームを作成し公開した。（https://git.trs.css.i.nagoya-u.ac.jp/transcription/dm-env）
既存のいずれの自動採譜手法においても、MIDIイベントと楽譜の各要素の不一致の解消のために、音の鳴り始めを表すonイベントと音を止めるoffイベントのうちでoffイベントを無視したところから処理を開始していた。この処理により自動採譜におけるさまざまな問題を引き起こしていた。本年度の研究において、この不一致の問題がイベント系列の分かち書きの概念を導入することによって理論的にスッキリと説明でき、分かち書きを含む日本語文の解析に相当する手法を導入することにより解決する手法を考案した。これはブレークスルーとも言え、高精度な自動採譜への道筋が見えてきたといえる。
これまでに定義した３種類のトークンは、異なる音の高さ（ピッチ）をもつ和音、休符、引き続き音が鳴っていることを表すコンティニュエーションである。ここで和音のトークンは複数の装飾音符を含められるように設計した。そこで、これらのアイデアを自動採譜システムに実装し、実験を行うことにより和音を含む単旋律の自動採譜の精度を高める方向での研究を進める。単旋律のみを扱う場合にも、和音の内まだ鳴り続けているのに一部の音が止まったり、スタッカートの取り扱いなどいくつもの課題が残っている。これらの問題点に対して新たなトークンを導入することで解決できるか、あるいは、他の解決方法を考案する必要があるかなどの検討をおこなう。これらが早期に解決できれば、複旋律が一緒に記録されたMIDI入力に対しても、リズム量子化と旋律分離を同時に行う手法についても検討したい。 -
研究課題/研究課題番号：18K11161 2018年4月 - 2021年3月
日本学術振興会 科学研究費助成事業 基盤研究(C) 基盤研究(C)
中澤 巧爾, 木村 大輔
本研究では，帰納的に定義された述語を含む論理式に対する証明体系である循環証明体系に注目し，その基本性質であるカット除去可能性などの証明論的性質を調べた．主な成果は以下のとおりである．(1) プログラム検証に利用されている分離論理において，シンボリックヒープと呼ばれる論理式のクラスに対する循環証明体系ではカット除去ができない例があることを示した．(2) この循環証明体系において，カットをある種の部分論理式にまで制限しても証明能力が真に異なることを示した．(3) 分離論理の基盤論理であるbunched logicに対する循環証明体系でもカット除去ができない例があることを示した．
-
実時間性を持つ並行プログラムに対するデバッグのための逆方向計算モデル
研究課題/研究課題番号：17H01722 2017年4月 - 2021年3月
日本学術振興会 科学研究費助成事業 基盤研究(B) 基盤研究(B)
結縁 祥治, 西田 直樹, 関 浩之, 中澤 巧爾
本研究の目的は、並行性をもつソフトウェアにおいて、逆計算のメカニズムを応用して新たな解析手法を与えることである。近年の並行性を持つソフトウェアの振舞いにおいては、同時に実行されるプログラムの振舞いは非決定的であり、どのように相互作用を行ったかということを逆にたどることはプログラムの動的解析にとって非常に重要な情報となる。
この観点において、本研究では、並行性を持つソフトウェアの振舞いモデルの研究を行い、応用技術として、デバッグを目的とした並行性をもつプログラムの逆方向の動的解析手法および関連したプログラム解析技法（情報圧縮、実時間計算、並行プログラムの型づけ）について研究を行った。 -
研究課題/研究課題番号：17H01723 2017年4月 - 2021年3月
日本学術振興会 科学研究費助成事業 基盤研究(B) 基盤研究(B)
五十嵐 淳, 馬谷 誠二, 中澤 巧爾, 海野 広志
漸進的型付けはひとつのプログラム中に静的型付けされる部分と動的型付けされる部分を共存させるための、プログラミング言語技術である．これを先進的なプログラミング言語に適用するための理論的基盤の研究を行った．主な成果は、多相性、セッション型、篩型、非決定性、ML型推論、交差型といった先進的なプログラミング言語機構へ漸進的型付けを導入した計算体系を与え、その性質(型安全性など)を証明した．さらに、漸進的型付けの実装技術として提案されている空間効率のよいコアーション計算を改良し、コアーション渡し形式を経由するコンパイル方法を提案し、実際に実装・評価を行い、その効果を確認した．
-
計算における無限概念と古典論理
2015年4月 - 2018年3月
科学研究費補助金 基盤研究(C)
中澤巧爾
担当区分：研究代表者
-
ソフトウェア契約に基づく高階型付プログラムの理論
2013年4月 - 2016年3月
科学研究費補助金 基盤研究(A)
五十嵐淳
担当区分：研究分担者
-
ストリーム計算のための計算モデル
2012年4月 - 2015年3月
科学研究費補助金 若手研究(B)
中澤巧爾
担当区分：研究代表者
-
バグのないソフトウェア構築環境に関する研究の新展開
2010年4月 - 2013年3月
科学研究費補助金 基盤研究(B)
佐藤雅彦
担当区分：研究分担者
-
二階存在量化子をもつ計算体系
2009年4月 - 2012年3月
科学研究費補助金 若手研究(B)
中澤巧爾
担当区分：研究代表者
-
計算と論理の融合によるバグのないソフトウェア構築環境に関する研究
2007年4月 - 2010年3月
科学研究費補助金 基盤研究(B)
佐藤雅彦
担当区分：研究分担者
-
古典論理の構文論的双対性とその計算論的意味
2006年4月 - 2009年3月
科学研究費補助金 若手研究(B)
中澤巧爾
担当区分：研究代表者
-
安全・安心な環境適応型ソフトウェアの基礎理論に関する研究
2006年4月 - 2007年3月
科学研究費補助金 特定領域研究
五十嵐淳
担当区分：研究分担者
-
古典論理に基づく非決定的計算体系
2004年4月 - 2006年3月
科学研究費補助金 若手研究(B)
中澤巧爾
担当区分：研究代表者
-
変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
2004年4月 - 2006年3月
科学研究費補助金 特定領域研究
佐藤雅彦
担当区分：研究分担者