Valid Lambda Expressions

Question

I have two questions about the validity of lambda expressions.

First, is a variable on its own a valid lambda expression (ex: λx)

Second, take for example these two lambda expressions (λx.fxya and λz.fxya). They're identical besides the fact that the bounded variable is different. Does this affect its validity?

Also, if these are all valid, is there a way to see some invalid lambda expressions so I can get an idea between what a valid and invalid one looks like?

Answer 1

It depends on what you mean by valid. Let's start with "syntactically valid". The definition of a valid lambda expression is inductive.

1. Any term is a valid lambda expression on its own. These are the atoms of our language, and for our purposes, we'll just say all of the lowercase letters are valid terms. But realistically, your terms could be whatever you choose, as long as you're consistent.
2. If α and β are two valid lambda expressions, then so is α β. We refer to this as the application of α to β.
3. If t is some term (as defined above) and α is any lambda expression, then λt. α is a valid lambda expression. We call this the abstraction of α over the term t.

By this definition, e is a valid lambda expression, since it's just a term. So is λf. f x, and so is a b c d e f. λ x, on its own, is not. It looks like the start of an abstraction but we never finished it, so it's just a nonsense sequence of letters. However, x on its own is an expression, and so is λx. x.

By this definition, λx. f x y a and λz. f x y a are both lambda expressions. Specifically, they're an abstraction of several applications of terms.

Now, for many purposes, we also want a lambda expression to have no free variables. A free variable is one that appears outside of any abstraction bindings for it. The opposite of a free variable is a bound variable. So in λx. f x y a, the x is bound (by the lambda abstraction), while f, y, and a are free. In λz. f x y a, all of f, x, y, and a are free. Having the unused z abstraction is perfectly acceptable.