Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
a:models_of_computation:lambda_calculus [2024/02/18 20:16] – removed - external edit (Unknown date) 127.0.0.1a:models_of_computation:lambda_calculus [2024/02/18 20:16] (current) – ↷ Page name changed from a:models_of_computation:lambda-calculus to a:models_of_computation:lambda_calculus charles
Line 1: Line 1:
 +====== Lambda Calculus ======
 +
 +The lambda calculus is a family of computational models that represent computation via expression reduction. 
 +Most variants of the lambda calculus utilize [[a:Type Theory:type checking]] to ensure the validity of lambda expressions.
 +Lambda Calculus is the primary foundation of modern [[a:Formal Verification]].
 +
 +===== Untyped Lambda Calculus =====
 +
 +Untyped Lambda Calculus is the original form of the lambda calculus proposed by [[b:Alonzo Church]] in his 1936 paper [[c:An Unsolvable Problem of Elementary Number Theory]].
 +
 +An expression is given by the following [[a:grammar]]:
 +$$ e := v \mid \lambda v . e \mid e_1\ e_2 $$
 +These rules are described as: "An expression may either be a variable name $v$, a lambda function with argument $v$ and expression $e$, or an application of an expression $e_1$ to argument $e_2$."
 +
 +The reduction of expressions can be summarized in one [[a:semantics|operational semantic]] rule:
 +\begin{align}
 +    \frac{}{(\lambda v. e_1)(e_2) \Downarrow e_1[e_2 / v] }
 +\end{align}
 +This rule can be described as "The application of a lambda expression $\lambda v . e_1$ to another expression $e_2$ is defined as replacing all occurrences of $v$ in $e_1$ with $e_2$ via [[a:capture-avoiding substitution]]." 
 +Some rule sets include additional rules, but these are generally abstractions to improve the usability of the untyped calculus.
 +This page will implicitly use some of these rules, such as allowing reduction inside of a lambda expression.
 +To introduce convenient notation we can colloquially say that $e_1 \rightarrow e_2$ means that "$e_1$ [[a:Models of Computation:unsoundness|eventually reduces to]] $e_2$."
 +
 +An example of expression reduction using this rule:
 +\begin{align}
 +    (\lambda x . x (\lambda y . y)) & (\lambda w . w w) \\
 +    (\lambda w . w w) & (\lambda y . y) \\
 +    (\lambda y . y) & (\lambda y . y) \\
 +    (\lambda y &. y)
 +\end{align}
 +
 +ULC is a [[a:Models of Computation:Turing Completeness|Turing-Complete]] model of computation[([[c:Computability and λ-Definability]])]. 
 +A common example of the expressiveness of ULC is the implementation of [[a:Church Numerals]], an encoding for the natural numbers:
 +\begin{align}
 +    \bold{0} &:= \lambda f . \lambda x . x \\
 +    \bold{S} &:= \lambda n . \lambda f . \lambda x . f (n f x)\ (\textrm{the successor function}) \\
 +    \bold{plus} &:= \lambda n . \lambda m . (n\ \bold{S}) m \\
 +    \bold{mult} &:= \lambda n . \lambda m . m\ (\bold{add} n) 0 \\
 +    \bold{pred} &:= \lambda n. \lambda f. \lambda x. n (\lambda g. \lambda h. h (g f)) (\lambda u.x) (\lambda u.u) \\
 +\end{align}
 +
 +Some example reductions using Church numeral encoding, unfolding each definition as it is reduced:
 +\begin{align}
 +    2 + 3 &:= \bold{plus}\ (\bold{S} (\bold{S}\ \bold{0}))\ (\bold{S} (\bold{S} (\bold{S}\ \bold{0}))) \\
 +    &:= (\lambda n . \lambda m . (n\ \bold{S}) m)\ (\bold{S} (\bold{S}\ \bold{0}))\ (\bold{S} (\bold{S} (\bold{S}\ \bold{0}))) \\
 +    &:= (\lambda m . ((\bold{S} (\bold{S}\ \bold{0}))\ \bold{S}) m)\ (\bold{S} (\bold{S} (\bold{S}\ \bold{0}))) \\
 +    &:= ((\bold{S} (\bold{S}\ \bold{0}))\ \bold{S})\ (\bold{S} (\bold{S} (\bold{S}\ \bold{0}))) \\
 +    &:= ((\lambda f . \lambda x . f (f x))\ \bold{S})\ (\bold{S} (\bold{S} (\bold{S}\ \bold{0}))) \\
 +    &:= (\lambda x . \bold{S} (\bold{S} x))\ (\bold{S} (\bold{S} (\bold{S}\ \bold{0}))) \\
 +    &:= \bold{S} (\bold{S} (\bold{S} (\bold{S} (\bold{S}\ \bold{0})))) \\
 +    &:= 5
 +\end{align}
 +
 +Additionally, we can implement [[a:boolean|booleans]]:
 +\begin{align}
 +    \bold{true} &:= \lambda t . \lambda f . t \\
 +    \bold{false} &:= \lambda t . \lambda f . f \\
 +    \bold{if\ c\ then\ p\ else\ n} &:= \lambda c . \lambda p . \lambda n . c\ p\ n \\
 +    \bold{and} &:= \lambda b_1 . \lambda b_2 . \bold{if}\ b_1\ \bold{then}\ (\bold{if}\ b_2\ \bold{then\ true\ else\ false})\ \bold{else\ false} \\
 +    \bold{or} &:= \lambda b_1 . \lambda b_2 . \bold{if}\ b_1\ \bold{then\ true\ else}\ (\bold{if}\ b_2\ \bold{then\ true\ else\ false}) \\
 +    \bold{is\_zero} &:= \lambda n . n\ (\lambda x . \bold{false})\ \bold{true}
 +\end{align}
 +
 +And simple [[a:data structures|data structures]]:
 +\begin{align}
 +    &\underline{\bold{Pairs}} \\
 +    \bold{pair (x, y)} &:= \lambda x . \lambda y . \lambda k . k\ x\ y \\
 +    \bold{fst} &:= \lambda pair . pair (\lambda x . \lambda y . x) \\
 +    \bold{snd} &:= \lambda pair . pair (\lambda x . \lambda y . y) \\
 +    &\underline{\bold{Lists}} \\
 +    \bold{nil} &:= \bold{0} \\
 +    \bold{cons\ h\ tl} &:= \lambda h . \lambda tl . \bold{pair(} h \bold{,} tl \bold{)} \\
 +    \bold{hd} &:= \bold{fst} \\
 +    \bold{tl} &:= \bold{snd} 
 +\end{align}
 +
 +Even recursion using the [[a:Models of Computation:Combinator Calculus|Y Combinator]], useful because $\forall g,\ \bold{Y}\ g \rightarrow g\ (\bold{Y}\ g)$:
 +\begin{align}
 +    \bold{Y} &:= \lambda f . (\lambda x . f (x\ x))\ (\lambda x . f (x\ x)) \\
 +    \bold{factorial} &:= \bold{Y} (\lambda f. \lambda n. \bold{if}\ (\bold{is\_zero}\ n)\ \bold{then}\ 1\ \bold{else}\ (\bold{mult}\ n\ (f\ (\bold{pred}\ n))))
 +\end{align}
 +The key idea being shown in the factorial example is that previously, all of our functions made specific use of the structure of Church numerals to accomplish their goal, whereas the factorial shown using the Y combinator instead utilizes the properties of the combinator in order to achieve arbitrary recursion that can be terminated at will. 
 +Note that our loop body never calls a function called \bold{factorial}, only a function $f$ that is provided by the Y combinator in order to achieve recursion.
 +This can further be specialized to other forms of repetition, such as while loops.
 +
 +===== Simply-Typed Lambda Calculus ($\lambda_\rightarrow$) =====
 +
 +The simply-typed lambda calculus is a development of the untyped lambda calculus intended to avoid potential unsoundness in the evaluation of terms.
 +STLC was proposed by Alonzo Church in his 1940 paper [[c:A Formulation of the Simple Theory of Types]].
 +
 +STLC adds a set of types to the operational semantics of ULC, as well as a series of typing rules that are the foundation of [[a:type checking]].
 +The primary added type is the arrow type, denoted by $\rightarrow$. 
 +This type represents functions, which now accept arguments of a specific type and evaluate to an expression with a specific type.
 +It is also necessary to add a set of fundamental types which cannot be subdivided. 
 +Here I will use the standard $\texttt{unit}$ type, which essentially represents the fundamental computational object.
 +Observe the new grammar and semantics:
 +\begin{align}
 +    e &:= () \mid v \mid \lambda v : t . e \mid e_1\ e_2 \\
 +    t &:= t_1 \rightarrow t_2 \mid \texttt{unit}
 +\end{align}
 +\begin{gather}
 +    \frac{}{\Gamma () : \texttt{unit} } (1) \\
 +    \frac{\Gamma e : t_2}{\Gamma (\lambda v : t_1 . e) : t_1 \rightarrow t_2} (2) \\
 +    \frac{\Gamma e_1 : t_1 \rightarrow t_2 \hspace{2em} \Gamma e_2 : t_1}{\Gamma (e_1\ e_2) : t_2} (3) \\
 +    \frac{\Gamma e_2 : t}{(\lambda v : t. e_1)(e_2) \Downarrow e_1[e_2 / v] } (4) \\
 +\end{gather}
 +We can see that the single evaluation rule (4) is essentially the same, but it enforces that the input type of the function must match the type of the expression it is applied to.
 +This type enforcement is achieved via rules 1-3, which say that
 +  - The type of $()$ is $\texttt{unit}$
 +  - The type of a lambda function is its input type arrow the type of its expression
 +  - The type of an application expression is only valid if the left expression is an arrow type, and the entire expression's type is the output of that arrow type
 +
 +STLC's strength is also its greatest weakness - although its type system removes unsoundness from the language, it also removes the ability to loop indefinitely, encode arbitrary conditional statements, as well as a number of other important features. 
 +For example, an attempt to port the Y Combinator into STLC: 
 +\[\lambda f : \alpha . (\lambda x : \beta . f (x\ x))\ (\lambda x : \beta . f (x\ x))\] 
 +fails, because as each sub-lambda is [[c:Models of Computation:Lambda Equivalence|equivalent]], they must have the same type $\beta \rightarrow \gamma$ for some arbitrary type $\gamma$, but the left sub-lambda expects an argument of only type $\beta$. This result actually hints at the [[c:Models of Computation:normalization|strongly-normalizing]] property of STLC: all terms must reduce to terms with a finite type, implying that all evaluation must terminate, which prohibits arbitrary recursion, necessary to achieve Turing-completeness.
 +
 +STLC is the simplest corner of the [[Lambda Calculus#lambda cube|lambda cube]], explored in depth throughout this page.
 +
 +===== System F ($λ_2$) =====
 +
 +===== Lambda-P ($λ_P$) =====
 +
 +===== System F$\underline{\omega}$ ($λ_\underline{ω}$) =====
 +
 +===== Lambda Cube =====
 +
 +The lambda cube is a structure that describes the combinations of typing features when applied to the simply-typed lambda calculus. 
 +STLC lies on the low, left, front corner of the cube. 
 +Directly above it lies System F with parametric polymorphism, to its right Lambda-P with dependent typing, and above it System F__ω__ with type constructors.
 +On the opposite corner lies the Calculus of Constructions, using the combination of each of these language features.
 +{{ :a:Models of Computation:1024px-lambda_cube_img.svg.png?400|}}
  

Trace:

Print/export
QR Code
QR Code Lambda Calculus (generated for current page)