3
$\begingroup$

I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes:

  1. In intuitionistic linear logic, environments are sets of available resources. In my logic, environments are partially ordered sets: some resources have to be consumed before others.

    • Multiplicative conjunction splits into two connectives: parallel conjunction and sequential conjunction.

    • Linear implication can only consume a resource X, if there is no other resource Y that must be consumed before X.

  2. Logical connectives are usually defined in terms of introduction and elimination rules. In my logic, I need a new kind of rule: usage rules, which describe how a resource can be used in a computation without destroying it.

    • I add a new unary operator, called borrowed pointer, which denotes a non-owning reference to an existing resource.

    • Creating a borrowed pointer uses but does not consume the resource being pointed. In particular, one may always create a borrowed pointer to an existing resource X, even if there is some resource Y that must be consumed before X.

    • No resource may be consumed until all borrowed pointers to it have been consumed. This is my main motivation for introducing the notion of sequential conjunction in the first place.

I want to give a formal presentation of the rules of inference of this logic using natural deduction and sequent calculus. However, I am having trouble coming up with a good notation that succinctly conveys ideas like:

  1. The environment $\Gamma$ can be split into sub-environments $\Delta, \Sigma$, where there is no resource in $\Sigma$ that must be consumed before any resource in $\Delta$.

  2. Given the environment $\Gamma$ and a resource $A \in \Gamma$, the result of adding a resource ${\rm ref} A$ to $\Gamma$, in such a way that ${\rm ref} A$ must be consumed before $A$.

  3. The sequential conjunction of $A$ and $B$.

  4. etc.

What guidelines should I follow in order to design a good notation for this logic?

$\endgroup$
  • $\begingroup$ There is no absolute notion of good presentation. It all depends on what you want to do with it. For proving meta-theorems like cut-elimination, a sequent style presentation might be suitable. For actual reasoning maybe natural deduction is more appropriate. Etc. $\endgroup$ – Martin Berger May 19 '14 at 13:31
  • $\begingroup$ @MartinBerger: The ultimate goal is using this logic as the basis for a type system for a functional language for systems programming. $\endgroup$ – pyon May 19 '14 at 15:34
  • $\begingroup$ Typing systems are often easily seen as logics presented in natural deduction style. $\endgroup$ – Martin Berger May 19 '14 at 15:39
  • $\begingroup$ Maybe the sequent calculus for multiplicative noncommutative logic by Abrusci and Ruet may be an inspiration? $\endgroup$ – Damiano Mazza May 20 '14 at 7:42
  • $\begingroup$ @DamianoMazza: Thanks, I am going to have a look. $\endgroup$ – pyon May 20 '14 at 8:16

Your Answer

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

Browse other questions tagged or ask your own question.