著者
大堀 淳
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.1, pp.1_30-1_42, 2014-01-27 (Released:2014-03-27)

コンパイラの構文解析器に広く使用されているLR構文解析の原理を解説する.LR構文解析の基礎をなすアイデアは,「正規言語の解析手法を繰り返し使い,文脈自由文法の幅広いクラスを解析する」という(多くの優れたアイデアがそうであるように)単純なものである.Knuthは,この直感的で単純なアイデアを基礎とし,緻密な理論的な展開と巧みな実用化戦略によって,構文解析におけるブレークスルーを達成した.本解説では,LR構文解析が基礎とするアイデアに即してその原理とアルゴリズムの構造を解説する.これらを理解するならば,一般に複雑で難解なものと受け取られているLR構文解析法の全体像が容易に理解できるはずである.本解説では,オートマトンの基礎知識を持つ一般の読者が,LR構文解析の考え方と原理を理解できることを目指す.
著者
大堀 淳 纓坂 智
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.24, no.2, pp.2_113-2_132, 2007 (Released:2007-05-31)

本論文では,パターンマッチングとそのコンパイルを系統的に理解するための表示的意味論を提示し,それを基に,パターンマッチング構文を効率よいコードにコンパイルする系統的なアルゴリズムを提案する.まず,パターンを値の部分集合と見なし,パターンマッチング構文を,マッチングの対象項が含まれる部分集合を決定する機構と見なすことにより,パターンマッチングの集合論的意味論を与える.次に,各パターンの表示的意味を表現する木構造を定義し,それに基づきパターンマッチングのコンパイルアルゴリズムを導出し,このアルゴリズムの正しさを証明する.導出されたアルゴリズムは,分岐の選択に関して正しいばかりでなく,実行時の値のテスト回数に関して最適であり,かつ,冗長なパターンや網羅的でないパターン集合を常に正確に検出することが保証されている.以上構築したアルゴリズムは,Standard MLの拡張言語であるSML#言語に対して実装され,SML#コンパイラのパターンマッチングコンパイルモジュールとしての使用を通じてその実用性が確認されている.
著者
大堀 淳
雑誌
情報処理
巻号頁・発行日
vol.49, no.11, pp.1246-1250, 2008-11-15

SML#は,文部科学省委託研究e-Society基盤ソフトウェアの総合開発の課題「プログラム自動解析に基づく高信頼ソフトウェアシステムの構築技術」の主要な実現目標の1つとして,東北大学電気通信研究所が有限会社算譜工房と共同で開発してきたML系次世代高信頼プログラミング言語である.レコード多相性,ランク1多相性,データベースの多相型理論,相互運用性の型理論,型主導コンパイル理論などの我々の基礎研究成果に基づく種々の機能を含む最先端のML系言語であるばかりでなく,C言語やJAVA,データベースとのシームレスな連携,多バイト文字処理等のライブラリ,自動プログラミングツールなどをサポートする実用性の高い言語を目指している.本稿では,SML#の開発の背景と意図を概観した後,SML#の特徴をプログラム例などを用いて紹介する.
著者
大堀 淳
雑誌
情報処理
巻号頁・発行日
vol.46, no.11, pp.1299, 2005-11-15
著者
大堀 淳
出版者
FIT(電子情報通信学会・情報処理学会)運営委員会
雑誌
情報科学技術フォーラム講演論文集
巻号頁・発行日
vol.8, no.1, pp.319-320, 2009-08-20

本発表では,コンパイラを系統的に構築することを可能にする証明論的な枠組みを提案する.本枠組みでは,ソース言語,ターゲットの機械語言語,さらにコンパイル段階に現れる中間言語は,すべて,論理学の証明システムとして表現され,コンパイルの各段階は,それら証明システム間の証明変換として表現される.さらに,それら証明システム間の証明変換は,証明システムのカット除関係を保存することを示すことができる.この表明論的枠組みは構成的であり,証明システム間の変換が可能であると言う性質の証明から,対応するコンパイル段階を実現するアルゴリズムが抽出できる.このアルゴリズムは,その構成方法から,型と操作的意味を保存することが帰結する.
著者
篠埜 功 大堀 淳
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.2, pp.2_193-2_203, 2012-04-25 (Released:2012-05-20)

SML#はCとの高い相互運用性を持っており,インポート構文により,Cの関数をSML#から整数型などを変換することなく呼び出すことができる.本論文では,SML#プログラム中にCプログラムを直接書けるようにSML#言語の拡張を行う.Cプログラムの埋め込み用の特別な構文をSML#の宣言部分に追加し,その構文内にCプログラムを埋め込めるようにする.この拡張により,Cのプログラムを,トップレベルのみでなく,let式の宣言部分,structure,functor,local宣言等の宣言部分に書くことができるようになる.さらに,埋め込まれたCからSML#プログラム中の変数の値を参照する機能を追加する.
著者
上野 雄大 大堀 淳
出版者
日本ソフトウェア科学会
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.29, no.1, pp.1_191-1_210, 2012-01-26 (Released:2012-02-26)

本論文では,多相レコード計算のコンパイル方式を応用し軽量に実現可能な,型付き関数型言語の第一級オーバーロード方式を提案する.この方式の下では,オーバーロードされた関数は,オーバーロードされた型上のみを動く型変数で束縛された多相型を持つ第一級の関数として扱われる.本機能の実現に要求されるものは,型抽象におけるインスタンス変数の生成と,型適用におけるインスタンスの選択のみであり,これらは多相レコードコンパイルと同様の方式で達成できる.本方式はSML#コンパイラ上に実装され公開されている.
著者
大堀 淳
出版者
Japan Society for Software Science and Technology
雑誌
コンピュータ ソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.31, no.1, pp.1_30-1_42, 2014

コンパイラの構文解析器に広く使用されているLR構文解析の原理を解説する.LR構文解析の基礎をなすアイデアは,「正規言語の解析手法を繰り返し使い,文脈自由文法の幅広いクラスを解析する」という(多くの優れたアイデアがそうであるように)単純なものである.Knuthは,この直感的で単純なアイデアを基礎とし,緻密な理論的な展開と巧みな実用化戦略によって,構文解析におけるブレークスルーを達成した.本解説では,LR構文解析が基礎とするアイデアに即してその原理とアルゴリズムの構造を解説する.これらを理解するならば,一般に複雑で難解なものと受け取られているLR構文解析法の全体像が容易に理解できるはずである.本解説では,オートマトンの基礎知識を持つ一般の読者が,LR構文解析の考え方と原理を理解できることを目指す.
著者
大堀 淳
出版者
東北大学
雑誌
基盤研究(C)
巻号頁・発行日
2007

直観主義的論理学の自然演繹証明システムとラムダ計算との同型関係を拡張・一般化し, 機械語コードの証明論を完成し, コードの最適化やコードの検証をより体系的に行う基礎を構築した。この証明論では, 機械語コードは, 左規則のみからなるある種のシーケント計算として表現され, その操作的意味, すなわち, コードを実行する機械の状態遷移規則は, シーケント計算のカット除去定理の証明から系統的に抽出することができる。さらに, この証明システムは, 低レベルコードのアクセス権限の検証や制御フロー遷移の最適化などの基礎となることが示された。