Arrow Research search

Author name cluster

Thomas Ehrhard

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

17 papers
2 author rows

Possible papers

17

FSCD Conference 2023 Conference Paper

The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic

  • Thomas Ehrhard
  • Claudia Faggian
  • Michele Pagani

We consider an extension of multiplicative linear logic which encompasses bayesian networks and expresses samples sharing and marginalisation with the polarised rules of contraction and weakening. We introduce the necessary formalism to import exact inference algorithms from bayesian networks, giving the sum-product algorithm as an example of calculating the weighted relational semantics of a multiplicative proof-net improving runtime performance by storing intermediate results.

Details

TCS Journal 2020 Journal Article

A calculus of branching processes

  • Thomas Ehrhard
  • Jean Krivine
  • Ying Jiang

CCS-like calculi can be viewed as an extension of classical automata with communication primitives. We are interested here to follow this principle, applied to tree-automata. It naturally yields a calculus of branching processes (CBP), where the continuations of communications are allowed to branch according to the arity of the communication channel. After introducing the calculus with a reduction semantics we show that CBP can be “implemented” by a fully compositional LTS semantics. We argue that CBP offers an interesting tradeoff between calculi with a fixed communication topology à la CCS and calculi with dynamic connectivity such as the π-calculus.

Details DOI

CSL Conference 2012 Conference Paper

Collapsing non-idempotent intersection types

  • Thomas Ehrhard

We proved recently that the extensional collapse of the relational model of linear logic coincides with its Scott model, whose objects are preorders and morphisms are downwards closed relations. This result is obtained by the construction of a new model whose objects can be understood as preorders equipped with a realizability predicate. We present this model, which features a new duality, and explain how to use it for reducing normalization results in idempotent intersection types (usually proved by reducibility) to purely combinatorial methods. We illustrate this approach in the case of the call-by-value lambda-calculus, for which we introduce a new resource calculus, but it can be applied in the same way to many different calculi.

Details

CSL Conference 2011 Conference Paper

Full Abstraction for Resource Calculus with Tests

  • Antonio Bucciarelli
  • Alberto Carraro
  • Thomas Ehrhard
  • Giulio Manzonetto

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 the original Scott D infinity 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.

Details

I&C Journal 2011 Journal Article

Probabilistic coherence spaces as a model of higher-order probabilistic computation

  • Vincent Danos
  • Thomas Ehrhard

We study a probabilistic version of coherence spaces and show that these objects provide a model of linear logic. We build a model of the pure lambda-calculus in this setting and show how to interpret a probabilistic version of the functional language PCF. We give a probabilistic interpretation of the semantics of probabilistic PCF closed terms of ground type. Last we suggest a generalization of this approach, using Banach spaces.

Details DOI

CSL Conference 2011 Conference Paper

Resource Lambda-Calculus: the Differential Viewpoint

  • Thomas Ehrhard

We present differential linear logic and its models, the associated resource and differential lambda-calculi, and the Taylor expansion of promotion boxes. We also describe an antiderivative which seems to be available in many models of differential Linear Logic, and we present a very simple categorical axiom for this operation.

Details

CSL Conference 2010 Conference Paper

Exponentials with Infinite Multiplicities

  • Alberto Carraro
  • Thomas Ehrhard
  • Antonino Salibra

Abstract Given a semi-ring with unit which satisfies some algebraic conditions, we define an exponential functor on the category of sets and relations which allows to define a denotational model of differential linear logic and of the lambda-calculus with resources. We show that, when the semi-ring has an element which is infinite in the sense that it is equal to its successor, this model does not validate the Taylor formula and that it is possible to build, in the associated Kleisli cartesian closed category, a model of the pure lambda-calculus which is not sensible. This is a quantitative analogue of the standard graph model construction in the category of Scott domains. We also provide examples of such semi-rings.

Details

I&C Journal 2010 Journal Article

Interpreting a finitary pi-calculus in differential interaction nets

  • Thomas Ehrhard
  • Olivier Laurent

We propose and study a translation of a pi-calculus without sums nor recursion into an untyped version of differential interaction nets. We define a transition system of labeled processes and a transition system of labeled differential interaction nets. We prove that our translation from processes to nets is a bisimulation between these two transition systems. This shows that differential interaction nets are sufficiently expressive for representing concurrency and mobility, as formalized by the pi-calculus. Our study will concern essentially a replication-free fragment of the pi-calculus, but we shall also give indications on how to deal with a restricted form of replication.

Details DOI

MFCS Conference 2010 Conference Paper

Resource Combinatory Algebras

  • Alberto Carraro
  • Thomas Ehrhard
  • Antonino Salibra

Abstract We initiate a purely algebraic study of Ehrhard and Regnier’s resource λ -calculus, by introducing three equational classes of algebras: resource combinatory algebras, resource lambda-algebras and resource lambda-abstraction algebras. We establish the relations between them, laying down foundations for a model theory of resource λ -calculus. We also show that the ideal completion of a resource combinatory (resp. lambda-, lambda-abstraction) algebra induces a “classical” combinatory (resp. lambda-, lambda-abstraction) algebra, and that any model of the classical λ -calculus raising from a resource lambda-algebra determines a λ -theory which equates all terms having the same Böhm tree.

Details

TCS Journal 2008 Journal Article

Uniformity and the Taylor expansion of ordinary lambda-terms

  • Thomas Ehrhard
  • Laurent Regnier

We define the complete Taylor expansion of an ordinary lambda-term as an infinite linear combination–with rational coefficients–of terms of a resource calculus similar to Boudol’s lambda-calculus with multiplicities (or with resources). In our resource calculus, all applications are (multi)linear in the algebraic sense, i. e. commute with linear combinations of the function or the argument. We study the collective behaviour of the beta-reducts of the terms occurring in the Taylor expansion of any ordinary lambda-term, using, in a surprisingly crucial way, a uniformity property that they enjoy. As a corollary, we obtain (the main part of) a proof that this Taylor expansion commutes with Böhm tree computation, syntactically.

Details DOI

CSL Conference 2007 Conference Paper

Not Enough Points Is Enough

  • Antonio Bucciarelli
  • Thomas Ehrhard
  • Giulio Manzonetto

Abstract Models of the untyped λ -calculus may be defined either as applicative structures satisfying a bunch of first-order axioms ( λ -models), or as reflexive objects in cartesian closed categories (categorical models). In this paper we show that any categorical model of λ -calculus can be presented as a λ -model, even when the underlying category does not have enough points. We provide an example of an extensional model of λ -calculus in a category of sets and relations which has not enough points. Finally, we present some of its algebraic properties which make it suitable for dealing with non-deterministic extensions of λ -calculus.

Details

TCS Journal 2003 Journal Article

The differential lambda-calculus

  • Thomas Ehrhard
  • Laurent Regnier

We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus.

Details DOI

TCS Journal 2000 Journal Article

Parallel and serial hypercoherences

  • Thomas Ehrhard

It is known that the strongly stable functions which arise in the semantics of PCF can be realized by sequential algorithms, which can be considered as deterministic strategies in games associated to PCF types. Studying the connection between strongly stable functions and sequential algorithms, two dual classes of hypercoherences naturally arise: the parallel and serial hypercoherences. The objects belonging to the intersection of these two classes are in bijective correspondence with the so-called “serial–parallel” graphs, that can essentially be considered as games. We show how to associate to any hypercoherence a parallel hypercoherence together with a projection onto the given hypercoherence and present some properties of this construction. Intuitively, it makes explicit the computational time of a hypercoherence.

Details DOI

I&C Journal 1999 Journal Article

A Relative PCF-Definability Result for Strongly Stable Functions and some Corollaries

  • Thomas Ehrhard

We prove that, in the hierarchy of simple types based on the type of natural numbers, any finite strongly stable function is equal to the application of the semantics of a PCF-definable functional to some strongly stable (generally not PCF-definable) functionals of type two. Applying a logical relation technique, we derive from this result that the strongly stable model of PCF is the extensional collapse of its sequential algorithms model.

Details DOI

CSL Conference 1998 Conference Paper

Timeless Games

  • Patrick Baillot
  • Vincent Danos
  • Thomas Ehrhard
  • Laurent Regnier

Abstract Two models of classical linear logic are set up. First our recent version of AJM games model which will be our source model. Then the target model, polarized pointed relations, a variant of the plain relational model which is constructed in two steps: first the model of pointed relations, then the additional polarization structure which yields a proper duality. Then the natural time-forgetting map is shown to generate a lax functor from the source to the target. Finally a further refinement of the target model using bipolarities is sketched, giving a closer link with the games model for the interpretation of syntax. Thus a bridge is constructed that goes from a dynamic model to a static model of evaluation.

Details

TCS Journal 1993 Journal Article

A theory of sequentiality

  • Antonio Bucciarelli
  • Thomas Ehrhard

We show that the notion of sequentiality as presented in concrete data structures may be carried to a more general domain-theoretic framework. Cells are replaced by some linear maps on a domain which turns out to be a DI-domain. In a first phase we do not require the cells to be enabled as they are in CDSs, and we get a weak form of cartesian-closedness. Then, by enriching the structure, we get the standard one.

Details DOI
v2026.09.13