Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:untyped_lambda_calculus [2009/03/05 12:45] vkuncak |
sav08:untyped_lambda_calculus [2009/03/05 12:47] vkuncak |
||
---|---|---|---|
Line 35: | Line 35: | ||
The main rule of lambda calculus is beta reduction, which formalizes function application: | The main rule of lambda calculus is beta reduction, which formalizes function application: | ||
\begin{equation*} | \begin{equation*} | ||
- | (\lambda x.\, s) t\ \to^{\beta}\ s[x:=t] | + | (\lambda x.\, s) t\ \mathop{\to}\limits^{\beta}\ s[x:=t] |
\end{equation*} | \end{equation*} | ||
where we assume capture-avoiding substitution. In general, we identify terms that differ only by renaming of fresh bound variables. | where we assume capture-avoiding substitution. In general, we identify terms that differ only by renaming of fresh bound variables. | ||
- | + | Here $\mathop{\to}\limits^{\beta}$ is a binary 'reduction' relation on terms. We build larger relations on terms by | |
- | + | - performing reduction in any context $C$, so we have $C[(\lambda x.\, s) t]\ \mathop{\to}\limits^{\beta}\ C[s[x:=t]]$ | |
- | + | - taking its transitive closure: computes all terms reachable by reduction | |
- | + | ||
- | + | ||
===== Non-termination and Difficulties with Semantics ===== | ===== Non-termination and Difficulties with Semantics ===== |