Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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