Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

Here's something from Slonneger's "Syntax and Semantics of Programming Languages":

A variable may occur both bound and free in the same lambda expression: for example, in λx.yλy.yx the first occurrence of y is free and the other two are bound.

I assume the free variable is the y right after the λx. and the bound y's are the λy.y which I can sort of intuitively grasp. So ((λx.yλy.yx)a)b) would reduce to (yλy.ya)b) then to bba ? Can someone explain how this came to be? In the end it's the expression b twice. Can someone perhaps provide more examples of bound and free variables?

share|improve this question
add comment

1 Answer

You correctly identified the first y as the free variable. Basically lambda abstractions define a scope for their bound variables. The scope overrides any other uses of the same variable names, so the same variable name can be used several times in different abstractions or as free variable.

(y(λy.ya))b can not be reduced any further. Unbound variables will never be substituted in a beta reduction.

If it was (y(λy.ya)b) you could reduce to y(ba).

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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