Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:untyped_lambda_calculus [2009/03/05 12:45] vkuncak |
sav08:untyped_lambda_calculus [2009/03/05 12:47] vkuncak |
||
|---|---|---|---|
| Line 28: | Line 28: | ||
| \end{array}\] | \end{array}\] | ||
| 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 ===== | ||