著者

大堀 淳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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:04478053)

巻号頁・発行日

vol.33, no.3, pp.272-289, 1992-03-15

被引用文献数

1

著者

篠埜 功 大堀 淳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (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構文解析の考え方と原理を理解できることを目指す.

著者

逢坂 美冬 上野 雄大 大堀 淳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.3, pp.3_79-3_95, 2018-07-25 (Released:2018-09-25)

---

一般にWebアプリケーションにおけるWebページの動的生成は,テンプレートエンジンを用い,事前に用意されたテンプレートに対して動的に値を埋め込むことで行う.テンプレートはテキストファイルとして用意され,実行時に読み込まれる.そのため,テンプレートに対する操作は一般に型無しの文字列操作となる.従って,たとえホスト言語が強い型付けを持つ関数型言語であったとしても,実際のテンプレート構造とプログラムの想定の間の不整合は静的に検出されない.本論文では,動的に読み込まれるテンプレートに対して,部分動的レコードに基づく動的型検査を行うことで,型付きのテンプレート操作を実現する言語機構を提案する.この機構は,テンプレートにホール名をラベルとするMLの部分動的レコード型を与え,テンプレートに値を埋め込む操作をレコードの更新演算と同様に型付けする.テンプレートに存在しないホールへの値の埋め込みは型エラーとなる.プログラムが想定するテンプレートの型と実際のテンプレートの構造の整合性は,テンプレートファイル読み込み時に動的に検査する.本論文ではさらに,この機構をML系関数型言語SML#のコンパイラを拡張することで実装し,実例を通じて実用性を検証するとともに,実用上の課題について議論する.

著者

大堀 淳

雑誌

情報処理

巻号頁・発行日

vol.32, no.5, 1991-05-15

著者

大堀 淳

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.32, no.3, pp.3_1-3_1, 2015-07-24 (Released:2015-09-24)

著者

大堀 淳 小野寺 民也 鶴岡 邦敏 布川 博士 牧之内 顕文 安村 通晃

出版者

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

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.33, no.10, pp.1194-1206, 1992-10-15

著者

大堀 淳

出版者

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

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.46, no.11, 2005-11-15

著者

逢坂 美冬 菊地 大介 上野 雄大 大堀 淳 佐々木 加奈子

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.8, no.4, pp.17, 2015-12-04

---

今日広く用いられているWebアプリケーションフレームワークは,プログラムの自動生成やファイル名の命名規約など,プログラミング言語の範囲を超えた記述を要求するものが多い.この方法は,典型的なアプリケーションの開発において生産性が高いと考えられている一方,実行されるコードの全体像を把握することが難しく,フレームワークの想定から外れた,細やかな制御を必要とするアプリケーションを書くことは難しい.この問題を解決する1つの方法は,Webアプリケーションを構成するすべての要素がプログラミング言語の概念で網羅されるようにアプリケーションを構築することである.関数型言語は,高階関数やモジュール言語などの機能による高い記述力を持ち,このようなWebアプリケーション開発に適していると期待できる.従来の関数型言語では,Webアプリケーション開発に必須となる,データベースへのシームレスなアクセスやマルチコアCPUへの対応が不十分なため,言語単体でのWebアプリケーション開発は難しい.本発表では,SML#を用いた試作を通じて,関数型言語による高水準なWebアプリケーション開発の可能性を分析し,単独プロセスのWebサーバーとして動作するユーザプログラムとしてWebアプリケーションを開発する枠組みを提案する.提案手法では,HTTPサーバー機能を含む,サーバーサイドプログラミングに含まれるすべての要素はSML#のプログラムとして構築される.その構成から,SML#が持つCやデータベースとの連携により,データベースを含めた高水準なプログラミングや,マルチスレッドへのスケールアップ性は,自然に得られる.さらに本発表では,クライアントサイドプログラミングや,HTMLのリンクをユーザがたどることによる状態遷移など,本手法とクライアントとの連携の可能性について論じる.

著者

大堀 淳

出版者

東北大学

雑誌

基盤研究(C)

巻号頁・発行日

2007

---

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