Meeting 14 - Evaluation Order

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferrule}[3][]{ \let\and\qquad \begin{array}{@{}l@{}} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

What questions does your neighbor have?

Links

In-Class Slides
In-Class Jupyter
Book Chapter

Announcements

• Lab 3 due Tuesday 6pm
• Accelerated section enrollment
• Passive lecture vs. active learning format

Today

• Evaluation Order (mini-lecture)
• Preview Lab 3
• Triage Your Questions
  • Lab 3?

Questions?

• Preview:
  • What is evaluation order and short-circuit evaluation?

Questions?

Evaluation

Consider generic binary operator # and $. What does

1 # 2 # 3 $ 4

evaluate to?

Two issues:

• Syntactic concern: precedence and associativity
• Semantic concern: operand evaluation order: left-to-right, right-to-left, or something else

Does evaluation order matter? Without side-effects, it doesn’t. Called referential transparency.

Small-Step Operational Semantics

\[ e \longrightarrow e' \]

Expression \(e\) can take one step of evaluation to expression \(e'\).

• Defined on closed expressions \(e\).
• Eagerly apply the environment with substitution.
• Using environments or not is an orthogonal concern.

\[ \texttt{const one = 1; one + one} \quad\longrightarrow\quad \texttt{1 + 1} \]

Do Something

\(\inferrule[DoNeg]{ n' = - n_1 }{ \mathop{\texttt{-}} n_1 \longrightarrow n' }\)

\(\inferrule[DoPlus]{ n' = n_1 + n_2 }{ n_1 \mathbin{\texttt{+}} n_2 \longrightarrow n' }\)

Search for Something to Do

\(\inferrule[SearchNeg]{ e_1 \longrightarrow e_1' }{ \mathop{\texttt{-}} e_1 \longrightarrow\mathop{\texttt{-}} e_1' }\)

\(\inferrule[SearchPlus1]{ e_1 \longrightarrow e_1' }{ e_1 \mathbin{\texttt{+}} e_2 \longrightarrow e_1' \mathbin{\texttt{+}} e_2 }\)

\(\inferrule[SearchPlus2]{ e_2 \longrightarrow e_2' }{ n_1 \mathbin{\texttt{+}} e_2 \longrightarrow n_1 \mathbin{\texttt{+}} e_2' }\)

Implementation

defined trait Expr
defined trait Uop
defined trait Bop
defined class Unary
defined class Binary
defined class N
defined object Neg
defined object Plus

defined function isValue

e_oneplustwoplusthreeplusfour: Binary = Binary(
  bop = Plus,
  e1 = Binary(bop = Plus, e1 = N(n = 1.0), e2 = N(n = 2.0)),
  e2 = Binary(bop = Plus, e1 = N(n = 3.0), e2 = N(n = 4.0))
)

defined function step

Derivation

scala.NotImplementedError: an implementation is missing
  scala.Predef$.$qmark$qmark$qmark(Predef.scala:345)
  ammonite.$sess.cmd3$Helper.step(cmd3.sc:3)
  ammonite.$sess.cmd4$Helper.<init>(cmd4.sc:2)
  ammonite.$sess.cmd4$.<clinit>(cmd4.sc:7)

Calling step(e_oneplustwoplusthreeplusfour) corresponds to a witness of the judgment

\[ (1 \mathbin{\texttt{+}} 2) \mathbin{\texttt{+}} (3 \mathbin{\texttt{+}} 4) \longrightarrow 3 \mathbin{\texttt{+}} (3 \mathbin{\texttt{+}} 4) \]

------------------------------------------------ DoPlus
Binary(Plus,N(1.0),N(2.0)) ---> N(3.0)
------------------------------------------------ SearchPlus1
Binary(Plus,Binary(Plus,N(1.0),N(2.0)),Binary(Plus,N(3.0),N(4.0))) ---> Binary(Plus,N(3.0),Binary(Plus,N(3.0),N(4.0)))

defined function step
res5_1: Expr = Binary(
  bop = Plus,
  e1 = N(n = 3.0),
  e2 = Binary(bop = Plus, e1 = N(n = 3.0), e2 = N(n = 4.0))
)

Dynamic Typing

\[ \begin{array}{rrrl} \text{values} & v& \mathrel{::=}& n\mid b \end{array} \]

defined class B

defined function isValue

e_true: B = B(b = true)
e_trueplustwo: Binary = Binary(bop = Plus, e1 = B(b = true), e2 = N(n = 2.0))

\[ \begin{array}{rrrl} \text{step-results} & r& \mathrel{::=}& \mathop{\mathsf{typeerror}}e \mid e' \end{array} \]

defined class DynamicTypeError
defined type Result

Type Error: Neg

\[ \fbox{$e \longrightarrow r$} \]

\(\inferrule[DoNeg]{ }{ \mathop{\texttt{-}} n_1 \longrightarrow- n_1 }\)

\(\inferrule[TypeErrorNeg]{ v_1 \neq n_1 }{ \mathop{\texttt{-}} n_1 \longrightarrow \mathop{\mathsf{typeerror}}(\mathop{\texttt{-}} n_1) }\)

\(\inferrule[SearchNeg]{ e_1 \longrightarrow e_1' }{ \mathop{\texttt{-}} e_1 \longrightarrow\mathop{\texttt{-}} e_1' }\)

Type Error: Plus

\(\inferrule[DoPlus]{ }{ n_1 \mathbin{\texttt{+}} n_2 \longrightarrow n_1 + n_2 }\)

\(\inferrule[TypeErrorPlus2]{ v_2 \neq n_2 }{ n_1 \mathbin{\texttt{+}} v_2 \longrightarrow \mathop{\mathsf{typeerror}}(n_1 \mathbin{\texttt{+}} v_2) }\)

\(\inferrule[SearchPlus2]{ e_2 \longrightarrow e_2' }{ n_1 \mathbin{\texttt{+}} e_2 \longrightarrow n_1 \mathbin{\texttt{+}} e_2' }\)

\(\inferrule[TypeErrorPlus1]{ v_1 \neq n_1 }{ v_1 \mathbin{\texttt{+}} e_2 \longrightarrow \mathop{\mathsf{typeerror}}(v_1 \mathbin{\texttt{+}} e_2) }\)

\(\inferrule[SearchPlus1]{ e_1 \longrightarrow e_1' }{ e_1 \mathbin{\texttt{+}} e_2 \longrightarrow e_1' \mathbin{\texttt{+}} e_2 }\)

\(\inferrule[PropagateNeg]{ e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }{ \mathop{\texttt{-}} e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }\)

\(\inferrule[PropagatePlus2]{ e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }{ n_1 \mathbin{\texttt{+}} e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }\)

\(\inferrule[PropagatePlus1]{ e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }{ e_1 \mathbin{\texttt{+}} e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }\)

Implementation

defined function step

defined function step

defined function step

Short-Circuiting Evaluation

\(\inferrule[SearchBinary1]{ e_1 \longrightarrow e_1' }{ e_1 \mathbin{\mathit{bop}}e_2 \longrightarrow e_1' \mathbin{\mathit{bop}}e_2 }\)

\(\inferrule[SearchBinary2]{ e_2 \longrightarrow e_2' }{ v_1 \mathbin{\mathit{bop}}e_2 \longrightarrow v_1 \mathbin{\mathit{bop}}e_2' }\)

\(\inferrule[DoAndTrue]{ v_1 \rightsquigarrow \mathbf{true} }{ v_1 \mathbin{\texttt{\&\&}} e_2 \longrightarrow e_2 }\)

\(\inferrule[DoAndFalse]{ v_1 \rightsquigarrow \mathbf{false} }{ v_1 \mathbin{\texttt{\&\&}} e_2 \longrightarrow v_1 }\)

\(\inferrule[DoOrTrue]{ v_1 \rightsquigarrow \mathbf{true} }{ v_1 \mathbin{\texttt{||}} e_2 \longrightarrow v_1 }\)

\(\inferrule[DoOrFalse]{ v_1 \rightsquigarrow \mathbf{false} }{ v_1 \mathbin{\texttt{||}} e_2 \longrightarrow e_2 }\)

Variables

\(\inferrule[DoConstDecl]{ }{ \mathbf{const}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 \longrightarrow {}[v_1/x]e_2 }\)

\(\inferrule[SearchConstDecl]{ e_1 \longrightarrow e_1' }{ \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow\mathbf{const}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 }\)

Substitution

Shadowing \[ [\underbrace{\texttt{2}}_{e_1} /\underbrace{\texttt{a}}_{x} ] \underbrace{(\texttt{const a = 1; a + b})}_{e_2} = (\texttt{const a = 1; a + b}) \]

Free-Variable Capture

\[ [\underbrace{\texttt{(a + 2)}}_{e_1} /\underbrace{\texttt{b}}_{x} ] \underbrace{(\texttt{const a = 1; a + b})}_{e_2} = (\texttt{const c = 1; c + (a + 2)}) \]