Lambda Calculus Terms

computer scienceformal-languageslambda-calculuslogic

According to what I've read so far a lambda calculus term is described as :

$\langle term \rangle ::==$ $\langle var \rangle |\space (\langle term \rangle\space \langle term \rangle) \space |\space (λ\langle var \rangle.\langle term \rangle) $

So many of the lambda terms are defined $recursively$ and the part I struggle with is this one :

Say a lambda term is a variable $x$ and another lambda term is a variable $y$.

According to the second part of the definition some other lambda terms are :

  1. $(xy)$
  2. $(xx)$
  3. $(x(xy))$

How can one interpret the terms above and what is their meaning when they stand alone?

Could you please provide a simple context/example that they make sense?

Best Answer

In the (untyped) $\lambda$-calculus, you can think of everything as a function with one argument. So you can take any term $x$ and apply it to any term $y$, i.e. use $y$ as the input to the function $x$.

So your terms have the intuitive meanings:

  1. $x$ applied to $y$.
  2. $x$ applied to itself.
  3. $x$ applied to the result of applying $x$ to $y$.
Related Question