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:31] vkuncak |
sav08:untyped_lambda_calculus [2009/03/05 12:47] vkuncak |
||
|---|---|---|---|
| Line 7: | Line 7: | ||
| ===== Intuition ===== | ===== Intuition ===== | ||
| - | A function which takes its argument and increments it by 2 is given by lambda expression $\lambda x.x+2$. The $\lambda$ operator is a binder used to indicate that a variable is to be treated as an argument of a function. We indicate function application by juxtaposition. Here are some example expressions and their values: | + | A function which takes its argument and increments it by 2 is given by lambda expression $\lambda x.\, x+2$. The $\lambda$ operator is a binder used to indicate that a variable is to be treated as an argument of a function. We indicate function application by juxtaposition. Here are some example expressions and their values: |
| \begin{eqnarray*} | \begin{eqnarray*} | ||
| - | (\lambda x. x + 2)\, 7 &=& 9 \\ | + | (\lambda x.\, x + 2)\, 7 &=& 9 \\ |
| - | ((\lambda x. (\lambda y. x - y))\, 5)\, 3 &=& (\lambda y. 5 - y) 3 = 5 - 3 = 2 \\ | + | ((\lambda x.\, (\lambda y.\, x - y))\, 5)\, 3 &=& (\lambda y.\, 5 - y) 3 = 5 - 3 = 2 \\ |
| - | (((\lambda f. (\lambda x. f(f x))) (\lambda y. y^2))) 3 &=& (\lambda x. (\lambda y. y^2) ((\lambda y.y^2) x))) 3 = (\lambda y. y^2) ((\lambda y.y^2) 3) = (\lambda y.y^2) 9 = 81 | + | (((\lambda f.\, (\lambda x.\, f(f x))) (\lambda y.\, y^2))) 3 &=& (\lambda x.\, (\lambda y.\, y^2) ((\lambda y.\, y^2) x))) 3 = (\lambda y.\, y^2) ((\lambda y.\, y^2) 3) = (\lambda y.\, y^2) 9 = 81 |
| \end{eqnarray*} | \end{eqnarray*} | ||
| 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 = 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 ===== | ||