Resource Combinatory Algebras

Abstract. We initiate a purely algebraic study of Ehrhard and Regnier’s resource λ-calculus, by introducing three equational classes of algebras: resource combinatory algebras, resource lambda-algebras and reambda-abstraction algebras. We establish the relations between them, laying down foundations for a model theory of resource λ-calculus. We also show that the ideal completion of a resource combinatory (resp. lambda-abstraction) algebra induces a “classical” combinatory ambda-, lambda-abstraction) algebra, and that any model of the classical λ-calculus raising from a resource lambda-algebra determines a λ-theory which equates all terms having the same B¨ohm tree.

• Type: Journal
• Year: 2010
• Where: MFCS
• Authors: Alberto Carraro, Thomas Ehrhard, Antonino Salibra
• Keywords: Algebra, Combinatory Algebras, MFCS 2010, Resource, Theoretical Computer Science