• English only

# Differences

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

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.
+

Line 37: Line 38:
\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.