In short, my main confusion is between the two concept
I am reading this reference here:
The syntax of (pure) lambda expressions is defined as follows:
- A variable is a lambda expression (we will use single, lower-case letters for variables).
If M and N are lambda expressions, then so are each of the following:
We can express the rules given above that define the language of lambda expressions using a context-free grammar: exp → ID | ( exp ) | λ ID . exp // abstraction | exp exp // application
From rule #1 and the context-free grammar, I think the author means that
ID refers to
variable ∈ lambda expression. But I am not sure whether
lambda expression ∈ variable.
May I know whether I can use a "complex" expressions (e.g. a non-variable lambda expression) as
λid.M? Intuitively, I interpret
variable represented by an ID with a single letter, but I could not find reference to support my conjecture.
(or in other words, how is
variable defined in lambda calculus, if this is not too broad a question?)