強正規化性とPER Model

スポンサーリンク

概要

• 論文の詳細を見る

• 本稿では、λ計算と組合せ論理の強正規化性を、型の制約のある/ない状況で調べる。まず、型の制約のない状況において、λ計算の項から組合せ論理の項への変換で、強正規化性を保存し反映するものを与える。それにより、(1)ゲーデルのλ計算の強正規化性の、順序数割り当てによる証明を簡単にできる。また、(2)多相型λ計算の複雑な強正規化性の証明を2つの独立した段階に分けられる。(i)項書換え系の議論と(ii)型理論のモデルの標準的な議論、すなわち、PERモデルによる議論である。

• 一般社団法人情報処理学会の論文
• 1995-11-30

著者

• 赤間 陽二

  東北大学理学研究科数学専攻

• 赤間 陽二

  東京大学大学院理学系研究科情報科学専攻

関連論文

• $\beta$-expansionに関連したFine距離とWalsh関数系 (数学解析の計算機上での理論的展開とその遂行可能性)
• 計算可能無理数を基数とする記数法と計算可能実数 (数学解析の理論的展開の計算機による支援・遂行可能性)
• 強正規化性とPER Model
• Limiting Partial Combinatory Algebras (Towards new interaction between category theory and proof theory)
• A Study of Abramsky's Linear Chemical Abstract Machine
• 合同な四角形による球面タイリングの分類 (アルゴリズムと計算理論の新展開)

スポンサーリンク