| 研究概要 |
研究計画調書の段階では、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)という論文として発表した。
|
