DOKK Library
     A Stepper for a Functional JavaScript Sublanguage
                                                                          Martin Henz
                                                                          Thomas Tan
                                                                         Zachary Chua
                                                                           Peter Jung
                                                                          Yee-Jian Tan
                                                                          Xinyi Zhang
                                                                         Jingjing Zhao
                                            National University of Singapore (NUS)

                Figure 1. The stepper, showing the step just after the third call of factorial, written in JavaScript.

Abstract                                                                                  Source ğ2 programs. To support the learner in adopting this
The first two chapters of the introductory computer science                               mental model, we built an algebraic stepperÐa tool for visu-
textbook Structure and Interpretation of Computer Programs,                               alizing the evaluation of Source ğ2 programs according to
JavaScript Edition (SICP JS), use a subset of JavaScript called                           the model. As a sublanguage of JavaScript, Source ğ2 differs
Source ğ2. The book introduces the reduction-based łsubsti-                               from other purely functional programming languages by us-
tution modelž as a first mental model for the evaluation of                               ing a statement-oriented syntax, with statement sequences,
                                                                                          return statements, and block-scoped declarations. For the
Permission to make digital or hard copies of part or all of this work for
                                                                                          purpose of this tool description, we distill these distinguish-
personal or classroom use is granted without fee provided that copies are                 ing featuresÐalong with explicit recursionÐinto a Source ğ2
not made or distributed for profit or commercial advantage and that copies                sublanguage that we call Source ğ0, and focus on a stepper for
This this notice
       work    is and  the full under
                    licensed    citation aon Creative
                                             the first page. Copyrights
                                                        Commons         for third-
                                                                    Attribution-          this language. We formalize the substitution model of Source
party components
ShareAlike           of this work
             4.0 International     must be honored. For all other uses, contact
                                                                                          ğ0 as a lambda-calculus-style reduction semantics that han-
the owner/author(s).
                                                                                          dles explicit recursion by term graph rewriting and faithfully
SPLASH-E ’21, October 20, 2021, Chicago, IL, USA
© 2021 Copyright held by the owner/author(s).
                                                                                          implements the JavaScript specification, when restricted to
ACM ISBN 978-1-4503-9089-7/21/10.                                                         that language. Our implementation of the stepper represents                                                   term graphs by persistent data structures that maximize

SPLASH-E ’21, October 20, 2021, Chicago, IL, USA   Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Yee-Jian Tan, Xinyi Zhang, and Jingjing Zhao

sharing and enable random access to all steps. This work                      prog    ::= stmt . . .                      program
presents the first reduction-based semantics for a JavaScript
                                                                              stmt    ::= function name
sublanguage and the first algebraic stepper for a language
with return statements and block-scoped declarations. The                                    ( names ) block              function decl.
tool supports the learner with step-level explanations, redex                            |   return expr ;                return statement
highlighting, and function-level skipping and can also be                                |   expr ;                       expression st’ment
used for teaching the applicative-order-reduction lambda
calculus.                                                                   names     ::= 𝜖 | name ( , name ) . . . parameters

CCS Concepts: · Software and its engineering → Inte-                         block    ::= { prog }                        function body
grated and visual development environments; · Applied                         expr    ::= number | true | false
computing → Computer-assisted instruction; · Theory
                                                                                         |   undefined                    literal expression
of computation → Lambda calculus.
                                                                                         |   name                         name expression
Keywords: programming environments, education, function-
                                                                                         |   expr bin-op expr             binary op. comb.
al languages, lambda calculus, semantics, JavaScript, stepper,
term graph rewriting                                                                     |   expr ( exprs )               function appl.
ACM Reference Format:                                                                    |   expr ? expr : expr           conditional expr.
Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Yee-Jian Tan,                         |   ( expr )                     parenthesized expr.
Xinyi Zhang, and Jingjing Zhao. 2021. A Stepper for a Functional
JavaScript Sublanguage. In Proceedings of the 2021 ACM SIGPLAN              bin-op ::= + | - | * | / | ===
International SPLASH-E Symposium (SPLASH-E ’21), October 20,                             |   > | < | >= | <=              binary operator
2021, Chicago, IL, USA. ACM, New York, NY, USA, 11 pages. https:
//                                            exprs    ::= 𝜖 | expr ( , expr ) . . .       argument expr’s

1 Introduction                                                              Figure 2. Source ğ0 in Backus-Naur Form [18]; bold font
                                                                            for keywords, italics for syntactic variables, 𝜖 for nothing,
A hallmark of the introductory computer science textbook
                                                                            𝑥 | 𝑦 for 𝑥 or 𝑦, and ( 𝑥 ) . . . for zero or more repetitions of 𝑥.
Structure and Interpretation of Computer Programs (SICP, [1])
is its functional-programming-first approach. Computation
is introduced as a step-by-step process of simplification and
                                                                            semantics. Section 5 outlines how this semantics is imple-
function unfolding, reminiscent of familiar mental models in
                                                                            mented in our stepper and how the tool is integrated in
mathematical calculation and equation solving. In the book,
                                                                            the Source Academy, our online environment for teaching
this process is called the substitution model, and can in princi-
                                                                            SICP JS [23]. Section 6 gives example sessions of the step-
ple explain the evaluation of all programs in its first two chap-
                                                                            per to illustrate its basic features. Section 7 introduces the
ters. The JavaScript adaptation of SICPÐSICP JS [2]Ðuses
                                                                            advanced feature of function skipping, demonstrates its use
JavaScript for all programs instead of the language Scheme
                                                                            and discusses its implementation. Numerous stepper tools
used in the first two editions of SICP. JavaScript employs
                                                                            and systems for designing and implementing such tools are
a statement-oriented syntax, which is the syntactic style
                                                                            presented in the literature. In Section 8, we compare the most
of most mainstream languages as of 2021, including Java,
                                                                            closely related systems to our approach, before concluding
Python, and C, rather than Scheme’s expression-oriented
                                                                            and discussing planned extensions in Section 9.
syntax. The most significant change in the first two chapters
                                                                               The stepper is implemented in an open-source program-
of SICP JS, compared to SICP, is the use of return statements
                                                                            ming environment custom-built for first-year students. The
and block-scoped declarations.
                                                                            beginning of Section 6 explains how to use the system and
   While teaching Computer Science first-year students us-
                                                                            how to navigate to the stepper.
ing SICP JS, we saw the need for a tool that explains the
evaluation of programs in the first two chapters accord-
ing to the substitution model. Existing JavaScript imple-                   2 Syntax of Source §0
mentations, including the browsers’ JavaScript debugging                    To focus on the distinguishing features of the stepper, Fig-
tools, are not suitable for this task, because the substitu-                ure 2 specifies a Source ğ2 sublanguage that we call Source
tion model radically differs from their underlying computa-                 ğ0. We limit the discussion in this section and Sections 3
tional models. Section 2 specifies Source ğ0, a sublanguage                 and 4 to Source ğ0 to avoid excessive formalism in this tool
of JavaScript that includes the most important features that                description. The full language Source ğ2Ðspecified in [16]Ð
distinguish JavaScript from Scheme. Section 3 specifies its                 adds blocks as statements, constant declarations, conditional
formal, lambda-calculus-style reduction semantics, and Sec-                 statements, lambda expressions, unary operators, more bi-
tion 4 describes the notion of substitution employed in the                 nary operators, strings, and pairs as primitive data structures.

A Stepper for a Functional JavaScript Sublanguage                                          SPLASH-E ’21, October 20, 2021, Chicago, IL, USA

A full Source ğ2 stepper is implemented in the Source Acad-            that 𝑝𝑛 → 𝑞. If 𝑝𝑛 is of the form 𝑣;, we call 𝑣 the result
emy and described in [9].                                              of the program evaluation. If 𝑝𝑛 is the empty sequence of
  In the Source languages, the bodies of functions are blocks,         statements, we declare the result of the program evaluation
which may contain return statements and expression state-              to be the value undefined. Reduction can get łstuckž; the
ments in any position, as illustrated by the following (some-          result can be a program that has neither of these two forms,
what contrived) example program, which we will call f-apply.           which corresponds to a runtime error, for example when a
                                                                       function is used as an operand of the arithmetic operation *.
function f(x) { 17; return x + 1; 57; }
2 + 3; f (4 * 5) - 6;                                                  3.1  Operator Combinations, Conditionals, and
   The first two chapters of SICP JS adhere to purely func-                 Sequences
tional programming (no assignment, stateful operations or              The rules Op-Comb-Intro (OCI1, OCI2), Op-Comb-Red (OCR),
loops), and rely on (mutual) recursion as the central means            Cond-Intro (CI), and Cond-Red (CR1, CR2) implement the
of control flow. In the following example program, which we            binary operator combinations and conditional expressions
will call even-odd, the declarations of the mutually recursive         of Source ğ0.
functions even and odd are followed by the application of                                     𝑒 1 → 𝑒 1′
even to the literal 5.                                                                                              [OCI1]
                                                                                   𝑒 1 bin-op 𝑒 2 → 𝑒 1′ bin-op 𝑒 2
function even (n) {                                                                            𝑒 2 → 𝑒 2′
     return n === 0 ? true : odd (n - 1);                                                                            [OCI2]
                                                                                    𝑣 bin-op 𝑒 2 → 𝑣 bin-op 𝑒 2′
function odd (n) {                                                                   𝑣 is result of 𝑣 1 bin-op 𝑣 2
     return n === 0 ? false : even (n - 1);                                               𝑣 1 bin-op 𝑣 2 → 𝑣
}                                                                                                𝑒 1 → 𝑒 1′
even (5);                                                                            𝑒 1 ? 𝑒 2 : 𝑒 3 → 𝑒 1′ ? 𝑒 2 : 𝑒 3
   In JavaScript (and Source), the scope of a function declara-                                 [CR1]                              [CR2]
tion is the surrounding block, or the whole program if there           true ? 𝑒 1 : 𝑒 2 → 𝑒 1            false ? 𝑒 1 : 𝑒 2 → 𝑒 2
is no surrounding block as in this case. As in JavaScript, we          Our proof trees identify in square brackets each rule being
stipulate that function declarations are moved (łhoistedž) to          applied. The base case at the top of a tree is always a reduc-
the beginning of the block or program, as a preprocessing              tion rule ...-Red rule (...R...).
                                                                                    1 + 2→3
3 Reduction                                                                                                   [OCI1]
                                                                                3 === 1 + 2 → 3 === 3
In this section, we define a reduction relation →∗ that de-                                                                   [CI]
                                                                       3 === 1 + 2 ? 17 : 42 → 3 === 3 ? 17 : 42
scribes the evaluation of Source ğ0 programs. The stepper
                                                                         The program component where a reduction rule can be
visualizes the evaluation process. The reduction of the even-
                                                                       applied is called a redex. JavaScript semantics prescribes that
odd program above will include the following steps; the exact
                                                                       there is at most one redex in any program with only one
shapes of even and odd during reduction are explained in
                                                                       applicable rule, and therefore → must be a function. The re-
Section 3.2.
                                                                       dexes of our example proof trees of Section 3 are highlighted
   even-odd                                                            with a gray background.
→∗ even(5);    →∗ 5 === 0 ? true : odd(5 - 1);
                                                                       Expression-Statement-Intro (ESI): An expression statement as
→ odd(5 - 1); →∗ 4 === 0 ? false : even(4 - 1);
                                                                       first statement in a statement sequence can be reduced if the
→∗ odd(1 - 1); →∗ 0 === 0 ? false : even(0 - 1);
                                                                       expression can be reduced.
→∗ false;
                                                                                             expr → expr ′
   We will define the one-step reduction function → as a                                                        [ESI]
                                                                                      expr; prog → expr ′; prog
partial function from programs/statements/expressions to
programs/statements/expressions, and →∗ as its reflexive               First-Statement-Red (FSR), First-Statement-Intro (FSI): The
transitive closure. The one-step reduction function is the             JavaScript specification [15] categorizes statement sequences
least relation that meets all rules given in this section using        statically as value-producing (in our case: sequences contain-
Gentzen-style. A value is a literal expression or a recursive          ing expression or return statements) and not value-producing
function definition (introduced in Section 3.2), and values            (in our case: sequences of declarations). A statement 𝑣; in
are denoted with the letter 𝑣 in the following.                        front of a value-producing statement sequence is discarded,
   A reduction is a sequence of programs 𝑝 1 → 𝑝 2 → · · · →           and a statement 𝑣; in front of a not value-producing state-
𝑝𝑛 , where 𝑝𝑛 is not reducible, i.e. there is no program 𝑞 such        ment sequence is retained.

SPLASH-E ’21, October 20, 2021, Chicago, IL, USA   Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Yee-Jian Tan, Xinyi Zhang, and Jingjing Zhao

   The rule FSI explains why the final value of a program                   function odd (n) { (𝜇 even .( n) => {
is retained, the remaining not value-producing statement                      return n === 0          return n === 0
sequence being the empty sequence in this case. In Source ğ2,                  ? false                  ? true
the FSI rule also explains why the value of the program                        : (𝜇 even .( n) => { : (𝜇 odd .( n) => {
                                                                                    return n === 0          return n === 0
1; const x = 0;                                                                       ? true                  ? false
                                                                                      : odd (n - 1);          : (𝜇 even .( n) => {
is 1 and not undefined.                                                            })                             return n === 0
                                                                                   (n - 1);           →FDR
                                                                                                                    ? true
                 prog is value-producing                                    }
                                         [FSR]                                                                      : odd (n - 1);
                     v; prog → prog                                         (𝜇 even .( n) => {                   })
                                                                               return n === 0                   (n - 1);
                                                                                 ? true                    })
      prog → prog ′ and prog is not value-producing                              : odd (n - 1);
                                                    [FSI]                                                 (n - 1);
                   v; prog → v; prog ′                                        })                     })
                                                                            (5);                   (5);
Two steps from the reduction of f-apply illustrate some of                  Function-application-Red (FR): JavaScript’s specification [15]
the rules introduced so far; the shape of fun is explained in               stipulates applicative-order reduction and thus, the applica-
Section 3.2.                                                                tion of a function can be reduced, only if all arguments are
                                   [OCR]                                    values. Since all function declarations substitute the function
                     2 + 3→5                                                name by a 𝜇-term, we combine 𝛽-reduction of the lambda
                                                             [ESI]          calculus with the 𝜇-rule, stated in [3] in the context of the
 2 + 3; fun(4 * 5) - 6; → 5; fun(4 * 5) - 6;
                                                                            𝜆𝜇-calculus: 𝜇𝑥 .𝑍 → 𝑍 [𝑥 ← 𝜇𝑥 .𝑍 ]
                                                                                              expr = 𝜇 𝑓 .( 𝑥 1 . . . 𝑥𝑛 ) => block
                                                        [FSR]               expr(𝑣 1 . . . 𝑣𝑛 ) → block[𝑥 1 ← 𝑣 1 ]. . .[𝑥𝑛 ← 𝑣𝑛 ] [𝑓 ← expr]
       5; fun(4 * 5) - 6; → fun(4 * 5) - 6;
                                                                            This rule [FR] introduces a block expression, the second new
3.2    Function Declaration and Application                                 kind of expressions that is not part of Source ğ0:
Function-Declaration-Red (FDR): Function declarations are                               expr    ::=   block       block expression
reduced as follows.
                                                                            The result of the second step in the reduction of even-odd is
                                                              [FDR]         further reduced with FR (with no free occurrences of even to
function f (names) block prog                                               be unfolded), and then with BER3 (which we will introduce
              → prog[f ← 𝜇 𝑓 .(names) => block]                             in Section 3.3):
Here, 𝜇-terms [3] are used to represent recursive function
                                                                             return 5 === 0           5 === 0
definitions. They are not part of Source ğ0, but appear during
                                                                               ? true                 ? true
                                                                               : (𝜇 odd .( n) => {    : (𝜇 odd .( n) => {
                                                                                    return n === 0         return n === 0
expr ::= 𝜇 name.( names ) => block            recursive funct. def.
                                                                                     ? false                 ? false
                                                                                     : (𝜇 even .( n) => { : (𝜇 even .( n) => {
Every occurrence of name in block represents the recursive
                                                                                         return n === 0          return n === 0
function definition itself, and thus can be seen as a cycle in
                                                                            →FR,ESI        ? true      →BER3,ESI ? true
the expression. Here, 𝑡 [𝑥 ← 𝑠] denotes the capture-avoiding
                                                                                           : odd (n - 1);          : odd (n - 1);
substitution of 𝑠 for 𝑥 in 𝑡 (details in Section 3.2), according
                                                                                        })                      })
to the following scoping rules. In JavaScript [15], the scope
                                                                                       (n - 1);                (n - 1);
of a function declaration is the surrounding block or the
                                                                                  })                      })
whole program if there is no surrounding block, and the
                                                                                 (5 - 1);               (5 - 1);
scope of parameters is the function body. The scope of name
in 𝜇 name.( names ) => block is block.
   The first two reduction steps for the even-odd program                   Function-application-Intro (FI1, FI2): The application intro-
illustrate how function declarations give rise to cyclic recur-             duction rules stipulate strict, left-to-right reduction of the
sive function definitions.                                                  components of function applications, following JavaScript’s
even-odd →FDR                                                               specification [15].

A Stepper for a Functional JavaScript Sublanguage                                                            SPLASH-E ’21, October 20, 2021, Chicago, IL, USA

         expr → expr ′                                                                   the component to be substituted into a name binder con-
                                  [FI1]                                                  tains one of the binder’s names as a free name. In Source ğ0,
expr ( exprs ) → expr ′ ( exprs )
                                                                                         name binders are function declarations, whose parameters
                             expr → expr ′                                               are binding, blocks, whose function declarations are binding,
                                                                            [FI2]        and 𝜇-terms of the form 𝜇 name.(names) => block, where
𝑣 ( 𝑣 1, . . . , 𝑣𝑖 , expr, . . . ) → 𝑣 ( 𝑣 1, . . . , 𝑣𝑖 , expr ′, . . . )
                                                                                         name and all names in names are binding. Capture-avoiding
3.3 Block Expressions                                                                    substitution of an expression e for a name 𝑦 in a 𝜇-term is
The rule FR gives rise to block expressions, which are blocks                            defined as follows:
that appear as expressions as a result of the unfolding of a                                                      
                                                                                                                   (𝜇z.(names) =>
function application expression.                                                                                  
                                                                                                                         block[x ← 𝑧]) [𝑦 ← 𝑒]
                                                                                                                   if x occurs free in 𝑒
Block-Expression-Intro/Reduce (BEI, BER1, BER2): A block                                                          
                                                                                                                                ′
expression is reducible if its body is reducible. A block ex-                             (𝜇x.(names) => block)    (𝜇z.(names ) =>
pression whose body is the empty statement sequence or                                                          =         block[n ← 𝑧]) [𝑦 ← 𝑒]
                                                                                                       [𝑦 ← 𝑒]    
only contains a single value statement reduces to the value                                                       
                                                                                                                   if 𝑛 ∈ names occurs free in 𝑒
undefined.                                                                                                        
                                                                                                                   𝜇𝑥 .(names) =>
       prog → prog ′                                                                                              
                         [BEI]                        [BER1]                                                      
                                                                                                                                  block[𝑦 ← 𝑒]
                                   { } → undefined                                                                
   { prog } → { prog ′ }                                                                                           otherwise
                                                  [BER2]                                 where 𝑧 is fresh, neither being 𝑥 nor occurring in names,
                    { 𝑣 ; } → undefined
                                                                                         block or 𝑒, and where names ′ is the result of replacing 𝑛 by 𝑧
BER1 and BER2 reflect that in JavaScript, a function returns
                                                                                         in names. The replacement of 𝑥 or 𝑛 by 𝑧 prior to substitution
the value undefined, if the reduction of the function body
                                                                                         in the first two cases is called alpha-renaming.
does not encounter a return statement, for example:
                                                                                            The rules for avoiding capturing when applying substi-
                                                                                         tution to function declarations and blocks given in [9] sim-
function g(x) { x; } g(5);
                                                                                         ilarly avoid the capturing of free names in the substituted
                                            →∗    { 5; };
                                                                                         components by parameters and local names of the function
                                            →BER2 undefined;
                                                                                         declarations and blocks.
Block-Expression-Red (BER3): A block expression whose body
starts with a return statement reduces to the return expres-                             5 Implementation and Integration
sion of the return statement and ignores any subsequent                                  The Source Academy is web-based, written in TypeScript us-
statements.                                                                              ing React. The TypeScript sources are compiled to JavaScript
                                                                                         and bundled into a web application that gets served to the
                                                            [BER3]                       browser when the learner visits the public website of the
          { return 𝑒𝑥𝑝𝑟 ; stmt . . . } → 𝑒𝑥𝑝𝑟
                                                                                         Source Academy [14]. When the learners select the stepper,
Each line in the following reduction of the example f-apply                              their programs are not executed using the default Source
in Section 2 is annotated by all rules involved in the reduc-                            language implementation but by invoking the stepper com-
tion, and the redexes of ...-Red rules are highlighted.                                  ponent of a collection of open-source implementations of the
                                                                                         Source languages that also includes transpilers to JavaScript,
f-apply   →FDR 2+3; (𝜇f.(x) => { . . . })(4 * 5) - 6;                                    interpreters, compilers and virtual machines.
      →OCR,ESI 5; (𝜇f.(x) => { . . . })(4 * 5) - 6;                                         Upon invoking the stepper, the program is parsed into
      →FSR,ESI (𝜇f.(x) => { . . . })(4 * 5) - 6;                                         an abstract syntax tree (AST) following the ESTree spec of
→OCR,FI2,OCI1,ESI (𝜇f.(x) => { . . . })(20) - 6;                                         the JavaScript syntax [13]. Instead of representing 𝜇-terms
   →FR,OCI1,ESI { 17; return 20 + 1; 57; } - 6;                                          explicitly, we decided to implement back-references to en-
→FSR,BEI,OCI1,ESI { return 20 + 1; 57; } - 6;                                            closing function declarations simply by cyclic references
 →BER3,OCI1,ESI (20 + 1) - 6;                                                            to their nodes in the AST, which as a result is more aptly
      →OCR,ESI 21 - 6;                                                                   called an abstract syntax graph (ASG). The syntax graph of
      →OCR,ESI 15;                                                                       the given program is repeatedly reduced until the result is
                                                                                         reached. The ASGs of all reduction steps are stored in an ar-
4 Capture-Avoiding Substitution                                                          ray, and are converted back into program text in the frontend
As in the lambda calculus, we define substitution by apply-                              of the Source Academy whenever necessary. The learner can
ing substitution rules recursively, following the structure of                           access the steps by dragging a slider or using hotkeys. We ex-
the program. It avoids capturing by alpha-renaming, when                                 tend the ESTree spec for our purpose by allowing cycles and

SPLASH-E ’21, October 20, 2021, Chicago, IL, USA   Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Yee-Jian Tan, Xinyi Zhang, and Jingjing Zhao

coreferences, and by adding block expressions. In the inter-                destructive operations on pairs and thus, the evaluation of
face, we display 𝜇𝑥 .expr simply as 𝑥, so the reduction steps               their programs cannot be explained with a reduction-based
for the even-odd example appear as shown in the beginning                   model.
of Section 3.                                                                  After clicking on the stepper icon (see circle highlighted
   Our implementation of the reduction rules of Section 3                   in white), the evaluation switches to reduction and the REPL
represents ASGs as persistent data structures. In the terminol-             is replaced by the stepper. The learner can set a limit for the
ogy of [11], the ASG is partially persistent during reduction:              number of steps (with a default value of 1000), to handle long
all previous versions of the ASG can be accessed but only                   reductions. Figure 1 above the abstract shows the stepper
the newest version is being modified (constructed). Careful                 after the learner moves the slider to Step 22. Each reduction
implementation of reduction and substitution results in sig-                is shown in two steps: before (even step number) and after
nificant sharing of data structures across the elements of the              (odd step number) the reduction. The redex is highlighted in
array of ASGs. As typical for persistent data structures, a                 red in even-numbered steps and the result of reducing the
reduction step copies only the path from the root node of the               redex is highlighted in green in odd-numbered steps.
program to the redex. Our implementation of substitution                       Each step displays an explanation text below the program.
keeps track of the already processed nodes of the syntax
graph to avoid any repeated application of recursive substi-
tution rules to nodes of cyclic ASGs. Substituted expressions
are shared across the replacements sites, introducing corefer-
ences in the resulting ASG. Coreferences within and sharing
between ASGs enable the greedy generation and retention
in browser memory of all steps of the learner program.
   The run time of the stepper is not perceptible for most
textbook examples and learner programs. In our experience                     Step 22 in Figure 1 shows the program just after the third
of using the stepper in an introductory computer science                    call of factorial. Step 36 below shows the program just
course in NUS, the performance of the stepper is more than                  before the final recursive call of factorial, and the deferred
sufficient. An adjustable step limit allows the learner to play             multiplications that have accumulated during the previous
with non-terminating programs. As a gauge of the stepper’s                  recursive calls.
performance, the evaluation of the following infinite loop
takes 12 seconds with a step limit of 50,000, on a 2.2 GHz
MacBook Pro using the Google Chrome browser Version 20.
function f () { return f (); } f ();

6 Example Sessions                                                            The last step shows the result of factorial(5).
The web-based IDE of the Source Academy lets the learner
enter their programs in an editor on the left. After pressing
łRunž, the program is evaluated and the result is displayed
in a read-eval-print-loop (REPL) on the right, which allows
the learner to test and explore the functions declared in the
                                                                               To save space, we clipped off the display of the explanation
                                                                            in the images below.

                                                                            6.1   Stepping through the Program even-odd
                                                                            We show how the stepper visualizes the evaluation of the
                                                                            even-odd example discussed in Section 3.2.

Selection of the Source language (Source ğ1, ğ2, ğ3, or ğ4,
see oval highlighted in white) restricts the evaluator to only
accept programs of the selected JavaScript sublanguage. The
stepper is available when one of the purely functional Java-
Script sublanguages, Source ğ1 or Source ğ2, is selected. The
languages Source ğ3 and Source ğ4 include assignment and

A Stepper for a Functional JavaScript Sublanguage                                           SPLASH-E ’21, October 20, 2021, Chicago, IL, USA

   The functions even and odd are declared and substituted
into the rest of the program, where even is applied to 5. The
stepper highlights the next expression to be reduced.
   After reducing the declaration function even(n) {...}
with FDR in Section 3.2, the name even in even(n - 1); and
even(5); refers to a 𝜇-term 𝜇 even.expr, which the stepper
represents by just printing even to keep the program read-                The functions even and odd call each other recursively
able.                                                                   until the base case odd(0) is reached. This application is
                                                                        replaced with the return expression of odd, in which the
                                                                        condition 0 === 0 is now reduced to true,...

                                                                        ...finally returning the consequent expression false.

                                                                        6.2   Stepping through the f-apply Program
   When a recursive function definition is applied whose                We illustrate how the stepper visualizes the reduction of the
body consists of a single return statement as in even(5), the           f-apply example given at the end of Section 3.3.
stepper combines FR in Section 3.2 and BER3 in Section 3.3
into a single step. The result in this case is a conditional ex-
pression in which the condition 5 === 0 is reduced to false
with CI in Section 3.1, returning the alternative expression
odd(5 - 1) using CR2 in Section 3.1, which is reduced to

                                                                           The function f is declared and substituted into the rest of
                                                                        the program. After reducing the declaration function f(x)
                                                                        {...} with rule FDR in Section 3.2, the name f refers to a 𝜇-
                                                                        term in f(4 * 5) - 6;, which the stepper displays as just f.

   Similarly, the application of the recursive function defini-         The expression statement 2 + 3; is reduced to 5; using ESI,
tion odd is replaced with the return expression of its body, in         but 5; is discarded using FSR, both in Section 3.1.
which the condition 4 === 0 is reduced to false, returning
the alternative expression even(4 - 1), which is reduced
to even(3).

SPLASH-E ’21, October 20, 2021, Chicago, IL, USA   Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Yee-Jian Tan, Xinyi Zhang, and Jingjing Zhao

The application of f is replaced with the body of f using FR
in Section 3.2, in which all occurrences of x are substituted
by 20. Note the highlighted result showing a block expres-
sion within an operator combination, which is not part of
the JavaScript syntax.

As with 5; in Step 6, the statement 17; is discarded due to

The block expression’s first statement is now a return state-               At Step 10, the functions declarations are all substituted into
ment with the return expression 20 + 1. The block is re-                    the function expression of the final application sqrt(5)...
duced to the return expression due to BER3 in Section 3.3.

The remaining reduction steps are completed and the pro-
gram is reduced to 15;.

                                                                            ...which unfolds the body of the recursive function definition
                                                                            sqrt, resulting in another example of a non-JavaScript block
7 Skipping to Function Applications
The number of steps even for relatively simple textbook
programs can quickly reach several thousand. In addition to
the slider and hotkeys for moving forward and backward by
one step, we decided to support function-level skipping. When
the evaluation of a program reaches a function application
of a function 𝑓 , the learner has in general four options:
    • move to the previous step (if there is one), using a <
    • move to the next step (if there is one), using a > button,
    • take a łbig stepž backward by skipping to the previous
      application of 𝑓 (if there is one), using a ń button, or
    • take a łbig stepž forward by skipping to the next ap-
      plication of 𝑓 (if there is one), using a ż button.
We illustrate this feature using the example of Newton’s
method for computing square roots from Section 1.1.8 of
SICP JS. After running the program with the stepper, it shows                 Reduction continues to the application of sqrt_iter at
the entire program as łStart of evaluationž.                                Step 20.

A Stepper for a Functional JavaScript Sublanguage                                           SPLASH-E ’21, October 20, 2021, Chicago, IL, USA

Using only the arrow button > or hotkeys, the learner would
need to click through a large number of steps...

                                                                        Similarly, the learner may decide to trace the calls of the
                                                                      improve function by repeatedly pressing the ż button, start-
                                                                      ing in Step 42. search for the next call of sqrt_iter. Instead of carry-
ing out small reduction steps, the learner can skip from the
application of sqrt_iter in Step 20... the next application of this function, by pressing the ż
button, highlighted above with a white circle, skipping to
Step 52.                                                              ...followed by sqrt_iter(improve(2.333)); in Step 102
                                                                      and sqrt_iter(improve(2.238)); in Step 132 (not shown).
                                                                          The last call of the function is_good_enough...

  Repeated skipping allows the learner to quickly see the
reduction steps that involve sqrt_iter.
                                                                      ...returns true,...

SPLASH-E ’21, October 20, 2021, Chicago, IL, USA   Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Yee-Jian Tan, Xinyi Zhang, and Jingjing Zhao

...and the reduction terminates with an approximation of 5                  These implementations are based on term (tree) rewriting
to the required accuracy as the result.                                     and not on graph rewriting and do not handle explicit recur-
                                                                            sion, which is necessary for a direct implementation of our
                                                                            reduction semantics. They share with our stepper and with
                                                                            Hat that the intermediate results of a reduction are explicitly
                                                                            generated and stored. As a web-based interactive system
                                                                            written in TypeScript using React, Lambdulus has a similar
                                                                            general system architecture as the Source Academy.
                                                                               Our stepper performs before/after redex highlighting as
   Our implementation of this feature makes use of the shar-                do LambdaLab and Lambdulus. A survey of functional pro-
ing of syntax graphs in the array of graphs. The buttons ń                  gram visualization systems in [24] lists several earlier im-
and ż are rendered as clickable at a function application if a              plementations that share this feature, including the Scheme
previous/following application step is found, whose function                Stepper [10].
expression is the same syntax graph (using pointer equality)                   Chang introduces the JavaScript variant Javascripty [6]
as the function expression of the function application where                in his programming languages course, the only JavaScript-
the search started.                                                         related small-step reduction-based semantics that we are
                                                                            aware of. Javascripty is not designed as a JavaScript sublan-
8 Discussion of Related Work                                                guage. It deviates from JavaScript in the scoping of constant
Algebraic steppers have been developed for many functional                  declarations and supports only a restricted form of return
programming languages, including Scheme [10], Racket [20],                  statements. As opposed to Javascripty [6], our approach
Lazy Racket [7], and Haskell [8]. The Scheme, Racket, and                   handles JavaScript’s statement-oriented syntax, allows re-
Lazy Racket steppers generate a stack of continuations at                   turn statements to occur anywhere in a statement sequence,
run time by instrumenting the learner’s program with łcon-                  and covers JavaScript’s block-scoped declarations.
tinuation marksž in a preprocessing step. In contrast to these
steppers, our stepper directly reduces the given program,
following the presented reduction semantics and resulting                   9 Conclusion and Future Work
in a random-access trace data structure. In this approach, we               This system description presents the first reduction-based
follow Haskell’s stepper, Hat, which stores the full reduction              semantics for a sublanguage of JavaScript and the first al-
trace in a data structure called łaugmented redex trailž. Our               gebraic stepper for a language with return statements and
stepper also shares with Hat the strategy of maximizing shar-               block-scoped declarations. As partially persistent data struc-
ing for space efficiency, which leads in both systems to data               tures, the abstract syntax graphs that represent each step
sharing between steps, coreferences, and cycles and thus                    enjoy significant sharing among each other, and internally
requires term graph rewriting. The direct syntactic represen-               through coreferences and cycles, which enables a memory-
tation of intermediate states simplifies the specification and              efficient implementation. Redex highlighting and function
implementation of the tool and facilitates learner interaction              skipping contribute to the learner’s experience. Since the
but foregoes opportunities for optimized compilation of the                 lambda calculus is a subset of the JavaScript sublanguage
learner program.                                                            covered by the stepper, it can also be used for for teaching
   Broadly speaking, our approach is similar to the way                     applicative-order-reduction lambda calculus and capture-
rewriting-based operational semantics are implemented in                    avoiding substitution.
PLT Redex [12], a general framework for designing program-                     The Source Academy includes a picture language, follow-
ming languages along with their operational semantics. As                   ing Section 2.2.4 of SICP JS, which serves as a prominent
in PLT Redex, we represent the given programs syntactically                 example for the substitution model in our course. Future
during reduction, using the data structures that represent                  versions of the stepper should include an integration of pic-
their components. To maximize data structure sharing, our                   tures in a similar way in which the Racket IDE integrates
data structures represent recursive functions by cycles and                 the pictures generated by its Pict library [19]. In addition to
the instances of parameters by coreferences in their syntax                 function-level skipping, we intend to adopt the fine-grained
graph.                                                                      control provided by Lambdulus [22] using break points that
   As a minimal formal system for computation, the lambda                   are specified by the learner in the program editor.
calculus [4] is used in teaching the theory of computation and                 A specification of the reduction system in Coq [5] or light-
programming language semantics (e.g. [12]), often backed up                 weight mechanization tools (for an overview, see [17]) will
by programming exercises or even complete experimentation                   allow us to mechanize proofs of correctness of the stepper
environments such as LambdaLab [21] and Lambdulus [22].                     or improve testing.

A Stepper for a Functional JavaScript Sublanguage                                                            SPLASH-E ’21, October 20, 2021, Chicago, IL, USA

References                                                                            [12] Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009.
                                                                                           Semantics Engineering with PLT Redex. MIT Press, Cambridge, MA.
 [1] Harold Abelson and Gerald Jay Sussman with Julie Sussman. 1996.                  [13] Github estree repository. 2021. estree.
     Structure and Interpretation of Computer Programs (2nd ed.). MIT Press,               estree.
     Cambridge, MA.                                                                   [14] Github source-academy organization. 2021. Source Academy. https:
 [2] Harold Abelson and Gerald Jay Sussman. 2022. Structure and Interpre-                  //
     tation of Computer Programs, JavaScript edition. MIT Press, Cambridge,           [15] Jordan Harband and Kevin Smith (Eds.). 2020. ECMAScript 2020 Lan-
     MA. Adapted to JavaScript by Martin Henz and Tobias Wrigstad with                     guage Specification (11th ed.). Ecma International, Geneva.
     Julie Sussman.                                                                   [16] Martin Henz, Ning-Yuan Lee, and Daryl Tan. 2021. Specification of
 [3] Zena M. Ariola and Jan Willem Klop. 1997. Lambda Calculus with                        Source ğ2. Technical Report. National University of Singapore. https:
     Explicit Recursion. Information and Computation 139, 2 (December                      //
     1997), 154ś233.                                                                  [17] Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund,
 [4] Hendrik Pieter Barendregt. 2013. The Lambda Calculus: Its Syntax and                  Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, and
     Semantics (2nd ed.). Elsevier Science, Saint Louis, MO.                               Sam Tobin-Hochstadt. 2012. Run your research: on the effective-
 [5] Yves Bertot and Pierre Castéran. 2013. Interactive theorem proving and                ness of lightweight mechanization. In Proceedings of the 39th Annual
     program development: Coq’Art: the calculus of inductive constructions.                ACM SIGPLAN-SIGACT symposium on Principles of programming lan-
     Springer, Berlin/Heidelberg.                                                          guages, Michael Hicks (Ed.). POPL 2012, Philadelphia, PA, 285ś296.
 [6] Bor-Yuh Evan Chang. 2018. Principles and Practice in Programming            
     Languages: A Project-Based Course, University of Colorado, Boulder.              [18] Henry Ledgard. 1980. A human engineered variant of BNF. ACM
     (September 2018).                SIGPLAN Notices 15, 10 (1980), 57ś62.
 [7] Stephen Chang, John Clements, Eli Barzilay, and Matthias Felleisen.                   947732
     2011. Stepping Lazy Programs.                    [19] Racket team. 2021. Pict: Functional Pictures. https://docs.racket-
 [8] Olaf Chitil and Yong Luo. 2007. Structure and Properties of Traces for      
     Functional Programs. Electronic Notes in Theoretical Computer Science            [20] Racket team. 2021. The Stepper.
     176, 1 (2007), 39ś63.                [21] Daniel Sainati and Adrian Sampson. 2018. LambdaLab: An Interac-
 [9] Zachary Chua, Martin Henz, Peter Jung, Thomas Tan, Yee-Jian Tan,                      tive 𝜆-Calculus Reducer for Learning. In Proceedings of the 2018 ACM
     Xinyi Zhang, and Jingjing Zhao. 2021. Specification of Source ğ2 Step-                SIGPLAN Symposium on SPLASH-E, Benjamin Lerner (Ed.). ACM SIG-
     per. Source Academy Specifications. National University of Singapore.                 PLAN, Boston, MA, 10ś19.                             [22] Jan Sliacky and Petr Maj. 2019. Lambdulus: Teaching Lambda Calculus
[10] John Clements, Matthew Flatt, and Matthias Felleisen. 2001. Modeling                  Practically. In Proceedings of the 2019 ACM SIGPLAN Symposium on
     an Algebraic Stepper. In Proceedings of the 10th European Symposium                   SPLASH-E, Elisa Baniassad (Ed.). ACM SIGPLAN, Athens, Greece, 57ś
     on Programming Languages and Systems, ESOP’01 (LNCS), David Sands                     65.
     (Ed.), Vol. 2028. Springer, Berlin, Heidelberg, New York, 320ś334. https:        [23] Source Academy Organization. 2021. Source Academy. https://about.
[11] James Driscoll, Neil Sarnak, Daniel Sleator, and Robert Tarjan. 1986.            [24] J. Urquiza-Fuentes and J. Á. Velázquez-Iturbide. 2004. A Survey of
     Making data structures persistent. In Proceedings of the 18th Annual                  Program Visualizations for the Functional Paradigm. Proceedings of
     ACM Symposium on Theory of Computing, Juris Hartmanis (Ed.). STOC                     the 3rd Program Visualization Workshop, Research Report CS-RR-407.
     1986, Berkeley, CA, 109ś121.                      Department of Computer Science, University of Warwick, 2ś9.


A Stepper for a Functional JavaScript Sublanguage

Authors Jingjing Zhao Martin Henz Peter Jung Thomas Tan Xinyi Zhang Yee-Jian Tan Zachary Chua

License CC-BY-SA-4.0