Showing 1–26 of 26 results for author: Ehrhard, T

From Differential Linear Logic to Coherent Differentiation

Authors: Thomas Ehrhard

Abstract: In this survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are compatible with determinism. Indeed, due to the Leibniz rule of the differential calculus, differential linear logic and the differential lambda-calculus featur… ▽ More In this survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are compatible with determinism. Indeed, due to the Leibniz rule of the differential calculus, differential linear logic and the differential lambda-calculus feature an operation of addition of proofs or terms operationally interpreted as a strong form of nondeterminism. The main idea of coherent differentiation is that these sums can be controlled and kept in the realm of determinism by means of a notion of summability, upon enforcing summability restrictions on the derivatives which can be written in the models and in the syntax. △ Less

Submitted 26 January, 2024; originally announced January 2024.

Coherent Taylor expansion as a bimonad

Authors: Thomas Ehrhard, Aymeric Walch

Abstract: We extend the recently introduced setting of coherent differentiation for taking into account not only differentiation, but also Taylor expansion in categories which are not necessarily (left)additive.The main idea consists in extending summability into an infinitary functor which intuitively maps any object to the object of its countable summable families.This functor is endowed with a canonical… ▽ More We extend the recently introduced setting of coherent differentiation for taking into account not only differentiation, but also Taylor expansion in categories which are not necessarily (left)additive.The main idea consists in extending summability into an infinitary functor which intuitively maps any object to the object of its countable summable families.This functor is endowed with a canonical structure of bimonad.In a linear logical categorical setting, Taylor expansion is then axiomatized as a distributive law between this summability functor and the resource comonad (aka.~exponential), allowing to extend the summability functor into a bimonad on the Kleisli category of the resource comonad: this extended functor computes the Taylor expansion of the (nonlinear) morphisms of the Kleisli category.We also show how this categorical axiomatizations of Taylor expansion can be generalized to arbitrary cartesian categories, leading to a general theory of Taylor expansion formally similar to that of differential cartesian categories, although it does not require the underlying cartesian category to be left additive.We provide several examples of concrete categories which arise in denotational semantics and feature such analytic structures. △ Less

Submitted 3 October, 2023; originally announced October 2023.

Cartesian Coherent Differential Categories

Authors: Thomas Ehrhard, Aymeric Walch

Abstract: We extend to general Cartesian categories the idea of Coherent Differentiation recently introduced by Ehrhard in the setting of categorical models of Linear Logic. The first ingredient is a summability structure which induces a partial left-additive structure on the category. Additional functoriality and naturality assumptions on this summability structure implement a differential calculus which c… ▽ More We extend to general Cartesian categories the idea of Coherent Differentiation recently introduced by Ehrhard in the setting of categorical models of Linear Logic. The first ingredient is a summability structure which induces a partial left-additive structure on the category. Additional functoriality and naturality assumptions on this summability structure implement a differential calculus which can also be presented in a formalism close to Blute, Cockett and Seely's Cartesian differential categories. We show that a simple term language equipped with a natural notion of differentiation can easily be interpreted in such a category. △ Less

Submitted 7 June, 2023; v1 submitted 13 March, 2023; originally announced March 2023.

Comments: This article is a long version of a paper, with the same title and by the same authors, accepted at the ACM/IEEE Symposium on Logic in Computer Science 2023

Integration in Cones

Authors: Thomas Ehrhard, Guillaume Geoffroy

Abstract: Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates ``continuous data types'' such as the real line. So far however, they lacked a major feature to make them a model of more general probabilistic programming languages (notably call-by-value and call-by-push-value languages): a theor… ▽ More Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates ``continuous data types'' such as the real line. So far however, they lacked a major feature to make them a model of more general probabilistic programming languages (notably call-by-value and call-by-push-value languages): a theory of integration for functions whose codomain is a cone, which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory: our definition of integrals is an adaptation to cones of Pettis integrals in topological vector spaces. We prove that such integrable cones, with integral-preserving linear maps as morphisms, form a model of Linear Logic for which we develop two exponential comonads: the first based on a notion of stable functions introduced in earlier work and thesecond based on a new notion of integrable analytic function on cones. △ Less

Submitted 13 March, 2024; v1 submitted 5 December, 2022; originally announced December 2022.

A coherent differential PCF

Authors: Thomas Ehrhard

Abstract: The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite non-determinism and indeed these languages are essentially non-deterministic. In a previous paper we introd… ▽ More The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite non-determinism and indeed these languages are essentially non-deterministic. In a previous paper we introduced a categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces. Based on this semantics we develop a syntax of a deterministic version of the differential lambda-calculus. One nice feature of this new approach to differentiation is that it is compatible with general fixpoints of terms, so our language is actually a differential extension of PCF for which we provide a fully deterministic operational semantics. △ Less

Submitted 25 October, 2023; v1 submitted 9 May, 2022; originally announced May 2022.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 4 (October 26, 2023) lmcs:9969

Coherent differentiation

Authors: Thomas Ehrhard

Abstract: The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite nondeterminism and indeed these languages are essentially non-deterministic. We introduce a categorical fra… ▽ More The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite nondeterminism and indeed these languages are essentially non-deterministic. We introduce a categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces. Based on this semantics we sketch the syntax of a deterministic version of the differential lambdacalculus. △ Less

Submitted 29 November, 2021; v1 submitted 12 July, 2021; originally announced July 2021.

Categorical models of Linear Logic with fixed points of formulas

Authors: Thomas Ehrhard, Farzad Jafarrahmani

Abstract: We develop a denotational semantics of muLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baelde's propositional muMALL with exponentials. Our general categorical setting is based on the notion of Seely category and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of… ▽ More We develop a denotational semantics of muLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baelde's propositional muMALL with exponentials. Our general categorical setting is based on the notion of Seely category and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of sets and relations, least and greatest fixed points are interpreted in the same way. In the second one, based on a category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving them, least and greatest fixed points have distinct interpretations. This latter model shows that muLL enjoys a denotational form of normalization of proofs. △ Less

Submitted 19 May, 2021; v1 submitted 19 November, 2020; originally announced November 2020.

Comments: arXiv admin note: text overlap with arXiv:1906.05593

Journal ref: 36th ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), Jun 2021, Rome, Italy

Upper approximating probabilities of convergence in probabilistic coherence spaces

Authors: Thomas Ehrhard

Abstract: We develop a theory of probabilistic coherence spaces equipped with an additional extensional structure and apply it to approximating probability of convergence of ground type programs of probabilistic PCF whose free variables are of ground types. To this end we define an adapted version of Krivine Machine which computes polynomial approximations of the semantics of these programs in the model. Th… ▽ More We develop a theory of probabilistic coherence spaces equipped with an additional extensional structure and apply it to approximating probability of convergence of ground type programs of probabilistic PCF whose free variables are of ground types. To this end we define an adapted version of Krivine Machine which computes polynomial approximations of the semantics of these programs in the model. These polynomials provide approximations from below and from above of probabilities of convergence; this is made possible by extending the language with an error symbol which is extensionally maximal in the model. △ Less

Submitted 11 August, 2020; originally announced August 2020.

Differentials and distances in probabilistic coherence spaces

Authors: Thomas Ehrhard

Abstract: In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differentia… ▽ More In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful. △ Less

Submitted 4 August, 2022; v1 submitted 26 May, 2020; originally announced May 2020.

Comments: extended version of arXiv:1902.04836 . Improved redaction of the proof of the main result of Section 2 (expectation of computation time)

ACM Class: D.3.1; F.3.2

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 3 (August 8, 2022) lmcs:6511

On the linear structure of cones

Authors: Thomas Ehrhard

Abstract: For encompassing the limitations of probabilistic coherence spaces which do not seem to provide natural interpretations of continuous data types such as the real line, Ehrhard and al. introduced a model of probabilistic higher order computation based on (positive) cones, and a class of totally monotone functions that they called "stable". Then Crubill{é} proved that this model is a conservative ex… ▽ More For encompassing the limitations of probabilistic coherence spaces which do not seem to provide natural interpretations of continuous data types such as the real line, Ehrhard and al. introduced a model of probabilistic higher order computation based on (positive) cones, and a class of totally monotone functions that they called "stable". Then Crubill{é} proved that this model is a conservative extension of the earlier probabilistic coherence space model. We continue these investigations by showing that the category of cones and linear and Scott-continuous functions is a model of intuitionistic linear logic. To define the tensor product, we use the special adjoint functor theorem, and we prove that this operation is and extension of the standard tensor product of probabilistic coherence spaces. We also show that these latter are dense in cones, thus allowing to lift the main properties of the tensor product of probabilistic coherence spaces to general cones. Last we define in the same way an exponential of cones and extend measurability to these new operations. △ Less

Submitted 13 January, 2020; originally announced January 2020.

Non-idempotent intersection types in logical form

Authors: Thomas Ehrhard

Abstract: Intersection types are an essential tool in the analysis of operational and denotational properties of lambda-terms and functional programs. Among them, non-idempotent intersection types provide precise quantitative information about the evaluation of terms and programs. However, unlike simple or second-order types, intersection types cannot be considered as a logical system because the applicatio… ▽ More Intersection types are an essential tool in the analysis of operational and denotational properties of lambda-terms and functional programs. Among them, non-idempotent intersection types provide precise quantitative information about the evaluation of terms and programs. However, unlike simple or second-order types, intersection types cannot be considered as a logical system because the application rule (or the intersection rule, depending on the presentation of the system) involves a condition expressing that the proofs of premises satisfy a very strong uniformity condition: the underlying lambda-terms must be the same. Using earlier work introducing an indexed version of Linear Logic, we show that non-idempotent ty** can be given a logical form in a system where formulas represent hereditarily indexed families of intersection types. △ Less

Submitted 5 November, 2019; originally announced November 2019.

On the denotational semantics of Linear Logic with least and greatest fixed points of formulas

Authors: Thomas Ehrhard, Farzad Jafar-Rahmani

Abstract: We develop a denotational semantics of Linear Logic with least and greatest fixed points in coherence spaces (where both fixed points are interpreted in the same way) and in coherence spaces with totality (where they have different interpretations). These constructions can be carried out in many different denotational models of LL (hypercoherences, Scott semantics, finiteness spaces etc). We also… ▽ More We develop a denotational semantics of Linear Logic with least and greatest fixed points in coherence spaces (where both fixed points are interpreted in the same way) and in coherence spaces with totality (where they have different interpretations). These constructions can be carried out in many different denotational models of LL (hypercoherences, Scott semantics, finiteness spaces etc). We also present a natural embedding of G{ö}del System T in LL with fixed points thus enforcing the expressive power of this system as a programming language featuring both normalization and a huge expressive power in terms of data types. △ Less

Submitted 13 June, 2019; originally announced June 2019.

Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications

Authors: Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, Lorenzo Tortora de Falco

Abstract: This volume contains a selection of papers presented at Linearity/TLLA 2018: Joint Linearity and TLLA workshops (part of FLOC 2018) held on July 7-8, 2018 in Oxford. Linearity has been a key feature in several lines of research in both theoretical and practical approaches to computer science. On the theoretical side there is much work stemming from linear logic dealing with proof technology, compl… ▽ More This volume contains a selection of papers presented at Linearity/TLLA 2018: Joint Linearity and TLLA workshops (part of FLOC 2018) held on July 7-8, 2018 in Oxford. Linearity has been a key feature in several lines of research in both theoretical and practical approaches to computer science. On the theoretical side there is much work stemming from linear logic dealing with proof technology, complexity classes and more recently quantum computation. On the practical side there is work on program analysis, expressive operational semantics for programming languages, linear programming languages, program transformation, update analysis and efficient implementation techniques. Linear logic is not only a theoretical tool to analyse the use of resources in logic and computation. It is also a corpus of tools, approaches, and methodologies (proof nets, exponential decomposition, geometry of interaction, coherent spaces, relational models, etc.) that were originally developed for the study of linear logic's syntax and semantics and are nowadays applied in several other fields. △ Less

Submitted 12 April, 2019; originally announced April 2019.

Journal ref: EPTCS 292, 2019

Differentials and distances in probabilistic coherence spaces

Authors: Thomas Ehrhard

Abstract: In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differenti… ▽ More In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful. △ Less

Submitted 23 August, 2021; v1 submitted 13 February, 2019; originally announced February 2019.

Measurable Cones and Stable, Measurable Functions

Authors: Thomas Ehrhard, Michele Pagani, Christine Tasson

Abstract: We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We… ▽ More We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations. △ Less

Submitted 27 November, 2017; originally announced November 2017.

Probabilistic call by push value

Authors: Thomas Ehrhard, Christine Tasson

Abstract: We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flip** coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotat… ▽ More We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flip** coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotational model of probabilistic coherence spaces, a categorical model of full classical Linear Logic, interpreting data types as coalgebras for the resource comonad. We prove adequacy and full abstraction, generalizing earlier results to a much more realistic and powerful programming language. △ Less

Submitted 8 January, 2019; v1 submitted 15 July, 2016; originally announced July 2016.

Report number: hal-01345847 ACM Class: F.3.2

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 1 (January 9, 2019) lmcs:1537

A Fully Abstract Semantics for Value-passing CCS for Trees

Authors: Shichao Liu, Thomas Ehrhard, Ying Jiang

Abstract: This paper provides a fully abstract semantics for value-passing CCS for trees (VCCTS). The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. The labelled transition semantics is non-sequential, allowing more than one action occurring simultaneously. We develop the theory of behavioral equivalence by introducing both weak barbed… ▽ More This paper provides a fully abstract semantics for value-passing CCS for trees (VCCTS). The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. The labelled transition semantics is non-sequential, allowing more than one action occurring simultaneously. We develop the theory of behavioral equivalence by introducing both weak barbed congruence and weak bisimilarity. In particular, we show that weak barbed congruence coincides with weak bisimilarity on image-finite processes. This is the first such result for a concurrent model with tree structures. Distributed systems can be naturally modeled by means of this graph-based system, and some examples are given to illustrate this. △ Less

Submitted 1 July, 2016; originally announced July 2016.

Comments: arXiv admin note: substantial text overlap with arXiv:1512.00550

An introduction to Differential Linear Logic: proof-nets, models and antiderivatives

Authors: Thomas Ehrhard

Abstract: Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative… ▽ More Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions. △ Less

Submitted 6 June, 2016; originally announced June 2016.

Full abstraction for probabilistic PCF

Authors: Thomas Ehrhard, Michele Pagani, Christine Tasson

Abstract: We present a probabilistic version of PCF, a well-known simply typed universal functional language. The type hierarchy is based on a single ground type of natural numbers. Even if the language is globally call-by-name, we allow a call-by-value evaluation for ground type arguments in order to provide the language with a suitable algorithmic expressiveness. We describe a denotational semantics based… ▽ More We present a probabilistic version of PCF, a well-known simply typed universal functional language. The type hierarchy is based on a single ground type of natural numbers. Even if the language is globally call-by-name, we allow a call-by-value evaluation for ground type arguments in order to provide the language with a suitable algorithmic expressiveness. We describe a denotational semantics based on probabilistic coherence spaces, a model of classical Linear Logic developed in previous works. We prove an adequacy and an equational full abstraction theorem showing that equality in the model coincides with a natural notion of observational equivalence. △ Less

Submitted 4 November, 2015; originally announced November 2015.

CCS for Trees

Authors: Thomas Ehrhard, Ying Jiang

Abstract: CCS can be considered as a most natural extension of finite state automata in which interaction is made possible thanks to parallel composition. We propose here a similar extension for top-down tree automata. We introduce a parallel composition which is parameterized by a graph at the vertices of which subprocesses are located. Communication is allowed only between subprocesses related by an edge… ▽ More CCS can be considered as a most natural extension of finite state automata in which interaction is made possible thanks to parallel composition. We propose here a similar extension for top-down tree automata. We introduce a parallel composition which is parameterized by a graph at the vertices of which subprocesses are located. Communication is allowed only between subprocesses related by an edge in this graph. We define an observational equivalence based on barbs as well as weak bisimilarity equivalence and prove an adequacy theorem relating these two notions. △ Less

Submitted 7 June, 2013; originally announced June 2013.

Comments: 25 pages

ACM Class: F.1.2

The stack calculus

Authors: Alberto Carraro, Thomas Ehrhard, Antonino Salibra

Abstract: We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We g… ▽ More We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions. △ Less

Submitted 29 March, 2013; originally announced March 2013.

Comments: In Proceedings LSFA 2012, arXiv:1303.7136

ACM Class: F.4.1; F.3.2

Journal ref: EPTCS 113, 2013, pp. 93-108

Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

Authors: Thomas Ehrhard, Antonio Bucciarelli, Alberto Carraro, Giulio Manzonetto

Abstract: We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend… ▽ More We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a "must" parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus. △ Less

Submitted 8 October, 2012; v1 submitted 13 September, 2012; originally announced September 2012.

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 4 (October 10, 2012) lmcs:1047

Acyclic Solos and Differential Interaction Nets

Authors: Thomas Ehrhard, Olivier Laurent

Abstract: We present a restriction of the solos calculus which is stable under reduction and expressive enough to contain an encoding of the pi-calculus. As a consequence, it is shown that equalizing names that are already equal is not required by the encoding of the pi-calculus. In particular, the induced solo diagrams bear an acyclicity property that induces a faithful encoding into differential interact… ▽ More We present a restriction of the solos calculus which is stable under reduction and expressive enough to contain an encoding of the pi-calculus. As a consequence, it is shown that equalizing names that are already equal is not required by the encoding of the pi-calculus. In particular, the induced solo diagrams bear an acyclicity property that induces a faithful encoding into differential interaction nets. This gives a (new) proof that differential interaction nets are expressive enough to contain an encoding of the pi-calculus. All this is worked out in the case of finitary (replication free) systems without sum, match nor mismatch. △ Less

Submitted 1 September, 2010; v1 submitted 1 July, 2010; originally announced July 2010.

ACM Class: cs.PL

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 3 (September 1, 2010) lmcs:771

A convenient differential category

Authors: Richard Blute, Thomas Ehrhard, Christine Tasson

Abstract: In this paper, we show that the category of Mackey-complete, separated, topological convex bornological vector spaces and bornological linear maps is a differential category. Such spaces were introduced by Frölicher and Kriegl, where they were called convenient vector spaces. While much of the structure necessary to demonstrate this observation is already contained in Frölicher and Kriegl's book,… ▽ More In this paper, we show that the category of Mackey-complete, separated, topological convex bornological vector spaces and bornological linear maps is a differential category. Such spaces were introduced by Frölicher and Kriegl, where they were called convenient vector spaces. While much of the structure necessary to demonstrate this observation is already contained in Frölicher and Kriegl's book, we here give a new interpretation of the category of convenient vector spaces as a model of the differential linear logic of Ehrhard and Regnier. Rather than base our proof on the abstract categorical structure presented by Frölicher and Kriegl, we prefer to focus on the bornological structure of convenient vector spaces. We believe bornological structures will ultimately yield a wide variety of models of differential logics. △ Less

Submitted 16 June, 2010; originally announced June 2010.

On Linear Information Systems

Authors: A. Bucciarelli, A. Carraro, T. Ehrhard, A. Salibra

Abstract: Scott's information systems provide a categorically equivalent, intensional description of Scott domains and continuous functions. Following a well established pattern in denotational semantics, we define a linear version of information systems, providing a model of intuitionistic linear logic (a new-Seely category), with a "set-theoretic" interpretation of exponentials that recovers Scott continu… ▽ More Scott's information systems provide a categorically equivalent, intensional description of Scott domains and continuous functions. Following a well established pattern in denotational semantics, we define a linear version of information systems, providing a model of intuitionistic linear logic (a new-Seely category), with a "set-theoretic" interpretation of exponentials that recovers Scott continuous functions via the co-Kleisli construction. From a domain theoretic point of view, linear information systems are equivalent to prime algebraic Scott domains, which in turn generalize prime algebraic lattices, already known to provide a model of classical linear logic. △ Less

Submitted 29 March, 2010; originally announced March 2010.

Journal ref: EPTCS 22, 2010, pp. 38-48

A finiteness structure on resource terms

Authors: Thomas Ehrhard

Abstract: In our paper "Uniformity and the Taylor expansion of ordinary lambda-terms" (with Laurent Regnier), we studied a translation of lambda-terms as infinite linear combinations of resource lambda-terms, from a calculus similar to Boudol's lambda-calculus with resources and based on ideas coming from differential linear logic and differential lambda-calculus. The good properties of this translation w… ▽ More In our paper "Uniformity and the Taylor expansion of ordinary lambda-terms" (with Laurent Regnier), we studied a translation of lambda-terms as infinite linear combinations of resource lambda-terms, from a calculus similar to Boudol's lambda-calculus with resources and based on ideas coming from differential linear 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 linear 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 structure" 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. △ Less

Submitted 19 January, 2010; originally announced January 2010.