Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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|improve this question
1  
I think the paper Abramsky, Computational Interpretations of Linear Logic might be helpful. –  aws Jan 25 at 12:40

1 Answer 1

up vote 1 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|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 at 13:10

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.