Lambda the Ultimate

Are those slides and notes available?

Besides that, I have a truly ridiculous question. What makes linear / affine types linear / affine? That is, what, if anything, is the connection between the types (or, I suppose one should ask, the underlying logics) and linear algebra?

From Wikipedia:

1. Linear type systems (allow exchange, not weakening or contraction): Every variable is used exactly once.
2. Affine type systems (allow exchange and weakening, not contraction): Every variable is used at most once.
3. Relevant type systems (allow exchange and contraction, not weakening): Every variable is used at least once.
4. Ordered type systems (discard exchange, contraction and weakening): Every variable is used exactly once in the order it was introduced.

These are simple checks on the term which you can (also) push to the type system. For instance, a variable with linear type !Int can be used only once so simply flagging usage in the context should be enough.

In a linear type system variable -or resource- usage is enforced by the type system, in a linear logic, variable usage is enforced by the logic. AFAIK.

I don't remember details from Clean but I imagine it isn't enforcing linearity which is the big problem but using that property. For instance, by reclaiming a piece of used memory of given size.

Thanks for replying, but I don't mean "what is the definition?" but rather "why is that the name attached to this concept?" That is, is there any good mathematical reason (not just the purely historical one that Girard did it) to call it "linear logic" (which, to me, implies a connexion to linear algebra)?

Yes, there is such a connection: historical models of Linear Logic interpret its proofs as linear morphisms, i.e. functions preserving sums (or joins, in the order-theoretical setting). The link with linear algebra has been pushed much further by differential linear logic, but that is a very advanced subject IMO. I believe this preprint by Thomas Ehrhard is the best introduction to date.

Thank you! I see that Ehrhard mentions the fact about proofs as linear morphisms on p. 1, but do you happen to know a historical reference for this fact, that perhaps goes into more detail? (Also, the identification of “linear morphisms” as “functions preserving joins” makes me suspect that this is “linear algebra over ℤ”—i.e., that there is no particularly meaningful notion of scalar multiplication. Is that correct?)

I see that Ehrhard mentions the fact about proofs as linear morphisms on p. 1, but do you happen to know a historical reference for this fact, that perhaps goes into more detail?

I don't know of any standard reference (perhaps the paper gasche linked below?). Girard's normal functors paper, even if it is not striclty speaking about Linear Logic, might be the best place to start.

(Also, the identification of “linear morphisms” as “functions preserving joins” makes me suspect that this is “linear algebra over ℤ”—i.e., that there is no particularly meaningful notion of scalar multiplication. Is that correct?)

The first models of LL (Scott domains, dI domains, coherence spaces, etc.) were order-theoretical ones and thus had no notion of sum except for joins. But later "quantitative" models, starting I believe with Girard's normal functors, rely on more standard forms of sums. In particular, Ehrhard and his collaborators have built models of LL in various kinds of topological vector spaces, such as Köthe sequence spaces.

I imagine it is because formulas are treated as resources and their usage is tracked such they are used exactly once. Hence linear, you either copy between derivation steps or use a formula once.

I disagree with adrieng. I don't think there's a clear connection between linear logic and linear algebra, unless for some categorical link which I usually personally associate as something disgusting or a severe case of brain rot. No offense.

adrieng did not claim that there is a "clean" connection between linear logic and linear algebra, but that there is a connection that was understood by the people working on linear logic early on (models of linear logic where types are vector spaces and proofs are linear functions) and that this connection explains the name "linear" in "linear logic". As far as I know, this is perfectly correct, and it also accurately answers the question of the choice of naming. Neelk gave more details on the model, and adrieng above gave pointers to more advanced logics with stronger links to linear algebra.

There was no hint of any connection to linear algebra in the early papers, neither have I found anything on Wikipedia or any hint on a connection in Stanford's encyclopedia, and I don't even think the mentioned paper makes a strong connection with linear algebra.

Sorry, but I hate this kind of 'science'. It's just the same stuff as programmers knowing some correspondence between LC types as formulas, and then assuming that Java term and types somehow follow the same correspondence.

Notions like this should be crushed. Immediately. It's bad science.

There was no hint of any connection to linear algebra in the early papers

From Normal functors, power series and lambda-calculus (published 1988, communicated 1985 before the LL paper):

Added in print. It appears now (October 1986) that the main interest of the paper is the general analogy with linear algebra. The analogy brought in sight new operations, new connectives, thus leading to ‘linear logic’. The treatment of the sum of types (Appendix B) contains implicitly all the operations of linear logic. What has been found later is that the operations used here (e.g., linearization by means of ‘tensor algebra’) are of logical nature.

Well, there wasn't any hint of any relation in the sources I read, including Girard's own paper on linear logic. Rather, it was explained that he arrived at this result through careful examination of proof derivation in classical and intuitionistic logics.

But can't disagree with the horse's mouth, of course.

I still differ in that even Girard's inspiration is even that important. You can't simply switch between syntactic formalisms and linear algebra (which is somewhat informal from a logician's point of view) and then simply reason even over that with the sloppiest of all formalisms, category theory, to make a strong connection. A logician simply doesn't know what 'linear algebra' is supposed to be.

No. I agree Girard seemed to be inspired by linear algebra but the correspondence must be shallow. (As neelk also mentioned, there's some problem fitting these notions together I won't claim to understand.)

Thank you! This is a great historical pointer. Just to have a clickable link, I think that the Normal functors … paper you reference is at http://www.sciencedirect.com/science/article/pii/0168007288900255, and the cited passage is at the bottom of logical p. 131.

adrieng gave some historical pointers. For a formal development of Neelk's sketch below, see for example Logic and linear algebra: an introduction by Daniel Murfet, 2014. One thing that may make reading these work (same for descriptions of geometry of interaction, etc.) less obvious is the insistence on the categorical structure used to build the models (typically "symmetric monoidal category") rather than on specific algebraic structures -- it takes a bit of category-theory knowledge to be comfortable with the correspondence that is made between the categorical structures and the usual structures of linear algebra. But see "Denotation of formulas", Section 5.1 page 14.

You may be right in pointing out that the connection with linear algebra is only known to insiders of the field and not well-explained outside specialist territory. That does not justify insulting said specialists, especially when they (neelk, adrieng) come to you with specific information and guidance. Your behavior here remains distasteful.

Yah, and I give it to you that the original inspiration of Girard is omitted on purpose since logicians are well aware that it simply isn't that easy.

I don't mind your hobby, or even research -if any-, but one opens up a complete can of wurms trying to relate logic, any logic, with algebra, worse probably with a syntatic formalism and linear algebra.

Division by zero and a host of other problems relating to numerical stability? Equality? Maybe since it's only a model you can get away with it but you simply don't know very well what you're talking about. Soundness and completeness? Shown with a formalism where one doesn't know what equality is, whether notions of duality actually exist, where people in general have thrown the hope of arriving at something resembling an intuition -or, dare I say, model- out of the window?

At best you can relate some notion of linear algebra with some syntactic system resembling one of the linear logics developed with a substantial portion of hand waving.

And even if I accept that result I still see it as barking up the wrong tree. The hard work is in making a logic useful, proving various logical qualities, proving possible undecidability, exploring different invocations which might allow for efficient reasoning, deriving complexity results, finding an application domain, implementing some software.

You might find it interesting but I just can't be bothered with this kind of flutter.

Once usage is overkill. A code example "let x = y in if c then x else x" is linear in x, but x occurs twice. Linear means that the value is fetched once along the control path from the constructor: clearly this is correct above since provided c terminates, then exactly one of the two branches is taken.

So to make this work, you have to distribute the "once" over the "+" in a sum type (once in each branch). I have no idea what to do with products, I don't think it works. The reason is you can take a projection .. any projection .. of a product any time you want. To stop that we'd need a linear product, propagate the value to both components, but then insist exactly one projection is taken.

With exponentials it seems that if you move a resource to a the first argument of a function with arity two, the resource is not actually used until the application to the second argument, therefore the closure over the first argument must have an "execute once" type induced.

Linearity doesn't seem to fit well with functional programming but it seems to work much better with coroutines where the interpretation is that a read event must lead to a write event. In Felix this is a functional transducer. Filtering transducers are affine. If you connect a linear chip to an affine one, the result is affine.

Finite dimensional vector spaces are one of the standard models of classical linear logic.

Conjunctions A & B are interpreted by direct products.
Disjunctions A ⊕ B are interpreted by direct sums.
Tensor products A ⊗ B are interpreted by tensor products.
Linear negations ¬A are interpreted by dual spaces.

This is not quite a perfect match, since CLL doesn't give you syntax corresponding to the isomorphism of direct sums and products (ie, the biproduct structure). This is intentional, since Girard had more models in mind beyond vector spaces.

However, the tidiness of this interpretation went on to motivate a lot of Girard's work on the geometry of interaction (which he based on operator algebras).

I scanned Girard's early papers and it looks he wanted to solve a problem with classical and intuitionistic logic, didn't completely solve the original problem, stumbled onto a logic which could best be used to denote resource usage, and went on to look for other applications.

You can blow up a lot of syntactic formalisms to look for applications but those usually don't match well, are good for a few papers, and end up never to be read again after some niche has been explored.

As far as I am concerned, it's a resource logic until someone finds a good fit for something else.

Thanks very much; that's fascinating. However, I'm confused because the dual of a finite-dimensional vector space is non-canonically isomorphic to the original space, and the direct product and the direct sum of two finite-dimensional vector spaces are canonically isomorphic (via the canonical inclusion of the latter in the former). Is the logic unaffected by using isomorphic spaces for non-equivalent propositions?

Also, as a total non-expert on the subject—I'm literally just browsing Girard's paper—there seem to be more connectives in his initial list: negation isn't explicitly listed, but there are implication, a connective (whose name I don't know, but which he calls the “bilinear version of ‘or’”) ⅋, and two “exponential” connectives ! and ?. Do these fit nicely into the FDVS model?

The fact that the double-dual is canonically isomorphic to the original space corresponds to the classical rule of double-negation elimination, that ¬¬A is equivalent to A.

The non-canonical isomorphism between a space and its dual doesn't correspond to anything in linear logic. Basically, type operators are interpreted as functors, and the term formers all correspond to the natural transformations. Since the non-canonical isomorphism between a space and its dual isn't a natural isomorphism, you can't say it in CLL.

The multiplicative disjunction A ⅋ B (pronounced "A par B"), is equivalent to (A∗ ⊗ B∗)∗. You can think of this via de Morgan duality -- it's like defining "A or B" as not (not-A and not-B). Once you have par, the implication A ⊸ B can be defined the usual de Morgan way as ¬A ⅋ B (which boils down to (A ⊗ B∗)∗).

I've never looked into it, so I don't know how (or even if!) the exponential !A can be interpreted in finite-dimensional vector spaces -- adrieng might know, though.

I've never looked into it, so I don't know how (or even if!) the exponential !A can be interpreted in finite-dimensional vector spaces

I think that most models use infinite-dimensional vector spaces for that reason. Of course, this shifts the difficulty to the interpretation of linear negation. As far as I understand, this is generally accomplished by using a well designed orthogonality relation. Since this is a bit awkward from the mathematical point of view, people have also tried to find more natural settings; one example is Marie Kerjean's use of weak topologies.

Taking a step back, Filip, I feel like we are drifting to topics which are fascinating (to some people) but also quite unrelated to your original question. If you like to read about precise connections between proof theory and pure math, then that's great! But a deep understanding of Linear Logic is neither necessary nor sufficient to understand modern resource-aware type systems. I would rather follow gasche's advice in the opening comment, and then perhaps read François Pottier's slides about linear types, capabilities, and regions (discussed previously on LtU).

About an hour in it looks like he starts making small mistakes.

(EDIT: Finished. Not so bad. He misnames a derivation which was noted by the audience, made another small mistake which was also noted, and I think he had a consequent wrong. Not bad at all.)