2003 Fiscal Year Annual Research Report
| Project/Area Number |
14540119
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
藤田 憲悦 島根大学, 総合理工学部, 助教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
近藤 通朗 東京電機大学, 情報環境学部, 教授 (40211916)
|
|---|
| Keywords | λμ計算 / CPS変換 / 表示的意味論 / カリー・ハワード同型 / 継続 / スコット領域 / Cモノイド |
|---|
| Research Abstract |
直観主義論理と型付きλ計算との対応関係は,カリー・ハワードの同型対応として知られている.λμ計算とは,この対応関係を古典論理まで拡張することによりM.Parigotによって導入された論理体系である.λμ計算はλ計算の自然な拡張となっており,計算モデルとしてそれ自体興味深い体系となっている.本研究では,表示的な意味論の観点から,外延的なタイプフリーλμ計算が固有にもっている計算の構造やその性質をλ計算との比較において解明をして,次の結果が得られた.
(1)継続の概念に基づくλμ計算の表示的意味論:完備半順序集合で,D×D=D=[D→D]を満たす領域Dより,継続の概念に基づくλμ計算のモデルを与えた.この解釈では,継続をDXDの要素として,λμ式を[D×D→D]である連続関数と定義している.従って,外延的なタイプフリーλμ式の意味は,継続を引数にとる連続関数となっている.一方,Cモノイドは,上記領域方程式を満たすカルテシアン閉カテゴリにおける対象Dのエンドモルフィズムとなっている.よってλμ式の意味は,同時に,Cモノイドでも与えられることが明らかになった.
(2)外延的なタイプフリーλμ計算から全射的な組を持つλ計算への全単射的CPS-変換:まず,外延的なλμ計算から全射的な組を持つλ計算への健全なCPS変換を定義した.次に,CPS変換の像で,簡約規則の下で閉じているλ式の集合を生成するために,文脈自由文法を与えた.この形式文法に基づき,λμ計算への逆変換を定義することができた.これにより,上で与えたCPS変換の完全性を示すことができた.さらに,このCPS変換は,λμ式の集合と簡約規則の下で閉じているλ式の集合間の全単射を形成していた.
なお,以上の成果は学術論文でそれぞれ公表されている.
|
-
[Publications] 藤田 憲悦: "λμ計算のモデルについて"コンピュータソフトウェア. 20・3. 73-79 (2003)
-
[Publications] Ken-etsu Fujita: "An injective CPS-translation for the extensional λ-calculus"Memoirs of the Faculty of Science and Engineering, Shimane University, Series B : Mathematical Science. 36. 39-48 (2003)
-
[Publications] Ken-etsu Fujita: "A sound and complete CPS-translation for λμ-calculus"Lecture Notes in Computer Science. 2701. 120-134 (2003)
-
[Publications] Michio Kondo: "Fuzzy congruence on BCI-algebras"Scientiae Mathematicae Japonicae. 57. 191-196 (2003)
-
[Publications] Y.B.Jun, H.S.Kim, M.Kondo: "The class of B-algebras coincides with the class of groups"Scientiae Matheraaticae Japonicae. 58. 93-97 (2003)
-
[Publications] Michio Kondo: "A note on interval-valued subalgebras ideals in BCK-algebras"Far East Jour.of Math.Sciences. 8. 109-119 (2003)
