MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am interested in models of intuitionistic linear logic, that is, the logic that you get if you take classical linear logic and restrict the set of operators to $\otimes$, $1$, $\multimap$, $\times$, $\top$, $+$, $0$, and $!$. I know what categorical models of this logic are. However I am looking for something more concrete, something that reflects the interpretation that intuitionistic linear logic is about resources.

Intuitionistic linear logic corresponds to a variant of the λ-calculus that cannot only deal with values (which can be duplicated and destroyed at will), but also with resources (which can neither be duplicated nor destroyed by default). The ordinary simply typed λ-calculus can be given a semantics where the meaning of a type is the set of its inhabitants. Can something similar be done for the linear λ-calculus such that the idea of computing with resources is directly expressed?

share|cite|improve this question
1  
I think the paper Abramsky, Computational Interpretations of Linear Logic might be helpful. – aws Jan 25 '14 at 12:40
up vote 4 down vote accepted

I think the Petri net semantics for linear logic probably best captures this intuition that it is a logic about resource manipulation. The idea is that Petri nets model the movement of tokens (i.e., resources) through a network. Here's the money quote from Lokhorst 1997.

Petri nets are models of dynamic processes in terms of types of resources, represent ed by places which can hold to arbitrary nonnegative multiplicity, and how these resources are consumed or produced by actions, represented by transitions. They are usually described in terms of multisets.

Lokhorst, Gert-Jan C. 1997. Deontic linear logic with Petri net semantics. Technical report, FICT (Center for the Philosophy of Information and Communication Technology). Rotterdam. http://homepages.ipact.nl/~lokhorst/deopetri.pdf.

share|cite|improve this answer
    
Thank you; this was very helpful indeed. Lokhorst cites the paper “Linear Logic on Petri Nets” by Engberg and Winskel, which seems to be relevant as well. – Wolfgang Jeltsch Feb 18 '14 at 13:10

The paper "On linear information systems" by Bucciarelli, Carraro, Ehrhard, and Salibra, might be relevant.

Although it fairly quickly wanders off into categorical considerations (so you might already know about it), the basic idea, that is, modeling linear logic by information systems, sounds quite concrete. The authors also mention the resource intuition, but I'm not sure if they make any explicit connections (I haven't studied the paper).

share|cite|improve this answer

So-called relational semantics of linear logic is usually regarded as a denotational semantics reflecting the resource-sensitiveness of the system.

Every type A is interpreted as a set $[\![A ]\!]$, and every proof $\pi$ of a sequent $\Gamma \vdash A$ is interpreted as a binary relation $[\![\pi]\!] \subseteq [\![\Gamma]\!]\times [\![A]\!]$, where clearly $\times$ denotes the product of sets. The interpretation is self-dual, in the sense that $[\![A ]\!] = [\![A^{\bot} ]\!]$. Therefore every operator of linear logic is interpreted in the same way as its dual:

  • both $\otimes$ and its dual "par" (i.e. the upside-down "$\&$"), and in fact even $\multimap$, are interpreted as the product of sets $\times$;
  • both $\&$ and its dual $\oplus$ are interpreted as the disjoint union of sets;
  • $T$ is the empty set $\emptyset$ and 1 is the singleton $\{*\}$;
  • both $!$ and its dual $?$ are interpreted as the finite multisets operator $\mathcal{M}_f$ (for every set $X$ we call $\mathcal{M}_f(X)$ the set of all finite multisets with elements in X).

From the categorical perspective, this means that the category Rel whose objects are sets and whose morphisms are binary relations - together with all the stuff listed above - is a self-dual $\star$-autonomous category (i.e., a symmetric closed monoidal category with a dualizing object $\bot$) and at the same time a cartesian category. This model has been known as a kind of toy model of linear logic since the discovery of the system in the 80's.

By the co-Kleisli construction of the comonad $! = \mathcal{M}_f\,$ one also gets a CCC, i.e. a categorical model of the simply typed $\lambda$-calculus. This one is "less toy". A term $x_1:A_1,\dots,x_n:A_n \vdash M: A$ is interpreted as a binary relation between the disjoint union of all the $\mathcal{M}_f([\![A_i]\!])$ on one side and the set $[\![A]\!]$ on the other. One can see the idea of resources explicitly represented in this interpretation, because of the multiplicities that elements can have in the multisets interpreting the entries of the program. The same can be said for the models of the untyped $\lambda$-calculus that one can find therein. The first one appeared at the end of this article:

[Hyland, Nagayama, Power, Rosolini: A Category Theoretic Formulation for Engeler-style Models of the Untyped λ-Calculus. ENTCS 161 (2006)]

Another one - a relational version of Scott's $D_{\infty}$ - was studied in

http://www.pps.univ-paris-diderot.fr/~ehrhard/pub/rellam.pdf

(this paper is also a decent introduction to all the basic technicalities concerning relational semantics)

and its relation to $D_{\infty}$ was further explored in

[Ehrhard: the Scott model of Linear Logic is the extensional collapse of its relational model. TCS 424 (2012)].

A generalization of relational semantics where binary relations (i.e. matrixes with entries 0 and 1) are replaced with matrixes on more general rings is developed in

[Laird, Manzonetto, McCusker, Pagani: Weighted relational models of typed lambda-calculi. LICS'13]

People in Cambridge are also exploring a 2-categorical approach to semantics of linear logic and $\lambda$-calculus inspired by relational semantics, where binary relations are replaced by pro functors, see for instance:

[Hyland: Some reasons for generalising domain theory. MSCS 20 (2010)]

share|cite|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.