According to wikipedia:

  • a variable, $x$, is itself a valid lambda term
  • if $t$ is a lambda term, and $x$ is a variable, then $(λ x . t )$ is a lambda term (called a lambda abstraction);
  • if $t$ and $s$ are lambda terms, then ( $t$ $s$ ) ($ts$) is a lambda term (called an application).

How can $\lambda x.x^2$ be a valid lambda term if $x^2$ is not, as it is not a variable and is neither an abstraction nor an application?


I don't know the actual context, but it appears that this is syntactic sugar.

I would interpret it as $$\lambda x.\ \mathrm{m}\ x\ x$$ where $\mathrm{m}$ stands for the multiplication operation in context (or $\lambda x.\ \mathrm{p}\ x\ 2$ where $\mathrm{p}$ is the power opertion and $2$ stands for the term corresponding to numeral $2$).

Please note, that we use syntactic sugar often and pure lambda calculus is rather rare, e.g., $$\mathrm{let}\ i = \lambda x.\ x\ \mathtt{in}\ i\ \ i$$ and $$i\ i\ \mathrm{where}\ i = \lambda x.\ x$$ both actually stand for $$ (\lambda i.\ i\ i)\ (\lambda x.\ x) $$ which is a way harder to read. It is quite inconvienient to use just pure lambda calculus.

Other than that, sometimes lambda calculus gets extended, but then the context should specify how we are to interpret such extensions.

I hope this helps $\ddot\smile$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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