Bohm's Theorem for Resource Lambda Calculus through Taylor Expansion

摘要

We study the resource calculus, an extension of the A-calculus allowing to model resource consumption. We achieve an internal separation result, in analogy with Bohm's theorem of A-calculus. We define an equivalence relation on the terms, which we prove to be the maximal non-trivial congruence on normalizable terms respecting /3-reduction. It is significant that this equivalence extends the usual ^-equivalence and is related to Ehrhard's Taylor expansion - a translation mapping terms into series of finite resources.