多相環境計算における強正規化可能性

情報処理学会 Web Site 参考文献8件

書誌事項

タイトル別名
  • タソウ カンキョウ ケイサン ニ オケル キョウ セイキカ カノウセイ
  • Strong Normalization in Polymorphic Environment Calculus

この論文をさがす

抄録

多相環境計算は，環境をファーストクラスオブジェクトとして扱うことができるλ 計算に，多相型体系を導入したものである．これまでに，ML 多相型体系を持つ環境計算とその型推論アルゴリズムは提案し，その主部簡約定理を得ていたが，強正規化可能性定理はまだ得ていなかった．本論文ではML 多相型体系を包含する，2 階型体系を提案し，その強正規化可能性定理を証明する．この性質は，多相環境計算から多相λ 計算（2 階型付λ 計算）への変換をもちいて，多相環境計算の強正規化可能性を多相λ 計算の強正規化可能性に帰着することによって得られる．

Polymorphic environment calculus is a polymorphic lambda calculus with first-class environments. We proposed environment calculus with ML-polymorphic type system and its type inference algorithm and proved principal type theorem with respect to the type system. In this paper, we propose second-order type system for the environment calculs, which includes the ML-polymorphic type system and prove strong normalization theorem with respect to the second-order type system. The theorem is proved by using transformation of the environment calculus to the polymorphic lambda calculus.

収録刊行物

参考文献 (8)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ