A correspondence between Scheme and the lambda(,upsilon)-CS-calculus

[摘要] We study the relationship between the programming language Scheme and the $lambdasb{v}$-CS-calculus. To this end, we define a correspondence between Scheme and $Lambdasb{CS}$-terms--the language of the calculus--where every Scheme term is an abbreviation of a $Lambdasb{CS}$-term. Although Scheme and $Lambdasb{CS}$ have constructs that roughly correspond to each other, the relationship is rather complex: the inclusion of domain predicates in Scheme enforces the uniform treatment of all values in Scheme as procedural abstractions. Therefore, we must conclude that $Lambdasb{CS}$ cannot express Scheme as a notational definition, but only simulate it through a translation. On the other hand, the embedding reveals Scheme;;s object-oriented nature relative to $Lambdasb{CS}$, and provides a formal basis for the development and formal investigation of an object-oriented extension of Scheme.

[发布机构] Rice University