8
$\begingroup$

Question is whether it is possible to model in linear logic two modes of access to a resource. I know that two modes of resources are possible, i.e:

$!r \vdash$ r is infinitely available
$r \vdash \quad$ r is only once available

But what if I don't want to decide whether r is infinitely or only once available. And the query, i.e access, should decide, so:

$*r \vdash r \quad \quad \quad \quad \quad \quad$ r is only checked (like it were !r)
$*r \vdash consume(r)$ r is consumed (like it were r alone)

Can I model a consume(r) and a normal r access in linear logic? Similarly I would like to have produce(r) operator, which then asserts the form *r of a resource.

Improve this question
$\endgroup$
5
  • $\begingroup$ Jan, you can use LaTeX for math in your posts. $\endgroup$
    – Kaveh
    May 4 '11 at 22:10
  • $\begingroup$ \otimes $\otimes$ and \multimap $\multimap$ (checked one of Neel's posts :). $\endgroup$
    – Kaveh
    May 4 '11 at 22:37
  • 1
    $\begingroup$ @Jan, I am not sure what problem you are suggesting. If you want to describe a conjunction of conditions $\exists X. p(a,X) \wedge p(X,b)$, you should be using additive conjunction & ("with"). The entailment $p(a,b) \vdash \exists X. p(a,X) \& p(X,b)$ is provable in linear logic. $\endgroup$
    – Noam Zeilberger
    May 5 '11 at 9:43
  • $\begingroup$ My answer here cstheory.stackexchange.com/questions/5797/… to another question has a few links to papers on planning using linear logic. $\endgroup$
    – Dave Clarke
    Oct 19 '11 at 9:00
  • $\begingroup$ How about using $r\oplus !r$ or $r\& !r$ to model that a choice needs to be made between a single $r$ or an arbitrary number of them? One choice is made externally, the other is made internally (though off the top of my head, I cannot remember which is which). $\endgroup$
    – Dave Clarke
    Oct 22 '11 at 18:57
5
$\begingroup$

With non-commutative linear logic (cf. Retoré 1997, for pomset logic), you can model the sequentiality of checking resources and avoid having the resource checking occur within the scope of whatever choice operator you want to use.

For example, you could model your query so:

$$(r; a \vee b) \multimap (c; r)$$

You might interpret this as saying: if I can take $r$ and then consume $a \vee b$, then I can provide $c$ and then free $r$. Is that the semantics you want?

It looks, unfortunately, like you can't combine non-commutative linear logic with usual linear logic in the sequent calculus and maintain the needed proof-theoretic properties to model planning via proof search. You can do this is the Calculus of Structures, see (Strassburger, 2003), which has been used for planning (Kahramanogullari 2009).

If you want to go the route of having a modality decorating just $t$, well that might be tricky because you essentially want to be able to look at $r$ without consuming it, and without having it available for unlimited use, which is not a propositional attitude of regular linear logic. You can try to see if

$$((?r \otimes a) \vee (?r \otimes b)) \multimap c$$

works for you, but it probably won't, because $?r$ is cheaper than $r$ — it is a bit like having a reference ro $r$; and so does not actually ensure that you can put your hands on $r$. $?!r$ might work better, and is the basis for the two encodings used to model classical logic in linear logic, but to have $r$ doesn't mean you can provide $?!r$. Looking at one of the various weak exponentials for linear logic might help here.

References

  1. Retoré 1997, Pomset logic: a non-commutative extension of classical linear logic
  2. Strassburger 2003, Linear Logic and Noncommutativity in the Calculus of Structures
  3. Kahramanogullari 2009, On Linear Logic Planning and Concurrency, Information and Computation 207:1229 - 1258.
Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy