| 研究課題/領域番号 |
24700011
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | ラムダ計算 / プログラミング言語のモデル / ストリーム / 型システム |
|---|
| 研究概要 |
本年度は，ストリーム計算を表現する抽象的計算体系であるラムダ・ミュー計算に対するモデルに関して以下の結果を得た．
1. ストリーム・モデルに対して完全な計算体系の研究．型無しラムダ・ミュー計算の外延的モデルとして既に提案しているストリーム・モデルに対して健全かつ完全な計算体系としてラムダ・ミュー-consを提案した．ラムダ・ミュー-consは，ラムダ・ミュー計算に，明示的にストリームを表現する構文を追加し，ストリーム構成子の全射性を公理として追加した体系である．このラムダ・ミュー-consにおいては，ストリーム・モデルとして項モデルを構築することが可能であり，これを利用して，ストリーム・モデルに対して健全かつ完全であることが示される．また，健全性を利用してラムダ・ミュー-consの無矛盾性を証明した．
2. ストリーム計算に対する型システムの研究：ラムダ・ミュー-consに対する型システムを提案し，この型システムに対してストリーム・モデルの考え方を適用した．型システムではストリーム・データの型を無限対の型として自然に表現している．この型付きラムダ・ミュー-consに対するストリーム・モデルを構築し，健全かつ完全であることを証明した．さらに，関数空間と無限対を全て含み，基底型について無限集合であるようなストリーム・モデルが，ラムダ・ミュー-consの外延的等価性を特徴付けることを，ストリーム・モデル上の論理関係を定義することにより証明した．これは，単純型付ラムダ計算とその外延的モデルに対するフリードマンの定理に対応する性質であり，計算体系ラムダ・ミュー-consのある種の正当性を示すものである．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
理論面においてはおおむね予定を超える進度で研究が進められている．
|
| 今後の研究の推進方策 |
理論面については，本年度と同様の方向で引き続き研究を行なう．とくに，型システムの論理的側面についてより深い知見を得られるよう調査を行なう．
次年度はさらに，実際のプログラミングにおけるストリームの扱いについて調査を行ない，理論的成果をより現実のプログラミング言語に応用できるよう，研究を行なう．
|
| 次年度の研究費の使用計画 |
主に，研究成果を国内外の研究集会で発表し，フィードバックを得るための旅費，および，研究会参加費として，また，研究の遂行に必要な書籍の購入費として使用する．
|
