Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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.
  
 
sav08/untyped_lambda_calculus.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice