Are common lambda calculus notation conventions sloppy?

Question

I am supposing that the definition of a $\lambda$-term $(\Lambda)$ in the book 'Type Theory and Formal Proof: An Introduction' is a common one. In short grammar we have, with $V$ being a variable:

$$ \Lambda: V|(\Lambda\Lambda)|(\lambda V. \Lambda) $$

The problem I am worried about manifests itself when doing $\beta$-reduction of $(x((\lambda y.y)z))$ which is a proper term without any notational convenience:

\begin{align} & \;\; (^{^1}x(^{^2}(^{^3}\lambda y.y)^{^3}z)^{^2})^{^1} \\ \to_\beta & \;\; (^{^1}x(^{^2}z)^{^2})^{^1} \\ \end{align}

But now notice that according to the grammar, this is not a valid term. The valid term we think of when we see this is $ (xz) $ formed by grammar rule 2 from two variables with no parenthesis around each as in rule 1. Instead we have $ (x(z)) $ but this cannot be a valid term because according to the grammar, $(z)$ is not a term, but only $z$ is.

Is the book simply sloppy in its grammar definition? Should single-variable terms also require parentheses to be fully correct? This would amount to the following modified grammar:

$$ \Lambda: (^{!}V)^{!}|(\Lambda\Lambda)|(\lambda V. \Lambda) $$

Answer 1

As Rob Arthan stated, you are correct that the grammars provided do not accurately and precisely capture the concrete syntax of the lambda calculus. That's because they are not intended to. A statement like $\Lambda ::= V \mid (\Lambda \Lambda) \mid (\lambda V.\Lambda)$ is intended to be a declaration of abstract syntax. It is very much akin to a data declaration in a language like Haskell, ML, or Agda. For example, in Haskell syntax it might look like: data Exp = Var V | Abs Exp Exp | Lam V Exp. Many tools that are closer to specification than programming such as Agda, Coq, or the $\mathbb{K}$ Framework allow much more syntactic flexibility for a comparable investment of effort. For example, in the $\mathbb{K}$ Framework the following declaration captures some of the common conventions for lambda notation and produces a working parser:

syntax L ::= Id
           | L L          [left]
           | "(" L ")"    [bracket]
           > "λ" Id "." L

This correctly parses "λx.λy.x y y" and further produces the exact same AST for "λx.λy.((x y y))". My point with this is most work indicates the abstract syntax as that's what a semantics operates over. Obviously, at the end of the day they have to use some concrete syntax even to write down the abstract syntax. The precise details are rarely spelled out in anything other than descriptions of machine implementations. The details are usually tedious, unimportant, and, as the above demonstrates, largely mechanically derivable given a bit of additional information beyond the context-free grammar. Nevertheless, for me "formal" = "machine-checked"; everything else is informal no matter how detailed. In that vein, here's a complete executable formalization of beta reduction in $\mathbb{K}$:

require "substitution.k"
module LAM
    imports SUBSTITUTION
    syntax L ::= Id
               | L L          [left]
               | "(" L ")"    [bracket]
               > "^" Id "." L [binder]

    syntax KVariable ::= Id

    rule (^ X:Id . M:L) N:L => M[N / X] [anywhere]
endmodule

where I've replaced λ with ^ because while the generated parser doesn't have an issue with the Unicode, the rewrite engine does. This correctly reduces "^y.(^x.^y.x y)y" to "^ y . ^ _1 . y _1" where the inner "y" has been alpha-renamed to "_1". Of course, all the real work of this definition has been hidden away in the predefined SUBSTITUTION module. At any rate, as the tooling advances, there's less and less reason not to formalize these sorts of things in my sense of "formalize".