LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:untyped_lambda_calculus [2009/03/05 12:47]
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 46: Line 46:
  
 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.