Semantics

Semantically the λ-calculus can do substitutions and not much more. For some term $ t $ we write $ [x \rightarrow a] t $ meaning that we substitute all bound occurrences of $ x $ in $ t $ with the term $ a $. A variable, $ x $, becomes bound when $ \lambda $ is placed in front of it. Thus we bind values when using them as arguments. Say we have $$ \lambda x . \lambda y . x\ a\ b\ c $$ in this expression $ x $ and $ y $ are bound from the $ \lambda $ in front of them and to the end of the scope they appear in, that is the whole expression. $ a $, $ b $ and $ c $, however are not bound. We say that not bound variables are free. Since syntactically application binds tighter than abstractions, we have to place parentheses around an abstraction to end the scope, ex. $$ (\lambda x . \lambda y . x\ a\ b)\ x\ y $$ In this expression the rightmost $ x $ and $ y $ are outside the scope of any bindings and are thus free. So are $ a $ and $ b $. If no free variables are present in a term, we say that this term is closed, we call it a combinator.

So evaluation of an λ-calculus expression consists of substituting what is applied to abstraction until no more applications can be performed. We call each successful application a reduction. Expressions that can be reduced, are called a redex, and the action of successful application is called beta-reduction. In general when some expression is fully reduced we say that it is in normal form.

Scope Notation

With a mix of notation from TaPL and other literature we denote a scope as $ \rho $. We update $\rho$ using the same notation as for substitution. Say we want some scope in which $ a $ maps to $ \lambda x . x $ and $ b $ maps to $ fls $. To update $ \rho $ accordingly we write $$ \rho [a \mapsto \lambda x . x , b \mapsto fls ] $$ Now, for this implementation $ \rho $ is always empty, so content rely on updates. This has nothing to do with how you write programs in the lambda calculus. It is just notation. After successful evaluation I have noted the scope, empty or not, as given above.