M2 LMFI 2025-2026
Preuves et programmes: cours spécialisé
Linear Logic and Quantitative Semantics (Part I)
https://master.math.u-paris.fr/modules/m2lmfi-ppcs/
- Organisation
- 5 weeks, 4 hours per week: January 7th, January 21st, January 28th, February 4th, and March 11th. Courses in the other weeks are taught by Gabriele Vanoni and Patrick Baillot.
- Time and place
- 11am-1pm and 2pm-4pm, location shown here
- Language
- French or English upon request.
Programme
- January 7th: sequent calculus & abstract machines.
- Positive connectives: λ-calculus with sums, call-by-value λ-calculus.
- Abstract rewriting theory with higher-order rewriting systems.
- January 21st-February 4th (3 weeks): linear logic, tools & applications
- Unifying call-by-name and call-by-value
- Application to focusing proof-search for LJ
- Linear logic: proof nets, Girard translations
- March 11th: linearity in programming language semantics
- Constructive classical logic through a linear logic lens
- Linear call-by-push-value: effect and resource modalities
Concepts with linearity in programming languages
Details week per week
Week 1 (January 7th)
The first class was cancelled. In the second class, we saw problems with positive connectives (here, sums) in the λ-calculus, and we introduced an alternative term model of computation with an abstract machine calculus, that has three term categories: commands, expressions and contexts. We gave typing rules for the system and saw that the rules correspond to that of sequent calculus.
Notes
Notes in French: GdT Logique 1 (Section 2) and GdT Logique 2 (Sections 1 and 2).
Homework (for January 21st)
To be returned by e-mail or physical paper.
- Write down the typing derivations in the λ-calculus corresponding to the commuting conversions between ∨ and both of ∧ and ∨ (4 derivations to write).
- In terms of the abstract machine calculus, define tu, πᵢt and δ(t,u,v) together with their typing derivations, such that the derivations correspond to the elimination rules for →,∧,∨ in natural deduction.
Week 2 (January 21st)
We reviewed the calculus from the last time and introduced the notions of underlying sequent, active (e.g. principal) formula, and activation and deactivation. We reviewed the definitions of elimination rules in terms of left-introduction rules. We saw a computational intuition for the three categories t,c,e. We saw how to express structural rules (contraction, weakening) in terms of variable substitution.
We refined the abstract machine calculus to make η-expansions easy to express for all connectives. We introduced a distinction between positive and negative connectives based on their η-expansions, and introduced a new connective: the positive conjunction.
We saw how the η-expansions suggest certain choices in the reductions, and introduced explicit polarity annotations to remove critical pairs in the calculus. We mentioned criteria for a higher-order rewriting system to be confluent: left-linearity and absence of critical pairs. We defined call by name and call by value versions of λ-calculus abstraction and application.
Notes
- 1st course: GdT Logique 2 (Section 2)
- 2nd course: for similar material from a paper you can have a look at Polarised Intermediate Representation of Lambda Calculus with Sums (Sections I to III).
- We have settled on the syntax of polarised intuitionistic sequent calculus (LJpη) from Note on LCBPV figs. 1, 2 & 3 (handed out in class, see also fig. 4) without the connectives !,0,⊤ for the moment (only 1,⊗,⇾,&,⊕).
- Going further: confluence of higher-order rewriting systems which are orthogonal (left-linear, no critical pair): see Femke van Raamsdonk, “Higher-Order Rewriting” (1999), doi:10.1007/3-540-48685-2_17.
Suggested exercise
- Write the typing derivations for the η-expansions of ⊗,⇾,&,⊕.
Homework (for January 28th)
- Consider the λ-term “(λx.z)((λy.yy)(λy.yy))”. Calculate the reductions of this term according to:
- the call by name definitions of λ and application (given in class, or cf. Note on LCBPV, fig. 4, column “call-by-name encoding” taking ε=ε₂=⊖)
- the call by value definitions of λ and application (given in class, or cf. Note on LCBPV, fig. 4, column “call-by-value encoding” taking ε=ε₁=ε₂=+)
- (Optionally) If you are unsatisfied with your previous answers to homework n°2 from January 7th (derivation of elimination rules from left-introduction rules), and wish to do it again, or if you did not return anything yet, you can do so.
Week 3 (January 28th)
Call-by-value (CBV) definition of the λ-calculus in LJp: right-to-left vs. left-to-right; analysis in terms of abstract machine reductions. We introduced the big-step evaluation for the CBV λ-calculus and we showed the equivalence with head reduction for the CBV encoding in LJp. For this purpose we introduced a linearity property of co-variables α with a rewriting lemma. We saw that there exist λ-terms without value that are stuck for the naive CBV λ-calculus, but for which the compatible reduction in LJp reveals hidden reductions (e.g. (λx.ω)(yy)ω where ω=λz.zz).
New examples of “commuting conversions” that are obtained by focusing (e.g. ι1(δt(x.u)(y.v))≃δt(x.ι1(u))(y.ι1(v))): the idea that the right-introduction rules of positive connectives, and the left-introduction rules of negative connectives, hide cuts. Notion of “η-restriction” of LJpη: equivalence between “ς” reductions revealing hidden cuts, defining values/stacks recursively, and unlocking reductions by forcing η-expansions.
Link between cut elimination and abstract machine reduction. Definition of cut-free command. A normal command for compatible reduction is cut-free; the derivation of a well-typed cut-free command gives a cut-free proof. Preservation of typing during reductions (mentioned without proof).
Dealing with structural rules as variable renamings. Compression lemma: for any typing derivation, there is an equivalent derivation that ends with a unique structural rule followed by a non-structural rule.
Focusing proof search: 1) canonical forms for proofs, 2) decision or semi-decision algorithm. Example of a LJpη term in normal form for which η-expansion creates further simplification (⟨z‖μ̄(x,y').⟨z‖μ̄(x',y).c⟩⁺⟩⁺). Focused proofs alternate focused phases (in normal form for focusing reduction) and inversion phases (obtained by maximally η-expanding). Focused phase: choices are made (e.g. A⊕B), order matters. Inversion phase: only one way to proceed, order does not matter.
Inversion: η-expanding for positives on the left of ⊢ and negatives on the right. Definition of inversion relation on multisets of sequents. The inversion relation is terminating and confluent: terminating because decreasing for the multiset order, and confluent because terminating and locally confluent.
Notes
- Note on LCBPV: Sections 1, 3, 4, and the beginning of 6.4, as far as the calculus LJpη without !,0,⊤ is concerned. (This means that the structural rules are given for σ∈Σ(Γ,Γ'), including contraction and weakening.) Also we have not seen the notion of CBPV models and the interpretation of LJpη in CBPV models, so it is possible to ignore the coherence and soundness clauses in the statements.
- For those having notions of category theory, it is also possible to understand the coherence and soundness clauses as referring to an interpretation of intuitionistic sequent calculus in any bi-cartesian closed category, where ⊗ and & coincide (any bi-CCC is such a CBPV model).
- On the Dershowitz-Manna ordering: T. Nipkow, An inductive proof of the well-foundedness of the multiset order.
Homework (for February 4th)
- Value-restricted dual η-expansion for ⊗:
- define positive expressions F(t) and G(t) such that ⟨F(V⊗W)‖S⟩⁺ ▷* ⟨V‖S⟩⁺ and ⟨G(V⊗W)‖S⟩⁺ ▷* ⟨W‖S⟩⁺ for any values V,W and stack S
- show F(V)⊗G(V) ≃ V for any value V (where t⊗u is defined as in fig. 3 from the notes).
- Compute all the transitive reducts, for the inversion relation (§6.4), of the (singleton) multiset {(⊢((1⊗(A⊗(B→C)))⊕D) → ((E&F)⊗G))} where A,...,G are assumed to be atomic formulae.