型変換とマージ・オペレータのopfibrationによる意味づけ

概要

論文の詳細を見る
筆者は,オブジェクト指向計算の基礎として,単純型つき計算を拡張した計算λ_mおよびλ^mを考案してきた[2].これらの計算は,実行時に型変換を明示的に挿入することにより,式が唯一の型を持ち,それが計算により変わらないことを保証している.また,メソッドをクラスと分離させ,CLOSの総称関数のように同じ名前を持つメソッドを融合(マージ)して一つの関数として考えることにより,型とクラスを一致させている.これらの特徴は,部分型を型の間の集合の包含関係として扱ったのでは,得ることができない.λ_mとλ^mは,一つのルールが異なるだけであるが,全く異なる動作をする. λ_mの型変換とメソッドのマージの機構は,型の集合をBase Category,それぞれの型に属する値の集合をFiberとするOpfiberationというカテゴリ的構造によって解釈される.本稿では,この意味論を説明することにより,λ_mとλ^mのモデル,動作の違いについて述べる.
一般社団法人情報処理学会の論文
1993-05-28