2002 Fiscal Year Annual Research Report
| Project/Area Number |
14540119
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
藤田 憲悦 島根大学, 総合理工学部, 助教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
近藤 通朗 東京電機大学, 情報環境学部, 教授 (40211916)
|
|---|
| Keywords | タイプフリーラムダミュウ計算 / 表示的意味論 / CPS変換 / 継続的意味論 / タイプフリーラムダ計算 / 不動点演算子 / 制御オペレータ / 完備半順序集合(CPO) |
|---|
| Research Abstract |
直観主義論理の証明とプログラム(ラムダ計算)との対応関係は,カリー・ハワードの同型対応として知られている。ラムダミュウ計算とは,この対応関係を古典論理にまで拡張することによってParigotにより導入された論理体系である。ラムダミュウ計算はラムダ計算の自然な拡張となっており,それ自体興味深い計算体系である。本研究では,特に表示的意味論の観点から,タイプフリーのラムダミュゥ計算が固有にもっている計算の構造やその性質を,ラムダ計算との比較において解明して,以下の二つの成果が得られた。
(1)任意のラムダモデルからラムダミュウモデルが構成可能である:最初に,ラムダミュウ計算のミュウオペレータが不動点演算子によりコード化可能であることが示された。この結果を用いて,ミュウ式μa.Mとそのη展開した式とがβ変換のみで等価となる解釈が与えられた。このアイディアにより,外延的なラムダモデルが任意に与えられると,Godel-Gentzenの変換を介して,外延的なラムダミュウモデルが構築された。本結果の副産物として,ミュウオペレータは無限に続くラムダ抽象として解釈可能であることが明らかになった。
(2)ラムダミュウ計算の継続的な意味論は,CPS変換の像に対するScott流の直接的な意味論と模倣関係にある:再帰的な領域方程式D×D=D=[D→D]を満たす任意の領域Dより,ラムダミュウ計算の継続的意味論を与えた。次に,ラムダミュゥ計算からラムダ計算への構文的な変換であるCPS変換を定義した。そして,その像に対する所謂Scott流の直接的な意味論と,前述の継続的な意味論との間には完備半順序集合(CPO)上の形式的な模倣関係が定義可能であることが示された。
なお,以上の二つの結果は,学術論文によりそれぞれ公表されている。
|
-
[Publications] Ken-etsu Fujita: "An interpretation of λμ-calculus in λ-calculus"Information Processing Letters. 84. 261-264 (2002)
-
[Publications] Ken-etsu Fujita: "Continuation semantics and CPS-translation of λμ-calculus"Scientiae Mathematicae Japonicae. 57・1. 73-82 (2003)
-
[Publications] Michio Kondo: "On the structure of weak interlaced bilattice"Proc. 32^<nd> International Symposium for Multiple-Valued Logic. 23-26 (2002)
-
[Publications] H.J.Jung, M.Kondo, S.M.Hong: "Intuitionistic fuzzy filters in BCH-algebras"Mathematica Japonica Online. 7. 337-345 (2002)
