SU-CS242 OCT152024

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
state