Lambda Calculus, review
Grammar:
\begin{equation} e \to (x | \lambda x.e | e e) \end{equation}
and beta reductions:
\begin{equation} (\lambda x . e_1) e_2 \to e_1 [x := e_2] \end{equation}
structural operational semantics
“why can’t we have logical rules to explain how programs execute?”
bold
type judgment
\begin{equation} A \vdash e :t \end{equation}
“under environment \(A\) for the free variables of \(e\), the entirety of \(e\) has type \(t\)”
value judgment
\begin{equation} E \vdash e \to v \end{equation}
“under environment \(E\) assigning values to the free variables in \(e\), \(e\) will reduce to the value of \(v\)”
value
A value in computation is a subset of programs that can’t be further reduced. In particular, some pure lambda abstraction \(\lambda x . e\) is a value.
value judgment evaluations
Under a call-by-value scheme—we will first reduce function arguments.
variables
\begin{equation} \frac{}{E \vdash x \to E(x)} \end{equation}
(i.e. the value of a variable can just be looked up)
integer
\begin{equation} \frac{}{E \vdash i \to i} \end{equation}
application
\begin{equation} \frac{\begin{align} &E \vdash e_1 \to < \lambda x . e_0, E’ > \\ &E \vdash e_2 \to v \\ &E’ [x:v] \vdash e_0 \to v' \end{align}}{E \vdash e_1 e_2 \to v’} \end{equation}
abstractions
\begin{equation} \frac{}{E \vdash \lambda x . e \to < \lambda x . e, E >} \end{equation}
state
OMG side effect smh