アクセス数 : 954 件
ダウンロード数 : 53 件
この文献の参照には次のURLをご利用ください : https://ir.lib.shimane-u.ac.jp/5086
島根大学総合理工学部紀要. シリーズB 36 巻
2003-03 発行
An Injective CPS-translation for the Extensional λ-calculus
藤田 憲悦
本文ファイル
c0020036r004.pdf
( 198 KB )
内容記述
We give a syntactical proof to the statement that a novel CPS translation with surjective pairing is injective for the extensional λ-calculus. The result itself might be preliminary, since the source language (the extensional λ-calculus) of the translation is a sublanguage of the target language (λ-calculus with surjective pairing). However this paper shows that there exists a nontrivial injection from the extensional λ-calculus into the λ-calculus with surjective pairing. In this sense our result can be regarded as an extension of Plotkin, i.e., a call-by-value simulation of call-by-name λ-calculus with η-rule (extensionality). Moreover, the method presented here can be naturally extended to the case of the extensional λη-calculus which is defined from the extensional λ-calculus together with control operators.
About This Article
Pages
Other Article