2000 Fiscal Year Annual Research Report

論理体系の意味論と文法的性質の関係

Research Project

Project/Area Number	12680329
Research Institution	Chiba University
Principal Investigator	桜井貴文千葉大学, 理学部, 助教授 (60183373)
Co-Investigator(Kenkyū-buntansha)	山本光晴千葉大学, 理学部, 助手 (00291295) 古森雄一千葉大学, 理学部, 教授 (10022302) 辻尚史千葉大学, 理学部, 教授 (70016666)
Keywords	様相部分構造命題論理 / カット除去 / 正規化 / 文法的性質 / explicit environment / context / 代入操作
Research Abstract	研究計画調書の段階では、12年度には様相部分構造命題論理のカット除去可能定理の証明ができる意味論的な枠組みが成立するための条件を明らかにすることにより更に一般的なモデルを構成し、13年度にはより強力な証明図正規化定理を証明する、という目標を立てた。現在考えている様相部分構造命題論理体系はシークエント計算による形式化がされているFLという論理体系であり、この目標に到達するには自然演繹による同等の論理体系を作らなければならないと考えていた。そのためには様相!と?から作られる型を持つ項を作らなければならないが、?に関しては困難で先行研究も見られなかった。しかし、下で述べるexplicit substitutionに関する研究に関して参考にした論文("The Cut Rule and Explicit Substitutions"(R.Vestergaard))により、シークエント計算による体系に項を付与すればカットがexplicit substitutionに対応し、その項に対する計算規則を与えることができることがわかった。上記の研究と並行してexplicit substitutionに関する研究も行なっており、上記で述べた知見を得ることができたが、その他に、本年度はこれまでの成果を"Explicit Environments"(M.Sato,T.Sakurai,R.Burstall)という論文にまとめ、さらにそれを拡張してfirst-class contextを持つような体系を考えた。contextとはholeを持つλ項であり、contextを体系内で扱えるように拡張することによりメタなレベルで行なっている操作を形式化できるようにするのが目的である。我々が提案した体系では束縛変数は名前を持つので代入操作は従来の名前のα変換による方法を用いることができず、自由変数の名前を変更するという新しい方法を与えた。さらにその体系は通常のλ計算の自然な拡張になっており、合流性は強正規化性という望ましい性質を持っていることを示した。その成果は、"A Simply Typed Context Calculus with First-Class Environments"(M.Sato,T.Sakurai,Y.Kameyama)という論文として発表した。

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] Masahiko Sato: "Explicit Environments"Fundamenta Informaticae. 45・1-2. 79-115 (2001)
[Publications] Masahiko Sato: "A Simply Typed Context Calculus with First-Class Environments"Proc.of 5th FLOPS (LNCS 2024). 359-374 (2001)
[Publications] Takafumi Sakurai: "Categorical Model Construction for Proving Syntactic Properties"Int.Journal of Foundations of Computer Science. (2001)
[Publications] Sachio Hirokawa: "A lambda proof of the P-W theorem"The Journal of Symbolic Logic. 65・4. 1841-1849 (2000)
[Publications] Yuichi Komori: "On Komori algebras"Bulletin of the Section of Logic. (toappear).
[Publications] 山本光晴: "グラフ探索アルゴリズムの発展とその検証"ソフトウェア発展[コンピュータソフトウェア別冊]. 92-108 (2000)

2000 Fiscal Year Annual Research Report

論理体系の意味論と文法的性質の関係

Principal Investigator

桜井 貴文 千葉大学, 理学部, 助教授 (60183373)

Research Products

[Publications] Masahiko Sato: "Explicit Environments"Fundamenta Informaticae. 45・1-2. 79-115 (2001)

[Publications] Masahiko Sato: "A Simply Typed Context Calculus with First-Class Environments"Proc.of 5th FLOPS (LNCS 2024). 359-374 (2001)

[Publications] Takafumi Sakurai: "Categorical Model Construction for Proving Syntactic Properties"Int.Journal of Foundations of Computer Science. (2001)

[Publications] Sachio Hirokawa: "A lambda proof of the P-W theorem"The Journal of Symbolic Logic. 65・4. 1841-1849 (2000)

[Publications] Yuichi Komori: "On Komori algebras"Bulletin of the Section of Logic. (toappear).

[Publications] 山本光晴: "グラフ探索アルゴリズムの発展とその検証"ソフトウェア発展[コンピュータソフトウェア別冊]. 92-108 (2000)

桜井貴文千葉大学, 理学部, 助教授 (60183373)