- English only

# Lab for Automated Reasoning and Analysis LARA

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