• 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) Both sides previous revision Previous revision 2009/03/05 12:47 vkuncak 2009/03/05 12:45 vkuncak 2009/03/05 12:45 vkuncak 2009/03/05 12:45 vkuncak 2009/03/05 12:44 vkuncak 2009/03/05 12:31 vkuncak 2008/05/27 20:42 vkuncak 2008/05/27 20:40 vkuncak 2008/05/27 20:39 vkuncak 2008/05/27 20:27 vkuncak 2008/05/27 20:12 vkuncak 2008/05/27 19:50 vkuncak 2008/05/27 17:44 vkuncak 2008/05/27 15:55 vkuncak 2008/05/27 15:54 vkuncak 2008/05/27 15:52 vkuncak 2008/05/27 15:51 vkuncak created Next revision Previous revision 2009/03/05 12:47 vkuncak 2009/03/05 12:45 vkuncak 2009/03/05 12:45 vkuncak 2009/03/05 12:45 vkuncak 2009/03/05 12:44 vkuncak 2009/03/05 12:31 vkuncak 2008/05/27 20:42 vkuncak 2008/05/27 20:40 vkuncak 2008/05/27 20:39 vkuncak 2008/05/27 20:27 vkuncak 2008/05/27 20:12 vkuncak 2008/05/27 19:50 vkuncak 2008/05/27 17:44 vkuncak 2008/05/27 15:55 vkuncak 2008/05/27 15:54 vkuncak 2008/05/27 15:52 vkuncak 2008/05/27 15:51 vkuncak created 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.