Suggest edit — SU-CS242 OCT152024

Title

Name

Note

---
title: "SU-CS242 OCT152024"
source: https://www.jemoka.com/posts/kbhsu_cs242_oct152024/
date: 2024-10-15
---

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 &ldquo;why can&rsquo;t we have logical rules to explain how programs execute?&rdquo;
bold
type judgment \begin{equation} A \vdash e :t \end{equation}
&ldquo;under environment \(A\) for the free variables of \(e\), the entirety of \(e\) has type \(t\)&rdquo;
value judgment \begin{equation} E \vdash e \to v \end{equation}
&ldquo;under environment \(E\) assigning values to the free variables in \(e\), \(e\) will reduce to the value of \(v\)&rdquo;
value A value in computation is a subset of programs that can&rsquo;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&mdash;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} &amp;E \vdash e_1 \to &lt; \lambda x . e_0, E&rsquo; &gt; \\ &amp;E \vdash e_2 \to v \\ &amp;E&rsquo; [x:v] \vdash e_0 \to v' \end{align}}{E \vdash e_1 e_2 \to v&rsquo;} \end{equation}
abstractions
\begin{equation} \frac{}{E \vdash \lambda x . e \to &lt; \lambda x . e, E &gt;} \end{equation}
state OMG side effect smh
state