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

• Item type: Trans(1)
• 公開日: 2005-04-15
• タイトル: 多相環境計算における強正規化可能性
• タイトル / 言語: en
• タイトル: Strong Normalization in Polymorphic Environment Calculus
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 新日鉄ソリューションズ株式会社
• 著者所属: 東京工業大学大学院情報理工学研究科計算工学専攻
• 著者所属(英): en
• 著者所属(英): NS Solutions
• 著者所属(英): en
• 著者所属(英): Department of Computer Science Tokyo Institute of Technology
• 著者名: 清水, 亮; 西崎, 真也
• 著者名(英): Ryo, Shimizu; Shin-ya, Nishizaki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 多相環境計算は，環境をファーストクラスオブジェクトとして扱うことができるλ 計算に，多相型体系を導入したものである．これまでに，ML 多相型体系を持つ環境計算とその型推論アルゴリズムは提案し，その主部簡約定理を得ていたが，強正規化可能性定理はまだ得ていなかった．本論文ではML 多相型体系を包含する，2 階型体系を提案し，その強正規化可能性定理を証明する．この性質は，多相環境計算から多相λ 計算（2 階型付λ 計算）への変換をもちいて，多相環境計算の強正規化可能性を多相λ 計算の強正規化可能性に帰着することによって得られる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 46, 号 SIG6(PRO25), p. 35-46, 発行日 2005-04-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会