Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
lambda_calculus [2007/05/28 21:18] vkuncak |
lambda_calculus [2015/04/21 17:32] (current) |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| Note: in Isabelle and Jahob notation we use '% x.F' or '\<lambda> x.F' to denote $\lambda$.F binder. In [[http://caml.inria.fr|ocaml]], one can use 'function x -> F', and in [[http://www.haskell.org|Haskell]] one can use '\ x -> F'. | Note: in Isabelle and Jahob notation we use '% x.F' or '\<lambda> x.F' to denote $\lambda$.F binder. In [[http://caml.inria.fr|ocaml]], one can use 'function x -> F', and in [[http://www.haskell.org|Haskell]] one can use '\ x -> F'. | ||
| + | |||
| ===== Lambda expressions ===== | ===== Lambda expressions ===== | ||
| Untyped lambda expressions are given by following grammar: | Untyped lambda expressions are given by following grammar: | ||
| - | \begin{equation*} | + | \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{equation*} | + | \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 43: | Line 44: | ||
| References: | References: | ||
| - | * Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984) | + | * Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984) ([[http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html|Chad Brown's notes on this book]]) |
| - | ([[http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html|Chad Brown's notes]]) | + | |