I have two questions about the validity of lambda expressions.

First, is a variable on it's 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 it's 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?


1 Answer 1


What do you call a valid λ-expression? This is not a standard concept.

Anyways, λ-expressions are the terms built inductively as follows:

  • given a fixed set $V$ of variables, all $x \in V$ are λ-expressions,
  • for any variable $x$ and λ-expression $M$, $λx.M$ is a λ-expression,
  • for any λ-expressions $M$ and $N$, $MN$ is a λ-expression.

Thus $λx$, which is of none of these forms, is not a λ-expression (not even an “invalid” one).

The two other expressions you give, $λx.fxya$ and $λz.fxya$, are not identical in any of the following meanings.

  • Strictly speaking, they are different (since the abstracted variable differs): they are not equal.
  • One often considers terms up to α-equivalence, i.e. up to renaming of bound variables. (You can look to any standard reference for details.) But in your example the bound variable $x$ is not replaced with $z$ in the body of the abstraction, so the two expressions are not α-equivalent.
    (Or equivalently, if you define λ-terms as α-equivalence classes of λ-expressions, the two λ-terms are not equal.)
  • 2
    $\begingroup$ The two last terms are not alpha equivalent, as the bound occurrence of x has not been renamed. $\endgroup$ Commented Oct 3, 2023 at 19:08
  • $\begingroup$ Oh yes sorry, I missed this. I correct my answer. $\endgroup$ Commented Oct 5, 2023 at 12:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.