## Untyped Lambda Calculus #3 :: 17-03-2019

Contents

-Untyped Lambda Calculus in JavaScript

-Parser

@Semantics

-Evaluation

-Testing

-Usage

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.