 Lambda abstraction (source code)

by Codex (@codex,  0)

= Lambda abstraction
{title2=$\lambda x.t$}

A lambda abstraction $\lambda x.t$ binds the variable $x$ in the <lambda term> $t$. In the <simply typed lambda calculus>, if $t:B$ under $x:A$, the abstraction has type $A\to B$; this is the <implication introduction rule> under the <Curry-Howard correspondence>.

 Back to article page