The Lambda-calculus with multiplicities
Résumé
We introduce a refinement of the l-calculus, where the argument of a function is a bag of resources, that is a multiset of terms, whose multiplicities indicate how many copies of them are available. We show that this l-calculus with multiplicities has a natural functionality theory, similar to Coppo and Dezani's intersection type discipline. In our functionality theory the conjunction is managed in a multiplicative manner, according to Girard's terminology. We show that this provides an adequate interpretation of the calculus of the calculus, by establishing that a term is convergent if and only if it has a non-trivial functional character.