Unformatted text preview:

Interpreting JudgmentsCut as CompositionIdentity as ForwardingComposing CutsInputReductionExample: Coin ExchangeExercisesReferencesLecture Notes onCut Reduction as Computation15-816: Linear LogicFrank PfenningLecture 4January 30, 2012In this lecture we will examine a computational interpretation of linearlogic in its sequent formulation. We largely follow a recent paper by Caireset al. [CPT12], which contains additional details and further references. Thebasic idea is that propositions correspond to session types [Hon93], proofs toprocess expressions in the π-calculus [MPW92], and cut reduction to pro-cess reduction. We do not assume that you already know the π-calculus,although clearly it will be easier to follow the lecture if you do.1 Interpreting JudgmentsIn a functional setting, the basic judgment is generally of the form M :A, meaning either that M is a proof of A, or M is a term of type A. Inthe setting of communicating processes, it is unclear what it would meanto say that “P is a process of type A”. Processes communicate with theirenvironment, so we write instead P :: x : A, meaning P is a process offeringservice A along channel x. The channel here is considered a variable withscope P , so we can rename it as P {y/x} :: y : A if y is not already used in P .As is customary, we will perform such renamings silently as appropriate.Processes are uninteresting unless they are placed in a context wherethey not only offer services, but also use services offered by other processes.We write a sequentx1:A1, . . . , xn:An` P :: x : Ato express that process P offers service A along x when composed withprocesses Piproviding Aialong xifor 1 ≤ i ≤ n. All the variables xiLECTURE NOTES JANUARY 30, 2012Cut Reduction as Computation L4.2must be distinct. This just a decoration of a sequent ∆ ` A that labels theconclusion as well as all resources in ∆ uniquely. We continue to write ∆for the resources, now labeled by channels.Offering and using services are counterparts, but they are not the same.Therefore, formally, the judgment x:A on the right of the sequent and thejudgment xi:Aion the left should be considered different. Since we canalways tell by position which one is meant, we use the same notation forboth.Processes evolve through interactions along channels. Interacting ona channel xitherefore engenders a change of state, and the same channelcannot be used again with the same type. Therefore the turnstile symbol ‘`’denotes a linear hypothetical judgment [CCP03] where each antecedent mustbe used exactly once. Therefore the context is not subject to weakening orcontraction, but reordering is permitted since antecedents are identified byunique names.Even without defining any particular kind of service, some principlesshould hold for the judgments in general. We discuss these first, becausethey are an important guide to the rest of the development.2 Cut as CompositionWhen a process P offers service A along x, and another process Q uses a ser-vice A along x, the two can be composed so that they communicate alongx.∆ ` P :: x : A ∆0, x:A ` Q :: z : C∆, ∆0` (νx)(P | Q) :: z : CcutThe process expression for the composition puts P and Q together in a par-allel composition (P | Q), sharing x as a private channel, as indicated by thename restriction (νx). Note that this rule entails some implicit renaming, be-cause the channel along which P offers A must be equated with the channelalong which Q uses A. In the π-calculus, (νx)P is a binder for the variablex with scope P.Viewed from the purely logical perspective, this is simply the rule of cutin linear logic:∆ ` A ∆0, A ` C∆, ∆0` CcutIt is a little unusual that we use an intuitionistic version of linear logic witha singleton right-hand side in a sequent formulation. This is not absolutelyLECTURE NOTES JANUARY 30, 2012Cut Reduction as Computation L4.3essential (see [Abr93] for a related classical counterpart), but it streamlinesthe judgmental justification of the system. It also reflects an intrinsic asym-metry between offering and using a service, even though we will see theyare strongly related. It will also be beneficial in developing a dependenttype theory.3 Identity as ForwardingOne way to fulfill the promise of A along x is to just use a channel y that inturn promises A. This just corresponds to the identity rule.y:A ` [y ↔ x] :: x : AidThere is no standard notation for forwarding in the π-calculus, so we write[y ↔ x] to forward between y and x. We can implement the forwarding be-havior in the untyped π-calculus, but it is convenient to have it as a primi-tive for the session type discipline.In accordance with the linear hypothetical judgment, the antecedent y:Amust be the only one. In purely logical form:A ` AidIn summary, cut and identity connect offers and uses of services. Cutcomposes a process P that offers A along x with a process that uses A alongx, making x a private channel (νx)(P | Q). Identity uses a channel y sup-plying A to satisfy its own offer of x along A, [y ↔ x]. These general princi-ples are not connected to any particular services, which will be associatedwith logical connectives.4 Composing CutsMultiple parallel compositions should be required to synchronize only tothe extent that their interactions require it. Proof-theoretically, this meansthat the order of consecutive cuts should be insignificant. The correspond-ing laws have no inherent orientation as rewrite rules, so we think of themas structural proof equivalences. We leave it to the reader to write outLECTURE NOTES JANUARY 30, 2012Cut Reduction as Computation L4.4the simple proof figures. On the process calculus we obtain correspond-ing structural congruences.(νx)((νy)(P | Q) | R) ≡ (νy)(P | (νx)(Q | R))provided x 6∈ fn(P ), y 6∈ fn(R)(νx)(P | (νy)(Q | R)) ≡ (νy)(Q | (νx)(P | R))provided x 6∈ fn(Q), y 6∈ fn(P )These can be derived from more fundamental structural equivalences ofassociativity of parallel composition and scope extrusion.(P | Q) | R ≡ P | (Q | R) associativityP | Q ≡ Q | P commutativityP | (νx)Q ≡ (νx)(P | Q) scope extrusionprovided x 6∈ fn(P )The last rule comes with a side condition, namely that the variable x is notamong the free names in P . Since (νx) is a binder, this just makes surethat two different variables with the same name are not confused. We canalways (silently) rename the bound variable to allow the scope extrusion tohappen in case there is a conflict.In


View Full Document

CMU CS 15816 - Lecture

Download Lecture
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?