Title: Weird models of linear logic
Abstract:
The category of sets and relations is a quite standard denotational
model of linear logic which underlies most denotational models of
this system (coherence spaces, hypercoherence spaces, totality
spaces, finiteness spaces...). In this setting, a formula is
interpreted as a set, and a proof of that formula is interpreted as a
subset of the set interpreting the formula. Logical connectives are
interpreted very simply: tensor product, par and linear implication
are interpreted as cartesian products, whereas direct products (with)
and direct sums (plus) are interpreted as disjoint union. The linear
negation of a set is the same set. The exponential is interpreted as
the functor which maps a set X to the set of all finite multisets of
elements of X.
In the co-Kleisli cartesian closed category of the multiset comonad
there exist models of the untyped lambda calculus, whose theories are
sensible. With this standard multiset-based interpretation of
exponentials, the relational model interprets also the differential
extensions of linear logic and of the lambda calculus. In this
extension of the lambda calculus, terms can be derived
(differentiated) as in differential calculus of real analysis.
In this talk, we show that, given a semi-ring with unit which
satisfies some 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 co-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.
(joint work with A. Carraro and T. Ehrhard)
Antonino Salibra
Dipartimento di Informatica
Universita' Ca'Foscari di Venezia
salibra@dsi.unive.it
http://www.dsi.unive.it/~salibra/