When I was a master's student in Paris I was exposed to the following standard narrative: "J.-Y. Girard invented coherence spaces, then he noticed the decomposition $A \to B~=~!A \multimap B$ and that's how linear logic was born". But I've come across some conflicting information:

  • some people who have known Girard personally told me that he invented the normal functor / power series semantics of the λ-calculus first, and that's where he actually discovered linearity (corresponding to degree 1 monomials);

  • on the other hand, Girard's written quotes seem to indicate that linear logic indeed comes from coherence spaces, not from the interpretation of function types but from that of intuitionistic sum types as $A + B~=~!A \oplus !B$:

Linear logic first appeared after the author had been challenged by Berry and Curien to extend the coherent semantics (at the time: qualitative semantics) to the sum of types

(From Linear Logic (1987) section V)

It is this decomposition which is the origin of linear logic: the operations ⊕ (direct sum) and ! (linearisation) are in fact logical operations in their own right.

(From Proofs and Types chapter 12)

So what is the actual story here? (Is there any way to know?)

  • 5
    $\begingroup$ From Girard, I've always heard the second story you mention, on several occasions in talks and lectures. I had never heard the first version of the story until recently, from Thomas Seiller. Maybe you should ask him. I think it's quite possible that both are true: normal functors maybe exposed the notion of linearity but it wasn't until when he worked on the sum type in coherence spaces that Girard understood its importance and that it could be made into something systematic. $\endgroup$ Nov 11 at 6:13


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.