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 [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 23: | Line 23: | ||
Untyped lambda expressions are given by following grammar: | Untyped lambda expressions are given by following grammar: | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
T ::= v \mid \lambda v.T \mid T\, T \\ | T ::= v \mid \lambda v.T \mid T\, T \\ | ||
v ::= v_1 \mid v_2 \mid ... | v ::= v_1 \mid v_2 \mid ... | ||
- | \end{array}\] | + | \end{array}\end{equation*} |
That is, an expression is a variable, a lambda expression defining a function, or an application of one expression to another. | That is, an expression is a variable, a lambda expression defining a function, or an application of one expression to another. | ||
+ | |||
+ | |||
===== Beta reduction ===== | ===== Beta reduction ===== | ||
Line 33: | 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\limits^{\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 ===== | ||
Let $\omega$ denote term | Let $\omega$ denote term | ||
- | \[ | + | \begin{equation*} |
(\lambda x.xx)(\lambda x.xx) | (\lambda x.xx)(\lambda x.xx) | ||
- | \] | + | \end{equation*} |
Note that $\omega$ beta reduces to itself. It represents infinite loop. | Note that $\omega$ beta reduces to itself. It represents infinite loop. | ||
Note that the set of total functions is not a model of untyped lambda calculus. Consider the self-application expression $x x$. Suppose the interpretation of variable $x$ ranges over a domain $D$. This domain should be a set of total functions $f : A \to B$ to enable application. But all possible values of $x$ are an argument, so we have that | Note that the set of total functions is not a model of untyped lambda calculus. Consider the self-application expression $x x$. Suppose the interpretation of variable $x$ ranges over a domain $D$. This domain should be a set of total functions $f : A \to B$ to enable application. But all possible values of $x$ are an argument, so we have that | ||
- | \[ | + | \begin{equation*} |
D = [D \to D] | D = [D \to D] | ||
- | \] | + | \end{equation*} |
that is, the set $D$ is equal to the set of all functions from $D$ to $D$. But this is not possible in set theory, because we can prove that the set $D^D$ has larger cardinality (even if it is infinite). For example, if $D$ is the set of natural numbers (which is countably infinite), then $D^D$ would be uncountably infinite. | that is, the set $D$ is equal to the set of all functions from $D$ to $D$. But this is not possible in set theory, because we can prove that the set $D^D$ has larger cardinality (even if it is infinite). For example, if $D$ is the set of natural numbers (which is countably infinite), then $D^D$ would be uncountably infinite. | ||