# Can all linear lambda calculi be linearity checked syntactically?

Given a lambda calculus with explicit linearity and usual application and abstraction, can the linearity check be done on an untyped syntax tree if we keep track of the structural types? Are the explicit operators necessary?

I suspect the answer is yes, from these course notes by Frank Pfenning because syntactic constructs are needed to use $A \& B$, $A \otimes B$, and $A \oplus B$.

However, if named functions exist (as in an actual programming language), some types are clearly necessary: consider the function $cond \colon Bool \to A \& A \multimap A$.

Can type checking and linearity checking be done in two steps, and can linearity checking happen before type checking?

Edit: The algorithm provided in the above course notes type checks linear lambda calculus terms, which includes determining if the term is linearly well-formed. Is it possible to determine if a term is well-typed via a syntactic linear well-formedness check (which would eliminate $\lambda x. x x$) followed by a type check which does not consider linearity? Or is this interaction essential to complete type inference?

• I do not understand the question. – Andrej Bauer Jul 8 '15 at 16:09
• @AndrejBauer I have added a clarification – Gus O'Hanley Jul 8 '15 at 16:21
• Are you asking whether the linear $\lambda$-calculus can be checked by checking the intuitionistic $\lambda$-calculus types and then checking syntactically the linearity condition? – Andrej Bauer Jul 8 '15 at 21:57
• Yes, that is my question. – Gus O'Hanley Jul 8 '15 at 23:02

I don't want to make a statement about "all linear lambda calculi" since it's hard to make that precise, but for pure linear lambda-calculus the answer is yes. One way to enforce linearity in pure lambda calculus is by trying to type application and abstraction using the linear implication $A \multimap B$, $$\frac{\Gamma \vdash t:A\multimap B\quad \Delta\vdash u:A}{\Gamma,\Delta\vdash t(u):B} \qquad \frac{x:A,\Gamma \vdash t:B}{\Gamma\vdash \lambda x.t:A\multimap B}$$ together with the linear identity and exchange rules: $$\frac{}{x:A\vdash x:A} \qquad \frac{\Gamma,y:B,x:A,\Delta \vdash t:C}{\Gamma,x:A,y:B,\Delta \vdash t:C}$$
But if you just want to check that a lambda term is linear, types are overkill, and it suffices to check syntactically that every free or $\lambda$-bound variable is used exactly once.
A way to make that a bit more precise is to define the set of linear lambda terms $\Lambda_1(\gamma)$ with a given list $\gamma = x_i,\dots,x_1$ of distinct free variables. This is really a family of sets (indexed by $\gamma$) generated by the following rules (which can be seen as an abstraction of the typing rules above): $$\frac{}{x \in \Lambda_1(x)} \qquad \frac{t \in \Lambda_1(\gamma,y,x,\delta)}{t \in \Lambda_1(\gamma,x,y,\delta)} \qquad \frac{t\in \Lambda_1(\gamma)\quad u \in \Lambda_1(\delta)}{t(u) \in \Lambda_1(\gamma,\delta)} \qquad \frac{t \in \Lambda_1(x,\gamma)}{\lambda x.t \in \Lambda_1(\gamma)}$$ Then a term $t$ of pure lambda calculus with free variables $\gamma$ is linear just in case $t \in \Lambda_1(\gamma)$. Note that these rules (like the typing rules) also have the effect of performing scope checking, and thus ruling out certain syntactic expressions which might look linear but violate scoping (e.g., an expression like "$\lambda x.x(y)(\lambda y.\lambda z.z)$", where the variable $y$ is used before it is bound).
Finally, pure linear lambda calculus has the remarkable property that every term is typable (which is related to the fact that it is strongly normalizing). So, once we know that a lambda term is linear it is always possible to go back and give it a type. Even more remarkably, the principal type of a term uniquely identifies its $\beta$-normal form, so type inference is in fact equivalent to normalization. Harry Mairson had a nice paper discussing some aspects of these remarkable properties in Linear lambda calculus and PTIME-completeness (JFP 14:6, 2004).