Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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.
  
 
lambda_calculus.txt · Last modified: 2015/04/21 17:32 (external edit)