Differences

This shows you the differences between two versions of the page.

--- sav08:untyped_lambda_calculus [2009/03/05 12:31]
vkuncak
+++ sav08:untyped_lambda_calculus [2009/03/05 12:45]
vkuncak
@@ Line 7: / Line 7: @@
 ===== 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*}
-  (\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*}
@@ Line 35: / Line 35: @@
 The main rule of lambda calculus is beta reduction, which formalizes function application:
 \begin{equation*}
-  (\lambda x. s) t = s[x:=t]
+  (\lambda x.\, s) t\ \to^{\beta}\ s[x:=t]
 \end{equation*}
 where we assume capture-avoiding substitution.  In general, we identify terms that differ only by renaming of fresh bound variables.