From Natural Deduction to Sequent CalculusVariablesAdditive PairsMultiplicative PairsFunctionsPersistenceExercisesReferencesLecture Notes onFunctional Computation15-816: Linear LogicFrank PfenningLecture 11February 22, 2012In the linear λ-calculus from last lecture, we interpreted proof reductionsas term reductions in an underlying language of proof terms. This is theoriginal insight behind the Curry-Howard isomorphism [How69], albeit onan natural deduction for (non-linear) intuitionistic logic and simply-typed(non-linear) λ-terms. But there is still a significant step between proof termreduction and an operational semantics. For example, in functional pro-gramming languages such as ML or Haskell, we do not evaluate underλ-abstractions, and we impose a specific order of evaluation for functionssuch as call-by-value or call-by-name. Finding compelling logical under-pinnnings for these is still an active area of research.In this lecture we investigate a specific possibility for analyzing thecomputational content of linear natural deductions, using two pieces al-ready in place: the translation from natural deduction to sequent calculus,and the interpretation of sequent proofs as concurrent processes. Combin-ing these two will give us a concurrent operational semantics for the linearλ-calculus. More details and additional material on this translation can befound in Toninho et al. [TCP12]. This is definitely not the end of the story,however, because other interpretations are possible. We may return to themlater in the course.1 From Natural Deduction to Sequent CalculusIn the last lecture we stated that every natural deduction can be translatedto a sequent calculus proof. Annotating the resulting sequent calculusproofs with their process interpretations will therefore provide us with aLECTURE NOTES FEBRUARY 22, 2012Functional Computation L11.2compilation of linear λ-terms to the session-typed π-calculus. The realiza-tion of this idea is remarkably similar to Milner’s interpretation of functionsas processes [Mil92], even though Milner’s work was rooted in the untypedλ-calculus and π-calculus.Recall that linear hypothetical judgments of natural deduction have theformΓ ; ∆ `` M : Awhere Γ consists of unrestricted variable declarations uj:Bjwhile ∆ con-sists of linear variable declarations xi:Ai. Similarly, sequents annotatedwith process terms have the formΓ ; ∆ ` P :: x : Awhere Γ consists of shared channels uj:Bj, ∆ consists of linear channelsxi:Ai, and x:A is also a linear channel.Therefore, our goal is to translate proof terms M to processes P thatpreserves typing. We see that the processes use one additional channel,along which they offer a service, so the translation will have to take this asa parameter. We write[M]x= Pand expect the theoremFrom Functions to Processes.If Γ ; ∆ `` M : A then Γ ; ∆ ` [M ]x:: x : A.We also expect some connection between reductions on M, as shown in thelast lecture, and process reduction on [M]x, but we will not try to antici-pate it and instead extract it from the translation itself. We now proceedconstruct by construct to see what we obtain.2 VariablesVariables are translated to channels, and even in the statement of our de-sired theorem we did not formally distinguish between them. We restatethe case in the proof, now with proof terms.x:A `` x : AhypLECTURE NOTES FEBRUARY 22, 2012Functional Computation L11.3We construct:x:A ` [x ↔ w] :: w : AidAThis means[x]w= [x ↔ w]3 Additive PairsNext, we consider additive pairs, typed by A N B. First, the introductionrule:∆ `` M : A ∆ `` N : B∆ `` hM, Ni : A N BNIThe introduction rules correspond directly to right rules and we obtain∆ ` [M]x:: x : A ∆ ` [N]x:: x : B∆ ` x.case([M]x, [N]x) :: x : A N BNRSo [hM, Ni]x= x.case([M]x, [N]x). A pair therefore offers a choice betweenits components along the channel x. The client should be able to select thefirst or second component.The elimination rules use cut in the target of the translation, so we cantransport the formula to which we apply the elimination to the left-handside of a sequent. The rule∆ `` M : A N B∆ `` π1M : ANE1therefore becomes∆ ` A N BA ` AidAA N B ` ANL1∆ ` AcutANBNow we annotate this with process terms:∆ ` [M]x:: x : A N Bx:A ` [x ↔ w] :: w : AidAx:A N B ` x.inl; [x ↔ w] :: w : ANL1∆ ` (νx)([M ]x| x.inl; [x ↔ w]) :: w : AcutANBLECTURE NOTES FEBRUARY 22, 2012Functional Computation L11.4So, indeed, the client of a pair [M ]xselects the first component by send-ing inl along x and forwarding the result. Summarizing the three cases forpairs:[hM, Ni]x= x.case([M]x, [N]x)[π1M]w= (νx)([M ]x| x.inl; [x ↔ w])[π2M]w= (νx)([M ]x| x.inr; [x ↔ w])Now we should examine the reduction that arises when a destructor (suchas π1or π2) meets a constructor (such as h−, −i). We obtain:[π1hM, Ni]w= (νx)([hM, Ni]x| x.inl; [x ↔ w]) defn. of []w= (νx)(x.case([M]x, [N]x) | x.inl; [x ↔ w]) defn. of []x−→ (νx)([M]x| [x ↔ w]) process reduction−→ [M]wstructural reductionThe last reduction here comes from a cut where the first premise is anno-tated with [M]xand the second premise is the identity. This reduces to thefirst premise under some renaming to make sure the offer takes place alongthe correct channel.We can see from this that the induced operational semantics on naturaldeduction proof terms is lazy for pairs of type A N B, since the x.case(−, −)prefix protects it from reduction. As predicted, we can project out the de-sired component. It also corresponds directly to the term reductionπ1hM, Ni −→RM4 Multiplicative PairsRecall∆ `` M : A ∆0`` N : B∆, ∆0`` M ⊗ N : A ⊗ B⊗IUnder the translation, and writing in process terms immediately, we obtain∆ ` [M]y:: y : A ∆0` [N]x:: x : B∆, ∆0` (νy)xhyi.([M]y| [N]x) :: x : A ⊗ B⊗RAt this point it is not clear what to make of this. In the synchronous π-calculus the output prefix means that neither [M]ynor [N]xcan reduce. Sothis form of pair also appears to be lazy.LECTURE NOTES FEBRUARY 22, 2012Functional Computation L11.5Perhaps the elimination rule will shed more light on the situation. Weindex terms here with the explicitly mentioned variables or channels thatthey may depend on, because it clarifies the communication patterns. Wehave:∆ `` M : A ⊗ B ∆0, y:A, x:B `` Ny,x: C∆, ∆0`` let y ⊗ x = M in Ny,x: C⊗EHere is the translation, first without process terms:∆ ` A ⊗ B∆0, A, B ` C∆0, A