Abstract:
We introduce a refinement of the lambda-calculus, where each argument of a function has an explicit multiplicity, indicating how many copies of it are available. The management of these resources is done by means of explicit substitutions (with multiplicity). We show that the resulting calculus has a natural functionality theory, in the sense of Curry, in a fragment of Girard's linear logic. In particular we show a refinement of a result of Coppo and Dezani, namely that a term is convergent if and only if it has a non-trivial functional character.

[PostScript, .ps.gz ]