21 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}} $

In defining a big-step operational semantics (Section 18.1), we have carefully specified several aspects of how the expression $e_1 \mathbin{\texttt{+}} e_2$ should be evaluated. In essence, it says that it adds two numbers that result from evaluating $e_1$ and $e_2$. However, there is still at least one more semantic question that we have not specified, “Is $e_1$ evaluated first and then $e_2$ or vice versa, or are they evaluated concurrently?”

Why does this question matter? Consider the JavaScripty expression:

(console.log(1), 1) + (console.log(2), 2)

The , operator is a sequencing operator. In particular, $e_1$ , $e_2$ first evaluates $e_1$ to a value and then evaluates $e_2$ to value; the value of the whole expression is the value of $e_2$, while the value of $e_1$ is simply thrown away. Furthermore, console.log( $e_1$ ) evaluates its argument to a value and then prints to the console a representation of that value. If the left operand of + is evaluated first before the right operand, then the above expression prints 1 and then 2. If the operands of are evaluated in the opposite order, then 2 is printed first followed by 1. Note that the final value is 3 regardless of the evaluation order.

The evaluation order matters because the console.log( $e_1$ ) expression has a side effect. It prints to the screen. As alluded to early on in discussing functional versus imperative computation (Section 3.1), an expression free of side effects (i.e., is pure) has the advantage that the evaluation order cannot be observed (i.e., does not matter from the programmer’s perspective). Having this property is also known as being referentially transparent, that is, taking an expression and replacing any of its subexpressions by the subexpression’s value cannot be observed as evaluating any differently than evaluating the expression itself. So far in JavaScripty, our only side-effecting expression is console.log( $e_1$ ). If we remove the console.logs from the above expression, then the evaluation order cannot be observed.

21.1 A Small-Step Operational Semantics

The big-step operational semantics (Section 18.1) does give us a nice specification for implementing an interpreter, but it does leave some semantic choices like evaluation order implicit. Intuitively, it specifies what the value of an expression should be (if it exists) but not precisely the steps to get to the value.

We have already used a notation for describing a one-step evaluation relation: \[ e \longrightarrow e' \] This notation is a judgment form stating informally, “Expression $e$ can take one step of evaluation to expression $e'$.” Defining this judgment allows us to more precisely state how to take one step of evaluation, that is, how to make a single reduction step. Once we know how to reduce expressions, we can evaluate an expression $e$ by repeatedly applying reduction until reaching a value. Thus, such a definition describes an operational semantics and intuitively an interpreter for expressions $e$. This style of operational semantics where we specify reduction steps is called a small-step operational semantics.

In contrast to previous chapters, we will not extend this judgment form with value environments for free variables. Instead, we define the one-step reduction relation on closed expressions, that is, expressions without any free variables. If we require the “top-level” program to be a closed expression, then we can ensure reduction only sees closed expressions by intuitively “applying the environment” eagerly via substitution. That is, variable uses are replaced by the values to which they are bound before reduction gets to them. As an example, we will define reduction so that the following judgment holds: \[ \texttt{const one = 1; one + one} \quad\longrightarrow\quad \texttt{1 + 1} \] This choice to use substitution instead of explicit environments is orthogonal to specifying the semantics using small-step or big-step (i.e., one could use substitution with big-step as in Section 19.4 or environments with small-step). Explicit environments just get a bit more unwieldy here.

21.2 One Type of Values

Let us consider an object language with just numbers $n$, a unary arithmetic operator $\texttt{-}$, and a binary arithmetic operator $\texttt{+}$:

\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& v\mid\mathop{\mathit{uop}} e_1 \mid e_1 \mathbin{\mathit{bop}} e_2 \\ \text{values} & v& \mathrel{::=}& n \\ \text{unary operators} & \mathit{uop}& \mathrel{::=}& \texttt{-} \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{+} \\ \text{numbers} & n \end{array} \]

trait Expr // e
trait Uop  // uop
trait Bop  // bop

case class Unary(uop: Uop, e1: Expr) extends Expr            // e ::= uop e1
case class Binary(bop: Bop, e1: Expr, e2: Expr) extends Expr // e ::= e1 bop e2

case class N(n: Double) extends Expr // e ::= n
case object Neg extends Uop          // uop ::= -
case object Plus extends Bop         // bop ::= +

def isValue(e: Expr): Boolean = e match {
  case N(_) => true
  case _ => false
}

val e_oneplustwoplusthreeplusfour = Binary(Plus, Binary(Plus, N(1), N(2)), Binary(Plus, N(3), N(4)))

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))
)

Do Something

First, we need to describe what action does an operation perform. For example, we want to say that the $\texttt{-}$ operator negates a number and the $\texttt{+}$ operator adds two numbers, respectively. We say this with the following two rules:

$\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' }$

These rules say that the expression $\mathop{\texttt{-}} n_1$ and the expression $n_1 \mathbin{\texttt{+}} n_2$ reduces in one step to an integer value $n'$ that are the negation of a number $n_1$ and the addition of the numbers $n_1$ and $n_2$, respectively. We use the meta-variables $n_1$, $n_2$, and $n'$ to express constraints that particular positions in the expressions numeric values. Note that the in the conclusions are the syntactic operators $\texttt{-}$ and $\texttt{+}$, while the $-$ and $+$ in the premises express mathematical negation of a number and addition of two numbers, respectively. As we discussed previously, this symbol clash is rather unfortunate, but context usually allows us to determine which is which. We sometimes call this kind of rule that performs an operation a local reduction rule. We will prefix all rules for this kind of rule with $\TirName{Do}$ (and so will sometimes call them $\TirName{Do}$ rules).

Note that the following way of writing $\TirName{DoNeg}$ and $\TirName{DoPlus}$ say the same thing:

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

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

Observe the distinction between the syntactic operators $\texttt{-}$ and $\texttt{+}$ and the mathematical operations $-$ and $+$.

Search for Something to Do

Second, we need to describe how we find the next operation to perform. These rules will capture issues like evaluation order described informally above.

For $\mathop{\texttt{-}} e_1$, the rule $\TirName{SearchNeg}$ says, “If it is possible to take a step from $e_1$ to $e_1'$, then $\mathop{\texttt{-}} e_1$ steps to $\mathop{\texttt{-}} e_1'$.” That is, the next expression to reduce is somewhere in the sub-expression $e_1$.

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

For $e_1 \mathbin{\texttt{+}} e_2$, there are multiple ways we can define the next possible step. We could take a step in on the left (i.e., $e_1$) or on the right (i.e., $e_2$). We could reduce $e_1$ to a value before continuing on to $e_2$ (i.e., called left-to-right) or vice versa (i.e., called right-to-left), or we can allow $e_1$ and $e_2$ to reduce concurrently.

To specify that $e_1 \mathbin{\texttt{+}} e_2$ should be evaluated left-to-right, we use the following two rules:

$\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' }$

The $\TirName{SearchPlus1}$ rule states for an arbitrary expression of the form $e_1 \mathbin{\texttt{+}} e_2$, if $e_1$ steps to $e_1'$, then the whole expression steps to $e_1' \mathbin{\texttt{+}} e_2$. We can view this rule as saying that we should look for an operation to perform somewhere in $e_1$. The rest of the expression $\bullet \mathbin{\texttt{+}} e_2$ is a context that gets carried over untouched. The rule is similar except that it applies only if the left expression is a value (i.e., $n_1 \mathbin{\texttt{+}} e_2$). Together, these rules capture precisely a left-to-right evaluation order for an expression of the form $e_1 \mathbin{\texttt{+}} e_2$ because (1) if $e_1$ is not a value, then only $\TirName{SearchPlus1}$ could possibly apply, and (2) if $e_1$ is a number value, then only $\TirName{SearchPlus2}$ could possibly apply. We sometimes call this kind of rule that finds the next operation to perform a global reduction rule (or a $\TirName{Search}$ rule). The sub-expression that is the next operation to perform is called the redex (for reducible expression).

Observe that there is no rule for a number literal $n$. It is already a value, so there is no reduction step.

Implementation

We translate these rules directly to an implementation:

def step(e: Expr): Expr = {
  require(!isValue(e))
  e match {
    // DoNeg
    case Unary(Neg, N(n1)) => N(-n1)
    // SearchNeg
    case Unary(Neg, e1) => Unary(Neg, step(e1))
    // DoPlus
    case Binary(Plus, N(n1), N(n2)) => N(n1 + n2)
    // SearchPlus2
    case Binary(Plus, N(n1), e2) => Binary(Plus, N(n1), step(e2))
    // SearchPlus1
    case Binary(Plus, e1, e2) => Binary(Plus, step(e1), e2)
  }
}

defined function step

Observe that we do have to pay attention to the specificity of the pattern match and order the // SearchPlus2 case before the // SearchPlus1 case. And if there is no matching case, then we would get a MatchError exception.

A Test Case and a Step Judgment

We consider a test case to show evaluation order:

e_oneplustwoplusthreeplusfour
val e_step_oneplustwoplusthreeplus = step(e_oneplustwoplusthreeplusfour)

res2_0: 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))
)
e_step_oneplustwoplusthreeplus: Expr = Binary(
  bop = Plus,
  e1 = N(n = 3.0),
  e2 = Binary(bop = Plus, e1 = N(n = 3.0), e2 = N(n = 4.0))
)

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) \]

Observe that we reduce the left side of the top-level $\texttt{+}$.

Let us instrument step to show a derivation:

def step(e: Expr): Expr = {
  require(!isValue(e))
  val e_ = e match {
     // DoNeg
    case Unary(Neg, N(n1)) => {
      println("------------------------------------------------ DoNeg")
      N(-n1)
    }
    // SearchNeg
    case Unary(Neg, e1) => {
      println("------------------------------------------------ SearchNeg")
      Unary(Neg, step(e1))
    }
    // DoPlus
    case Binary(Plus, N(n1), N(n2)) => {
      println("------------------------------------------------ DoPlus")
      N(n1 + n2)
    }
    // SearchPlus2
    case Binary(Plus, N(n1), e2) => {
      val e2_ = step(e2)
      println("------------------------------------------------ SearchPlus2")
      Binary(Plus, N(n1), e2_)
    }
    // SearchPlus1
    case Binary(Plus, e1, e2) => {
      val e1_ = step(e1)
      println("------------------------------------------------ SearchPlus1")
      Binary(Plus, e1_, e2)
    }
  }
  println(s"$e ---> $e_")
  e_
}

step(e_oneplustwoplusthreeplusfour)

------------------------------------------------ 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
res3_1: Expr = Binary(
  bop = Plus,
  e1 = N(n = 3.0),
  e2 = Binary(bop = Plus, e1 = N(n = 3.0), e2 = N(n = 4.0))
)

Observe that the derivation is simply to find which sub-expression to apply a single $\TirName{Do}$ rule.

Meta-Theory

Considering these rules, there is at most one rule that applies that specifies the “next” step. If our set of inference rules defining reduction has this property, then we say that our reduction system is deterministic. In other words, there is always at most one “next” step. Determinism is a property that we could prove about certain reduction systems, which we can state formally as follows:

Proposition 21.1 (Determinism) If $e \longrightarrow e'$ and $e \longrightarrow e''$, then $e' = e''$.

In general, such a proof would proceed by structural induction on the derivation of the reduction step (i.e., $e \longrightarrow e'$). We do not consider such proofs in detail(cf., ?sec-induction-on-derivations).

21.3 Dynamic Typing

Let us add boolean values to our JavaScripty variant:

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

case class B(b: Boolean) extends Expr // e ::= b

def isValue(e: Expr): Boolean = e match {
  case N(_) | B(_) => true
  case _ => false
}

val e_true = B(true)
val e_trueplustwo = Binary(Plus, e_true, N(2))

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))

Since we only add boolean literals that are values, there are no additional rules we need for $e \longrightarrow e'$.

def step(e: Expr): Expr = {
  require(!isValue(e), s"$e should not be a value")
  e match {
    // DoPlus
    case Binary(Plus, N(n1), N(n2)) => N(n1 + n2)
    // SearchPlus2
    case Binary(Plus, N(n1), e2) => Binary(Plus, N(n1), step(e2))
    // SearchPlus1
    case Binary(Plus, e1, e2) => Binary(Plus, step(e1), e2)
  }
}

defined function step

As expected with the expression $\mathbf{true} \mathbin{\texttt{+}} 2$, we run into undefined behavior with these rules, which manifests haphazardly in our implementation as failing the require(!isValue(e)):

e_trueplustwo
val v_trueplustwo = step(e_trueplustwo)

java.lang.IllegalArgumentException: requirement failed: B(true) should not be a value
  scala.Predef$.require(Predef.scala:338)
  ammonite.$sess.cmd5$Helper.step(cmd5.sc:2)
  ammonite.$sess.cmd5$Helper.step(cmd5.sc:9)
  ammonite.$sess.cmd6$Helper.<init>(cmd6.sc:2)
  ammonite.$sess.cmd6$.<clinit>(cmd6.sc:7)

Our implicit intent is that a type error is where we are stuck—that is, there is no next step and the expression $e$ is not a value. But what if we are stuck because we have a bug in our rules? We want to explicit about when there is a dynamic type error (i.e., there is a bug in the object program that the programmer gave us) versus a bug in our semantic rules. Previously, we did so informally in implementation with throw DynamicTypeError(e) (cf. Section 18.3), but that relies on the exception semantics of the Scala meta-language that was not explicitly described in our semantics specification. We wish to also define precisely the sub-expression e that is to blame.

Let us introduce a step-result type \[ \begin{array}{rrrl} \text{step-results} & r& \mathrel{::=}& \mathop{\mathsf{typeerror}}e \mid e' \end{array} \] to make explicit that step can return a type-error result. Specifically, a step-result is either a $\mathop{\mathsf{typeerror}}e$ with the expression $e$ to blame or a one-step reduced expression $e'$.

case class DynamicTypeError(e: Expr)         // typeerror e
type Result = Either[DynamicTypeError, Expr] // r ::= typeerror e | e

defined class DynamicTypeError
defined type Result

We have chosen to represent a step-result $r$ in Scala as an Either[DynamicTypeError, Expr].

We now consider the judgment form $e \longrightarrow r$ that says, “Expression $e$ takes a step to a result $r$.” with the intention that step: Expr => Result is a total function:

def step(e: Expr): Result = ???

defined function step

We add rules that explicitly state when we step to a $\mathsf{typeerror}$:

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

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

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

$\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 }$

def step(e: Expr): Either[DynamicTypeError, Expr] = {
  require(!isValue(e))
  e match {
    // DoNeg
    case Unary(Neg, N(n1)) => Right(N(-n1))
    // TypeErrorNeg
    case Unary(Neg, v1) if isValue(v1) => Left(DynamicTypeError(e))
    case Unary(Neg, e1) => step(e1) match {
      // SearchNeg
      case Right(e1) => Right(Unary(Neg, e1))
      // PropagateNeg
      case Left(error) => Left(error)
    }
    case Binary(Plus, N(n1), v2) if isValue(v2) => v2 match {
      // DoPlus
      case N(n2) => Right(N(n1 + n2))
      // TypeErrorPlus2
      case _ => Left(DynamicTypeError(e))
    }
    case Binary(Plus, v1, e2) if isValue(v1) => v1 match {
      case N(n1) => step(e2) match {
        // SearchPlus2
        case Right(e2) => Right(Binary(Plus, N(n1), e2))
        // PropagatePlus2
        case Left(error) => Left(error)
      }
      // TypeErrorPlus1
      case _ => Left(DynamicTypeError(e))
    }
    case Binary(Plus, e1, e2) => step(e1) match {
      // SearchPlus1
      case Right(e1) => Right(Binary(Plus, e1, e2))
      // PropagatePlus1
      case Left(error) => Left(error)
    }
  }
}

defined function step

e_trueplustwo
val v_trueplustwo = step(e_trueplustwo)

res10_0: Binary = Binary(bop = Plus, e1 = B(b = true), e2 = N(n = 2.0))
v_trueplustwo: Either[DynamicTypeError, Expr] = Left(
  value = DynamicTypeError(
    e = Binary(bop = Plus, e1 = B(b = true), e2 = N(n = 2.0))
  )
)

From the implementation, we discover that there are three more cases, that is,

case Left(error) => Left(error)

cases to make step: Expr => Either[DynamicTypeError, Expr] a total function. In those cases, we encountered a $\mathsf{typeerror}$ in a sub-expression from recursively calling step, and we simply want to propagate the DynamicTypeError:

$\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 }$

Either.map

Recall that the Either[Err, A] type is often used like an Option[A] type, except that the “bad” case has some data payload (i.e., the None case for an Option[A] corresponds to the Left(err) case for an Either[Err, A]). This “propagate error” pattern is so common that the the Either[Err, A] type has a higher-order method map that takes a callback for what transformation to make with the Right case and otherwise propagate the Left case.

Thus, we can refactor the step implementation from above as follows:

def step(e: Expr): Either[DynamicTypeError, Expr] = {
  require(!isValue(e))
  e match {
    // DoNeg
    case Unary(Neg, N(n1)) => Right(N(-n1))
    // TypeErrorNeg
    case Unary(Neg, v1) if isValue(v1) => Left(DynamicTypeError(e))
    // SearchNeg and PropagateNeg
    case Unary(Neg, e1) => step(e1) map { e1 => Unary(Neg, e1) }
    case Binary(Plus, N(n1), v2) if isValue(v2) => v2 match {
      // DoPlus
      case N(n2) => Right(N(n1 + n2))
      // TypeErrorPlus2
      case _ => Left(DynamicTypeError(e))
    }
    case Binary(Plus, v1, e2) if isValue(v1) => v1 match {
      // SearchPlus2 and PropagatePlus2
      case N(n1) => step(e2) map { e2 => Binary(Plus, N(n1), e2)  }
      // TypeErrorPlus1
      case _ => Left(DynamicTypeError(e))
    }
    // SearchPlus1 and PropagatePlus1
    case Binary(Plus, e1, e2) => step(e1) map { e1 => Binary(Plus, e1, e2) }
  }
}

defined function step

Note that the map method is common for both Either[Err, A] and Option[A]:

None    map { (i: Int) => i + 1 }
Some(3) map { (i: Int) => i + 1 }

res12_0: Option[Int] = None
res12_1: Option[Int] = Some(value = 4)

21.4 Generic Evaluation Order

Let us add the boolean expressions for conditionals, $\texttt{!}$, $\texttt{\&\&}$, $\texttt{||}$, and $\texttt{===}$:

\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \\ \text{unary operators} & \mathit{uop}& \mathrel{::=}& \texttt{!} \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{\&\&}\mid\texttt{||}\mid\texttt{===} \end{array} \]

case class If(e1: Expr, e2: Expr, e3: Expr) extends Expr // e ::= e1 ? e2 : e3

case object Not extends Uop // uop ::= !
case object And extends Bop // bop ::= &&
case object Or extends Bop  // bop ::= ||

case object Eq extends Bop  // bop ::= ===

defined class If
defined object Not
defined object And
defined object Or
defined object Eq

Our first observation is that evaluation order is a concern regardless of the type of operations. Suppose we define that all binary operators are evaluated left-to-right, then we can replace the rules $\TirName{SearchNeg}$, $\TirName{SearchPlus1}$, and $\TirName{SearchPlus2}$ with these more generic versions:

$\inferrule[SearchUnary]{ e_1 \longrightarrow e_1' }{ \mathop{\mathit{uop}}e_1 \longrightarrow\mathop{\mathit{uop}}e_1' }$

$\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' }$

The same makes sense for the rules that propagate type error, replacing $\TirName{PropagateNeg}$, $\TirName{PropagatePlus1}$, and $\TirName{PropagatePlus2}$ with the following:

$\inferrule[PropagateUnary]{ e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }{ \mathop{\mathit{uop}} e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }$

$\inferrule[PropagateBinary1]{ e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }{ e_1 \mathbin{\mathit{bop}} e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }$

$\inferrule[PropagateBinary2]{ e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }{ v_1 \mathbin{\mathit{bop}} e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }$

21.5 Non-Determinism

Consider the relationship between the $\TirName{SearchBinary1}$ and $\TirName{SearchBinary2}$ rules that define generically for all binary operators $\mathit{bop}$ a left-to-right evaluation order and dynamic typing.

$\inferrule[TypeErrorPlus1]{ v_1 \neq n_1 }{ v_1 \mathbin{\texttt{+}} e_2 \longrightarrow \mathop{\mathsf{typeerror}}(v_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' }$

In the rules above, the $\TirName{TypeErrorPlus1}$ rule and the $\TirName{SearchPlus2}$ are disjoint (i.e., one rule applies to determine the next step) for an expression of the form $v_1 \mathbin{\texttt{+}} e_2$. However, if we replace $\TirName{SearchPlus2}$ with $\TirName{SearchBinary2}$, that is no longer the case. That is, our step relation $e \longrightarrow r$ is no longer deterministic, or we say that it has non-determinism.

What this means from an implementation standpoint is that while the semantics specification with $\TirName{SearchPlus2}$ states that an implementation must step to a $\mathsf{typeerror}$ using $\TirName{TypeErrorPlus1}$ before taking a step $e_2$. The pair of rules $\TirName{TypeErrorPlus1}$ and $\TirName{SearchBinary2}$ are not disjoint, so an implementation may choose to take some steps in $e_2$ using $\TirName{SearchBinary2}$ before stepping to a $\mathsf{typeerror}$ using $\TirName{TypeErrorPlus1}$. The implementation that steps to a $\mathsf{typeerror}$ as soon as possible is still valid but other implementations are now permitted.

21.6 Short-Circuiting Evaluation

Let us define the semantics of the core boolean expressions as in JavaScript. The $\TirName{DoNot}$ rule converts value $v_1$ into a boolean and returns its negation:

$\inferrule[DoNot]{ v_1 \rightsquigarrow b_1 }{ \mathop{\texttt{!}} v_1 \longrightarrow\neg b_1 }$

What we have seen already is that the $\texttt{\&\&}$ and $\texttt{||}$ operators do not behave like mathematical logic operators $\land$ and $\lor$ (whereas $\texttt{!}$ does behave like $\lnot$ after coercion):

$\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 }$

For the $\texttt{\&\&}$ and $\texttt{||}$ operators, given that binary operators evaluate left-to-right, once we have evaluated $e_1$ to a value, we do not necessarily need to evaluate $e_2$. That is, we may short-circuit evaluating $e_2$. We say that a short-circuiting evaluation of an expression is one where a value is produced before evaluating all sub-expressions to values. We say that the expressions $e_1 \mathbin{\texttt{\&\&}} e_2$ and $e_1 \mathbin{\texttt{||}} e_2$ may short-circuit. In particular, the $\TirName{DoAndFalse}$ rule says that $v_1 \mathbin{\texttt{\&\&}} e_2$ where $v_1$ converts to $\mathbf{false}$ evaluates to $v_1$ without ever evaluating $e_2$. The analgous rule for $\texttt{||}$ is $\TirName{DoOrTrue}$.

For $e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3$, the rules $\TirName{DoIfTrue}$ and $\TirName{DoIfFalse}$ specify with which expression to continue evaluation in the expected way depending on what boolean value to which the guard converts:

$\inferrule[DoIfTrue]{ v_1 \rightsquigarrow \mathbf{true} }{ v_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \longrightarrow e_2 }$

$\inferrule[DoIfFalse]{ v_1 \rightsquigarrow \mathbf{false} }{ v_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \longrightarrow e_3 }$

Observe how similar $\TirName{DoAndTrue}$ and $\TirName{DoOrFalse}$ are to $\TirName{DoIfTrue}$ and $\TirName{DoIfFalse}$, respectively. We see that $\texttt{\&\&}$ and $\texttt{||}$ operators have quite a bit similarity to control-flow operators like $e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3$ and significant differences compared to the mathematical logic operators $\land$ and $\lor$, respectively.

Many programming languages implement short-circuiting boolean operators $\texttt{\&\&}$ and $\texttt{||}$.

Searching for a redex in $\texttt{\&\&}$ and $\texttt{||}$ are covered by $\TirName{SearchBinary1}$ and $\TirName{SearchBinary2}$. For $e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3$, we need a $\TirName{SearchIf}$ rule to reduce the guard expression $e_1$ to a value:

$\inferrule[SearchIf]{ e_1 \longrightarrow e_1' }{ e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \longrightarrow e_1'\;\texttt{?}\;e_2\;\texttt{:}\;e_3 }$

and propagating $\mathsf{typeerror}$ as needed:

$\inferrule[PropagateIf]{ e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }{ e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3 \longrightarrow \mathop{\mathsf{typeerror}}e }$

21.7 Polymorphism

The $\texttt{===}$ operator does not perform coercions but is still polymorphic, that is, it applies regardless of the type of value of its arguments:

$\inferrule[DoEquality]{ }{ v_1 \mathbin{\texttt{===}} v_2 \longrightarrow v_1 = v_2 }$

We observe that $v_1 = v_2$ is $\mathbf{false}$ if the types of $v_1$ and $v_2$ do not match. In JavaScript, this is called strict equality, as it has another operator $\texttt{==}$ that performs coercions before comparing for equality called loose equality.

21.8 Recursion

Let us consider our object language JavaScripty with variables, binding, and optionally-named functions:

\[ \begin{array}{rrrll} \text{values} & v& \mathrel{::=}& x\mid x^{?}\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 \\ \text{expressions} & e& \mathrel{::=}& \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \mid e_1\texttt{(}e_2\texttt{)} \\ \text{optional variables} & x^{?}& \mathrel{::=}& x\mid\varepsilon \\ \text{variables} & x \end{array} \]

To call a function within itself, we permit functions to have a variable identifier to refer to itself. If the identifier is present, then it can be used for recursion.

case class Var(x: String) extends Expr                                 // e ::= x
case class ConstDecl(x: String, e1: Expr, e2: Expr) extends Expr       // e ::= const x = e1; e2
case class Fun(xopt: Option[String], y: String, e1: Expr) extends Expr // e ::= x?(y) => e1
case class Call(e1: Expr, e2: Expr) extends Expr                       // e ::= e1(e2)

def isValue(e: Expr): Boolean = e match {
  case N(_) | B(_) | Fun(_, _, _) => true
  case _ => false
}

defined class Var
defined class ConstDecl
defined class Fun
defined class Call
defined function isValue

For exmaple, here is an abstract syntax tree for a recursive function silly:

val e_sillyRecFun = Fun(Some("silly"), "i",
  If(Binary(Eq, Var("i"), N(0)),
     Var("j"),
     Binary(Plus,
            Var("j"),
            Call(Var("silly"), Binary(Plus, Var("i"), Unary(Neg, N(1)))))))

e_sillyRecFun: Fun = Fun(
  xopt = Some(value = "silly"),
  y = "i",
  e1 = If(
    e1 = Binary(bop = Eq, e1 = Var(x = "i"), e2 = N(n = 0.0)),
    e2 = Var(x = "j"),
    e3 = Binary(
      bop = Plus,
      e1 = Var(x = "j"),
      e2 = Call(
        e1 = Var(x = "silly"),
        e2 = Binary(
          bop = Plus,
          e1 = Var(x = "i"),
          e2 = Unary(uop = Neg, e1 = N(n = 1.0))
        )
      )
    )
  )
)

corresponding to the concrete syntax:

function silly(i) { return i === 0 ? j : j + silly(i + -1); }

Recall accidental “dynamic scoping” (cf. Chapter 19). We lazily wait until seeing a variable use to determine the variable binding site. The “bug” comes from using the “wrong” environment. A possible fix is to save the “right” environment with the function value—what’s known as closure.

A brute force alternative is to always work with closed expressions (i.e., expressions that have no free variable uses). As soon as we know the variable binding, we eagerly “get rid” of variable uses with substitution. We see that the definition of the set of free variables uses of an expression defines the binding site and scope of a variable:

def freeVars(e: Expr): Set[String] = e match {
  case N(_) | B(_) => Set.empty
  case Unary(_, e1) => freeVars(e1)
  case Binary(_, e1, e2) => freeVars(e1) union freeVars(e2)
  case If(e1, e2, e3) => freeVars(e1) union freeVars(e2) union freeVars(e3)
  case Var(x) => Set(x)
  case ConstDecl(x, e1, e2) => freeVars(e1) union (freeVars(e2) - x)
  case Fun(xopt, y, e1) => freeVars(e1) -- xopt - y
  case Call(e1, e2) => freeVars(e1) union freeVars(e2)
}

def closed(e: Expr): Boolean = freeVars(e).isEmpty

freeVars(e_sillyRecFun)
closed(e_sillyRecFun)

defined function freeVars
defined function closed
res16_2: Set[String] = Set("j")
res16_3: Boolean = false

Thus, the step function expects input expressions that are closed, non-value expressions:

def step(e: Expr): Either[DynamicTypeError, Expr] = {
  require(!isValue(e), s"$e should not be a value")
  require(closed(e), s"$e should be closed")
  ???
}

step(e_sillyRecFun)

java.lang.IllegalArgumentException: requirement failed: Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),Var(j),Binary(Plus,Var(j),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))) should not be a value
  scala.Predef$.require(Predef.scala:338)
  ammonite.$sess.cmd17$Helper.step(cmd17.sc:2)
  ammonite.$sess.cmd17$Helper.<init>(cmd17.sc:7)
  ammonite.$sess.cmd17$.<clinit>(cmd17.sc:7)

Correspondingly, there is no $\TirName{DoVar}$ rule for the judgment form $e \longrightarrow r$ because $e$ must be closed (cf. there is no $\TirName{EvalVar}$ rule in Section 19.4).

The $\TirName{DoConstDecl}$ rule for the variable binding expression $\mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2$ eagerly applies substitution to eliminate free-variable uses:

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

The expression-to-be-bound should already be a value $v_1$. We then proceed to $e_2$ with the value $v_1$ replacing the variable $x$. In general, the notation ${}[e_1/x]e_2$ is read as the capture-avoiding substitution of expression $e_1$ for variable $x$ in $e_2$.

We then need a $\TirName{SearchConstDecl}$ rule to step $e_1$ to a value in a $\mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2$ expression:

$\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 }$

$\inferrule[PropagateConstDecl]{ e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }{ \mathbf{const}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }$

We have two cases for reducing a function call $e_1\texttt{(}e_2\texttt{)}$, depending on whether the function is named or not:

$\inferrule[DoCall]{ }{ (\texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(}v_2\texttt{)} \longrightarrow{}[v_2/x]e_1 }$

$\inferrule[DoCallRec]{ v_1 = (x_1\texttt{(}x_2\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) }{ v_1\texttt{(}v_2\texttt{)} \longrightarrow {}[v_1/x_1] {}[v_2/x_2]e_1 }$

If it is unnamed, the $\TirName{DoCall}$ rule applies binding the actual argument $v_2$ to the formal parameter $x$ by substituting $v_2$ for free variable uses $x$ in $e_1$. If it named, then are two formal parameters $x_1$ and $x_2$ where $x_1$ is bound to the function value itself $v_1$ and $x_2$ is bound to the actual argument $v_2$. In this case, the $\TirName{DoCallRec}$ rule applies by stepping to ${}[v_1/x_1] {}[v_2/x_2]e_1 $. The $\TirName{DoCallRec}$ shows the essence of recursion—a self-reference to the function value itself!

If $v_1$ in the function call expression $v_1\texttt{(}e_2\texttt{)}$ is not a function value, then we have dynamic type error:

$\inferrule[TypeErrorCall]{ v_1 \neq x^{?}\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 }{ v_1\texttt{(}e_2\texttt{)} \longrightarrow \mathop{\mathsf{typeerror}} (v_1\texttt{(}e_2\texttt{)}) }$

Observe that we step to a $\mathsf{typeerror}$ only when $v_1\texttt{(}v_2\texttt{)}$. That is, we follow JavaScript here in delaying the check for a dynamic type error until both the function position and the argument position are values.

We define evaluating function call $e_1\texttt{(}e_2\texttt{)}$ as left-to-right and continuing even if $e_1$ reduces to a non-function value:

$\inferrule[SearchCall1]{ e_1 \longrightarrow e_1' }{ e_1\texttt{(}e_2\texttt{)} \longrightarrow e_1'\texttt{(}e_2\texttt{)} }$

$\inferrule[SearchCall2]{ e_2 \longrightarrow e_2' }{ v_1 \texttt{(}e_2\texttt{)} \longrightarrow v_1 \texttt{(}e_2'\texttt{)} }$

$\inferrule[PropagateCall1]{ e_1 \longrightarrow \mathop{\mathsf{typeerror}}e }{ e_1\texttt{(}e_2\texttt{)} \longrightarrow \mathop{\mathsf{typeerror}}e }$

$\inferrule[PropagateCall2]{ e_2 \longrightarrow \mathop{\mathsf{typeerror}}e }{ v_1\texttt{(}e_2\texttt{)} \longrightarrow \mathop{\mathsf{typeerror}}e }$

21.9 Substitution

The term capture-avoiding subsitution means that for ${}[e_1/x]e_2$, we get the expression that is like $e_2$, but we have replaced all instances of variable $x$ with $e_1$ while carefully respecting static scoping (cf., Chapter 14). There are two thorny issues that arise.

Shadowing: The substitution \[ [\underbrace{\texttt{2}}_{e_1} /\underbrace{\texttt{a}}_{x} ] \underbrace{(\texttt{const a = 1; a + b})}_{e_2} \] should yield $(\texttt{const a = 1; a + b})$. That is, only free instances of $x$ in $e_2$ should be replaced.
Free Variable Capture: The substutition \[ [\underbrace{\texttt{(a + 2)}}_{e_1} /\underbrace{\texttt{b}}_{x} ] \underbrace{(\texttt{const a = 1; a + b})}_{e_2} \] should yield something like $(\texttt{const c = 1; c + (a + 2)})$. In particular, the following result is wrong: \[ (\texttt{const a = 1; a + (a + 2)}) \] because the free variable $\texttt{a}$ in $e_1$ gets “captured” by the $\mathbf{const}$ binding of $\texttt{a}$.

In both cases, the issues could be resolved by renaming all bound variables in $e_2$ so that there are no name conflicts with free variables in $e_1$ or $x$. In other words, it is clear what to do if $e_2$ were instead \[ \texttt{const c = 1; c + b} \] in which case simple textual substitution would suffice.

The observation is that renaming bound variables should preserve the meaning of the expression, that is, the following two expressions are somehow equivalent: \[ (\texttt{const a = 1; a}) \quad\equiv_{\alpha}\quad (\texttt{const b = 1; b}) \] For historical reasons, this equivalence is known $\alpha$-equivalence, and the process of renaming bound variables is called $\alpha$-renaming (cf. Section 14.4).

In rules $\TirName{DoConstDecl}$, $\TirName{DoCall}$, and $\TirName{DoCallRec}$, our situation is more restricted than the general case discussed above. In particular, the substitution is of the form ${}[v/x]e$ where the replacement for $v$ has to be a value with no free variables, so only the shadowing issue arises.

\[ \begin{array}{rcll} {}[e'/x]y & \stackrel{\text{\tiny def}}{=}& e' & \text{if $x= y$} \\ {}[e'/x]y & \stackrel{\text{\tiny def}}{=}& y& \text{if $x\neq y$} \\[1ex] {}[e'/x] (\mathbf{const}\;y\;\texttt{=}\;e_1\texttt{;}\;e_2) & \stackrel{\text{\tiny def}}{=}& \mathbf{const}\;y\;\texttt{=}\; ({}[e'/x]e_1) \texttt{;}\;e_2 & \text{if $x= y$} \\ {}[e'/x] (\mathbf{const}\;y\;\texttt{=}\;e_1\texttt{;}\;e_2) & \stackrel{\text{\tiny def}}{=}& \mathbf{const}\;y\;\texttt{=}\; ({}[e'/x]e_1) \texttt{;}\; ({}[e'/x]e_2) & \text{if $x\neq y$} \\[1ex] {}[e'/x] (\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) & \stackrel{\text{\tiny def}}{=}& \texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 & \text{if $x= y$} \\ {}[e'/x] (\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) & \stackrel{\text{\tiny def}}{=}& \texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} ({}[e'/x]e_1) & \text{if $x\neq y$} \\[1ex] {}[e'/x] (y_1\texttt{(}y_2\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) & \stackrel{\text{\tiny def}}{=}& y_1\texttt{(}y_2\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1 & \text{if $x= y_1$ or $x= y_2$} \\ {}[e'/x] (y_1\texttt{(}y_2\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) & \stackrel{\text{\tiny def}}{=}& y_1\texttt{(}y_2\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} ({}[e'/x]e_1) & \text{if $x\neq y_1$ and $x\neq y_2$} \\[1ex] {}[e'/x]n & \stackrel{\text{\tiny def}}{=}& n\\ {}[e'/x]b & \stackrel{\text{\tiny def}}{=}& b\\ {}[e'/x](\mathop{\mathit{uop}}e_1) & \stackrel{\text{\tiny def}}{=}& \mathop{\mathit{uop}}({}[e'/x]e_1) \\ {}[e'/x](e_1 \mathbin{\mathit{bop}}e_2) & \stackrel{\text{\tiny def}}{=}& ({}[e'/x]e_1) \mathbin{\mathit{bop}}({}[e'/x]e_2) \\ {}[e'/x] (e_1\;\texttt{?}\;e_2\;\texttt{:}\;e_3) & \stackrel{\text{\tiny def}}{=}& {}[e'/x]e_1 \;\texttt{?}\; {}[e'/x]e_2 \;\texttt{:}\; {}[e'/x]e_3 \\ {}[e'/x] (e_1\texttt{(}e_2\texttt{)}) & \stackrel{\text{\tiny def}}{=}& ({}[e'/x]e_1) \texttt{(}{}[e'/x]e_2\texttt{)} \end{array} \]

Figure 21.1: Defining substitution assuming $e$ and $e'$ use disjoint sets of bound variables.

In Figure 21.1, we define substitution ${}[e'/x]e$ by induction over the structure of expression $e$. As a pre-condition, we assume that $e$ and $e'$ use disjoint sets of bound variables. This pre-condition can always be satisfied by renaming bound variables in $e$ appropriately as described above. Or if we require that $e'$ has to be a closed expression, then this pre-condition is trivally satisfied. The most interesting cases are for variable uses and bindings. For variable uses, we yield $e'$ if the variable matches the variable being substituted for; otherwise, we leave the variable use unchanged. For a $\mathbf{const}$-binding $\mathbf{const}\;y\;\texttt{=}\;e_1\texttt{;}\;e_2$, we recall that the scope of $x_1$ is $e_2$, so we substitute in $e_2$ depending on whether or not $x= y$. Observe that the same reasoning applies to function literals $x^{?}\texttt{(}y\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1$. The remaining expression forms simply “pass through” the substitution.

def substitute(with_e: Expr, x: String, in_e: Expr) = {
  require((freeVars(with_e) intersect freeVars(in_e)).isEmpty)
  def subst(in_e: Expr): Expr = in_e match {
    case Var(y) => if (x == y) with_e else in_e
    case ConstDecl(y, e1, e2) =>
      if (x == y) ConstDecl(y, subst(e1), e2) else ConstDecl(y, subst(e1), subst(e2))
    case Fun(yopt, y, e1) =>
      if (Some(x) == yopt || x == y) in_e else Fun(yopt, y, subst(e1))
    case N(_) | B(_) => in_e
    case Unary(uop, e1) => Unary(uop, subst(e1))
    case Binary(bop, e1, e2) => Binary(bop, subst(e1), subst(e2))
    case If(e1, e2, e3) => If(subst(e1), subst(e2), subst(e3))
    case Call(e1, e2) => Call(subst(e1), subst(e2))
  }
  subst(in_e)
}

defined function substitute

def toBoolean(e: Expr): Boolean = {
  require(isValue(e))
  e match {
    case B(b) => b
    case N(n) if (n compare 0.0) == 0 || (n compare -0.0) == 0 || n.isNaN => false
    case _ => true
  }
}

def step(e: Expr) = {
  require(closed(e), s"$e should be closed")
  def step(e: Expr): Either[DynamicTypeError, Expr] = {
    require(!isValue(e), s"$e should not be a value")
    e match {
      // DoNeg
      case Unary(Neg, N(n1)) => Right(N(-n1))
      // DoPlus
      case Binary(Plus, N(n1), N(n2)) => Right(N(n1 + n2))

      // DoNot
      case Unary(Not, v1) if isValue(v1) => Right(B(toBoolean(v1)))
      // DoAndTrue and DoAndFalse
      case Binary(And, v1, e2) if isValue(v1) => Right(if (toBoolean(v1)) e2 else v1)
      // DoOrTrue and DoOrFalse
      case Binary(Or, v1, e2) if isValue(v1) => Right(if (toBoolean(v1)) v1 else e2)
      // DoIf
      case If(v1, e2, e3) if isValue(v1) => Right(if (toBoolean(v1)) e2 else e3)
      // DoEquality
      case Binary(Eq, v1, v2) if isValue(v1) && isValue(v2) => Right(B(v1 == v2))

      // DoConstDecl
      case ConstDecl(x, v1, e2) if isValue(v1) => Right(substitute(v1, x, e2))
      // DoCall and DoCallRec
      case Call(v1 @ Fun(xopt, y, e1), v2) if isValue(v2) => {
        val e1_ = substitute(v2, y, e1)
        Right(xopt match {
          case None => e1_
          case Some(x) => substitute(v1, x, e1_)
        })
      }

      // SearchUnary and PropagateUnary
      case Unary(uop, e1) => step(e1) map { e1 => Unary(uop, e1) }
      // SearchBinary2 and PropagateBinary2
      case Binary(bop, v1, e2) if isValue(v1) => step(e2) map { e2 => Binary(bop, v1, e2) }
      // SearchBinary1 and PropagateBinary1
      case Binary(bop, e1, e2) => step(e1) map { e1 => Binary(bop, e1, e2) }

      // SearchIf and PropagateIf
      case If(e1, e2, e3) => step(e1) map { e1 => If(e1, e2, e3) }

      // SearchConstDecl and PropagateConstDecl
      case ConstDecl(x, e1, e2) => step(e1) map { e1 => ConstDecl(x, e1, e2) }

      // SearchCall2 and PropagateCall2
      case Call(v1, e2) if isValue(v1) => step(e2) map { e2 => Call(v1, e2) }

      // TypeErrorNeg
      case Unary(Neg, v1) if isValue(v1) => Left(DynamicTypeError(e))
      // TypeErrorPlus1
      case Binary(Plus, v1, _) if isValue(v1) => Left(DynamicTypeError(e))
      // TypeErrorPlus2
      case Binary(Plus, _, v2) if isValue(v2) => Left(DynamicTypeError(e))
      // TypeErrorCall
      case Call(v1, _) if isValue(v1) => Left(DynamicTypeError(e))

      // Anything else is an implementation bug
    }
  }
  step(e)
}

val e_closedSillyRecFun = ConstDecl("j", N(1), Call(e_sillyRecFun, N(3)))
val Right(e_oneStepClosedSillyRecFun) = step(e_closedSillyRecFun)
val Right(e_twoStepsClosedSillyRecFun) = step(e_oneStepClosedSillyRecFun)

defined function toBoolean
defined function step
e_closedSillyRecFun: ConstDecl = ConstDecl(
  x = "j",
  e1 = N(n = 1.0),
  e2 = Call(
    e1 = Fun(
      xopt = Some(value = "silly"),
      y = "i",
      e1 = If(
        e1 = Binary(bop = Eq, e1 = Var(x = "i"), e2 = N(n = 0.0)),
        e2 = Var(x = "j"),
        e3 = Binary(
          bop = Plus,
          e1 = Var(x = "j"),
          e2 = Call(
            e1 = Var(x = "silly"),
            e2 = Binary(
              bop = Plus,
              e1 = Var(x = "i"),
              e2 = Unary(uop = Neg, e1 = N(n = 1.0))
            )
          )
        )
      )
    ),
    e2 = N(n = 3.0)
  )
)
e_oneStepClosedSillyRecFun: Expr = Call(
  e1 = Fun(
    xopt = Some(value = "silly"),
    y = "i",
    e1 = If(
      e1 = Binary(bop = Eq, e1 = Var(x = "i"), e2 = N(n = 0.0)),
      e2 = N(n = 1.0),
      e3 = Binary(
        bop = Plus,
        e1 = N(n = 1.0),
        e2 = Call(
          e1 = Var(x = "silly"),
          e2 = Binary(
            bop = Plus,
            e1 = Var(x = "i"),
            e2 = Unary(uop = Neg, e1 = N(n = 1.0))
          )
        )
      )
    )
  ),
  e2 = N(n = 3.0)
)
e_twoStepsClosedSillyRecFun: Expr = If(
  e1 = Binary(bop = Eq, e1 = N(n = 3.0), e2 = N(n = 0.0)),
  e2 = N(n = 1.0),
  e3 = Binary(
    bop = Plus,
    e1 = N(n = 1.0),
    e2 = Call(
      e1 = Fun(
        xopt = Some(value = "silly"),
        y = "i",
        e1 = If(
          e1 = Binary(bop = Eq, e1 = Var(x = "i"), e2 = N(n = 0.0)),
          e2 = N(n = 1.0),
          e3 = Binary(
            bop = Plus,
            e1 = N(n = 1.0),
            e2 = Call(
              e1 = Var(x = "silly"),
              e2 = Binary(
                bop = Plus,
                e1 = Var(x = "i"),
                e2 = Unary(uop = Neg, e1 = N(n = 1.0))
              )
            )
          )
        )
      ),
      e2 = Binary(
        bop = Plus,
        e1 = N(n = 3.0),
        e2 = Unary(uop = Neg, e1 = N(n = 1.0))
      )
    )
  )
)

21.10 Multi-Step Reduction

We have now defined how to take one-step of evaluation (without $\mathsf{typeerror}$), namely a judgment of the form $e \longrightarrow e'$. The multi-step reduction judgment form \[ e\longrightarrow^{\ast}e' \] says, “Expression $e$ can step to expression $e'$ in zero-or-more steps.” This judgment is defined using the following two rules:

$\fbox{$e\longrightarrow^{\ast}e'$}$

$\inferrule[MultiStepZero]{ }{ e\longrightarrow^{\ast}e }$

$\inferrule[MultiStepAtLeastOne]{ e\longrightarrow e' \and e' \longrightarrow^{\ast}e'' }{ e\longrightarrow^{\ast}e'' }$

In other words, $e\longrightarrow^{\ast}e'$ is the reflexive-transitive closure of $e\longrightarrow e'$.

A property that we want is that our big-step semantics and our small-step semantics are “the same.” We can state this property formally as follows:

Proposition 21.2 (Big-Step and Small-Step Equivalence) $\cdot \vdash e \Downarrow v$ if and only if $e\longrightarrow^{\ast}v$.

The multi-step reduction judgment form $e\longrightarrow^{\ast}e'$ enables us to state when an expression $e'$ is reachable under some number of steps from $e$ (i.e., $e\longrightarrow\cdots$).

At the same time, we have implicitly assumed that there is a top-level or outer loop that repeatedly applies a step until reaching a value or $\mathsf{typeerror}$. Let us a define a judgment for $e \hookrightarrow r$ that says, “Evaluation $e$ reduces to a result $r$ that is either a value or a $\mathsf{typeerror}$ using some number of steps.”

$\fbox{$e \hookrightarrow r$}$

$\inferrule[ReducesToValue]{ e\;\mathsf{value} }{ e \hookrightarrow e }$

$\inferrule[ReducesToTypeError]{ e \longrightarrow \mathop{\mathsf{typeerror}}e' }{ e \hookrightarrow \mathop{\mathsf{typeerror}}e' }$

$\inferrule[ReducesToStep]{ e \longrightarrow e' \and e' \hookrightarrow r }{ e \hookrightarrow r }$

And let us implement $e \hookrightarrow r$ as follows with iterateStep:

def iterateStep(e: Expr): Either[DynamicTypeError, Expr] =
  // ReducesToValue
  if (isValue(e)) Right(e)
  else step(e) match {
    // ReducesToTypeError
    case Left(error) => Left(error)
    // ReducesToStep
    case Right(e) => iterateStep(e)
  }

defined function iterateStep

Note again the passthrough case Left(error) => Left(error). The Either[Err, A] type has a method flatMap similar to the map method, except it permits its callback to also “fail.” We can thus refactor iterateStep as follows using flatMap:

def iterateStep(e: Expr): Either[DynamicTypeError, Expr] =
  // ReducesToValue
  if (isValue(e)) Right(e)
  // ReducesToTypeError and ReducesToStep
  else step(e) flatMap iterateStep

defined function iterateStep

That is, if either step or iterateStep “fails” by returning a Left value, that Left will be returned. Otherwise, the resulting Expr from a “successful” step(e) was passed to iterateStep.

Let’s run an integration test for step from iterateStep:

iterateStep(e_closedSillyRecFun)

res22: Either[DynamicTypeError, Expr] = Right(value = N(n = 4.0))

One benefit of the small-step semantics is that we can easily log the intermediate steps of reduction:

def iterateStep(e: Expr) = {
  println(e)
  def loop(e: Expr): Either[DynamicTypeError, Expr] =
    // ReducesToValue
    if (isValue(e)) Right(e)
    // ReducesToTypeError and ReducesToStep
    else step(e) flatMap { e => println(s"--> $e"); loop(e) }
  loop(e)
}

iterateStep(e_closedSillyRecFun)

ConstDecl(j,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),Var(j),Binary(Plus,Var(j),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),N(3.0)))
--> Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),N(3.0))
--> If(Binary(Eq,N(3.0),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(3.0),Unary(Neg,N(1.0))))))
--> If(B(false),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(3.0),Unary(Neg,N(1.0))))))
--> Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(3.0),Unary(Neg,N(1.0)))))
--> Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(3.0),N(-1.0))))
--> Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),N(2.0)))
--> Binary(Plus,N(1.0),If(Binary(Eq,N(2.0),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(2.0),Unary(Neg,N(1.0)))))))
--> Binary(Plus,N(1.0),If(B(false),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(2.0),Unary(Neg,N(1.0)))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(2.0),Unary(Neg,N(1.0))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(2.0),N(-1.0)))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),N(1.0))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),If(Binary(Eq,N(1.0),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(1.0),Unary(Neg,N(1.0))))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),If(B(false),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(1.0),Unary(Neg,N(1.0))))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(1.0),Unary(Neg,N(1.0)))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(1.0),N(-1.0))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),N(0.0)))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Binary(Plus,N(1.0),If(Binary(Eq,N(0.0),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(0.0),Unary(Neg,N(1.0)))))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Binary(Plus,N(1.0),If(B(true),N(1.0),Binary(Plus,N(1.0),Call(Fun(Some(silly),i,If(Binary(Eq,Var(i),N(0.0)),N(1.0),Binary(Plus,N(1.0),Call(Var(silly),Binary(Plus,Var(i),Unary(Neg,N(1.0))))))),Binary(Plus,N(0.0),Unary(Neg,N(1.0)))))))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),Binary(Plus,N(1.0),N(1.0))))
--> Binary(Plus,N(1.0),Binary(Plus,N(1.0),N(2.0)))
--> Binary(Plus,N(1.0),N(3.0))
--> N(4.0)

defined function iterateStep
res23_1: Either[DynamicTypeError, Expr] = Right(value = N(n = 4.0))

## JavaScripty: Variables, Numbers, Booleans, Functions, and Strings