Abstract: In our paper Uniformity and the Taylor expansion of ordinary (with Laurent Regnier), we studied a translation of lambda-terms as infinite combinations of resource lambda-terms, from a calculus similar to Boudol's lambda-calculus with resources and based on ideas coming from differential logic and differential lambda-calculus. The good properties of this translation wrt. beta-reduction were guaranteed by a coherence relation on resource terms: normalization is linear and stable (in the sense of the coherence space semantics of logic) wrt. this coherence relation. Such coherence properties are lost when one considers non-deterministic or algebraic extensions of the lambda-calculus (the algebraic lambda-calculus is an extension of the lambda-calculus where terms can be linearly combined). We introduce a finiteness on resource terms which induces a linearly topologized vector space structure on terms and prevents the appearance of infinite coefficients during reduction, in typed settings.
Publication Year: 2010
Publication Date: 2010-01-19
Language: en
Type: preprint
Access and Citation
Cited By Count: 3
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot