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) $$

You are quite right in pointing out that the formal grammar in your book is not closed under $\beta$-reduction. Your modified grammar still has problems: $(\lambda x.x)(y)$ will reduce to $((y))$ according to the $\beta$-reduction rule, but $((y))$ isn't a valid $\lambda$-term. The correct view on this is that the parentheses show how the subterms are grouped but are to be ignored otherwise. I don't know of a reference that gets this right when formulas are viewed as strings of atomic symbols (rather than tree structures). — Rob Arthan, Aug 01 '17 at 22:02

score 2 · Accepted Answer · answered Aug 02 '17 at 05:20

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".

Are common lambda calculus notation conventions sloppy?

1 Answers1