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.

1. Write down the typing derivations in the λ-calculus corresponding to the commuting conversions between ∨ and both of ∧ and ∨ (4 derivations to write).
2. 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.

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 (LJ_p^η) 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:
  1. the call by name definitions of λ and application (given in class, or cf. Note on LCBPV, fig. 4, column “call-by-name encoding” taking ε=ε₂=⊖)
  2. 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.

Call-by-value (CBV) definition of the λ-calculus in LJ_p: 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 LJ_p. 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 LJ_p 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 LJ_p^η: 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 LJ_p^η 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 LJ_p^η 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 LJ_p^η 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 ⊗:
  1. 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
  2. show F(V)⊗G(V) ≃ V for any value V (where t⊗u is defined as in fig. 3 from the notes).
  (For simplifying, we assume that all polarity annotations are + and we can omit them.)
• 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.

First class: End of the presentation of focusing for polarised intuitionistic logic. Shape of inverted sequents. Decreasing measure on terms. Proof of completeness. Examples.

Second class: Multiplicative-additive linear logic. Involutive negation, formulae in negative normal form, one-sided sequents, interpretation as two-sided sequents. Multiplicative and additive connectives and interpretation. Two representations of proofs: proof nets (for multiplicatives only), and polarised calculus (unrestricted). Equation of depolarisation: ⟨t‖μx.⟨u‖μy.c⟩⟩ = ⟨u‖μy.⟨t‖μx.c⟩⟩ for all t,u,c (well-typed). Description of polarities in terms of preservation of structural rules (e.g. positives connectives preserve the ability to contract and weaken on the right). Exponential modalities, sketch of translation of polarised intuitionistic into linear logic.

Notes

• Focusing: Note on LCBPV: Sections 6.4, restricted to the calculus LJ_p^η without !,0,⊤ as before, and without considering the interpretation in CBPV models.
• Linear logic: Pierre-Louis Curien, Introduction to linear logic and ludics, part I, sections 1-3.
• Proof nets: see for instance the LL Handbook, sections 2.1 to 2.3 except what concerns the correctness criterion.
• Synthetic note with figures given in class (with minor corrections): 1) focusing in LJ_p^η, 2) polarised calculus for MALL (MALL_p^η) and for LL (LL_p^η).

Homework (for March 11th)

1. Focusing: let X,Y and Z be positive atoms. Determine all the possible derivations (up to →RE-convertibility) of the following sequents in LJ_p^η. Give the answers in the form of focused normal forms (i.e. obtained from alternations of inversion and focusing phases). Prove that you have found all the possible terms up to →RE-convertibility.
   1. ((X⊕Y)→Z)⊢(X→Z)&(Y→Z)
   2. (X⊗X)⊢(X⊗X)
   3. (X→X)⊢(X→X)
2. Linear logic:
   1. Let A,B,C be arbitrary formulae. Give a derivation of A⊗(B⅋C)⊢(A⊗B)⅋C, both with a term in MALL_p^η and a proof net.
   2. Definition: a formula A is !-fix if A⊢!A. Let A and B two !-fix formulae and show that A⊗B and A⊕B are !-fix.
   3. Let A,B,C,D be arbitrary formulae and A^⊥, B^⊥, C^⊥, D^⊥ their respective negations (written with an overline in class). Give two terms in the calculus MALL_p^η typable with the sequent (⊢A⊗B^⊥,B⊗C^⊥,C⊗D^⊥,D⅋A^⊥), that are distinct modulo →RE-convertibility (you do not need to justify that they are distinct). Give proof nets corresponding to their respective derivations. Show that the two terms of MALL_p^η are convertible into one another assuming the depolarisation equation.