I am thinking that many example only takes free variable with one occurrence, such as $(\lambda x.x )y$ where $y$ is free.

can we say $y y $ is a $\lambda$-term and two $y$ are same free variable? I did not see such examples so far, just wondering.


A possible definition (From Lambda-Calculus and Combinators):

Definition 1.11 (Free and bound variables) An occurrence of a variable $x$ in a term $P$ is called:

  • bound if it is in the scope of a $\lambda x$ in $P$

  • bound and binding, iff it is the $x$ in $\lambda x$

  • free otherwise

Let's define the set of free variables $FV$:

  • The free variables of $x$ are just $x$, that is $FV(x) = \{x\}$
  • $FV(\lambda x. P) = FV(P) \setminus \{x\}$ (since $x$ is bound)
  • $FV(st) = FV(s) \cup FV(t) $

And maybe you just need some examples:

  • $y$ is free in $y$

  • $x$ is free in $(\lambda x.x)x$ (Try to work out why)

  • $y$ is free in $(yy)$.

  • 1
    $\begingroup$ so I am right is that a single free variable could have many occurrences, such as $yyyyy$ with a single free variable $y$. Thank you! $\endgroup$ – alim Jan 27 '17 at 2:10
  • 1
    $\begingroup$ Yes, since $yyyyyy$ is just $((((yy)y)y)y)$. Which makes $FV(yyyyyy) = \{y\}$. $\endgroup$ – Aristu Jan 28 '17 at 0:47

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.