多重定義と部分型が存在する計算の強正規性と型保存性について
スポンサーリンク
概要
- 論文の詳細を見る
最近,単純型付きλ計算に多重定義と部分型を付け加えた計算λ&-calculusがCastagna, Ghelli, Longoにより提案された.λ&-calculusでは,多重定義と部分型の相互作用のため,強正規性がなりたたない,計算のモデルが考えにくいなどの好ましくない性質を持っている.本論文では,多重定義と部分型の相互作用について研究する.型の非保存性がこの計算の型理論的研究を困難にしている.そこで,型変換を導入することにより,型の保存性の成り立つようにλ&-calculusを変更した二つの計算λ&Cとλ&C^*を考える.これらは,多重定義された関数に対する2つの異なる意味の与え方に対応している.両者は,正規性,型変換の推移性などに異なる性質を持ち,異なるモデルを持つ.
- 一般社団法人情報処理学会の論文
- 1993-10-29
著者
関連論文
- 多重定義と部分型が存在する計算の強正規性と型保存性について
- 型変換とマージ・オペレータのopfibrationによる意味づけ
- マージオペレータを持つレコード計算
- 型継承および高階な総称関数の表示的意味論