Authors Jingjing Zhao Martin Henz Peter Jung Thomas Tan Xinyi Zhang Yee-Jian Tan Zachary Chua
License CC-BY-SA-4.0
A Stepper for a Functional JavaScript Sublanguage
Martin Henz
Thomas Tan
Zachary Chua
Peter Jung
Yee-Jian Tan
Xinyi Zhang
Jingjing Zhao
henz@comp.nus.edu.sg,{e0177215,e0543984,e0552326,e0325774,e0424857,e0424694}@u.nus.edu
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
bear
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
License.
ğ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
https://doi.org/10.1145/3484272.3484968 term graphs by persistent data structures that maximize
71
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:
//doi.org/10.1145/3484272.3484968 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.
72
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
[OCR]
return n === 0 ? false : even (n - 1); 𝑣 1 bin-op 𝑣 2 → 𝑣
} 𝑒 1 → 𝑒 1′
[CI]
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...).
step.
[OCR]
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.
73
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
reduction.
: (𝜇 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].
74
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
75
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
program.
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
76
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
odd(4).
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).
77
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
FSR.
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
expression.
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 <
button,
• 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.
78
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.
...in 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...
...to 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,...
79
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.
80
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. https://github.com/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- //github.com/source-academy.
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 //source-academy.github.io/source/source_2.pdf
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 https://doi.org/10.1145/2103656.2103691
Languages: A Project-Based Course, University of Colorado, Boulder. [18] Henry Ledgard. 1980. A human engineered variant of BNF. ACM
(September 2018). https://csci3155.cs.colorado.edu/csci3155-notes.pdf. SIGPLAN Notices 15, 10 (1980), 57ś62. https://doi.org/10.1145/947727.
[7] Stephen Chang, John Clements, Eli Barzilay, and Matthias Felleisen. 947732
2011. Stepping Lazy Programs. http://arxiv.org/abs/1108.4706. [19] Racket team. 2021. Pict: Functional Pictures. https://docs.racket-
[8] Olaf Chitil and Yong Luo. 2007. Structure and Properties of Traces for lang.org/pict.
Functional Programs. Electronic Notes in Theoretical Computer Science [20] Racket team. 2021. The Stepper. https://docs.racket-lang.org/stepper.
176, 1 (2007), 39ś63. https://doi.org/10.1016/j.entcs.2006.10.032 [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. https://doi.org/10.1145/3310089.3313180
https://docs.sourceacademy.org/source_2_stepper.pdf. [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. https://doi.org/10.1145/3358711.3361629
(Ed.), Vol. 2028. Springer, Berlin, Heidelberg, New York, 320ś334. https: [23] Source Academy Organization. 2021. Source Academy. https://about.
//doi.org/10.1007/3-540-45309-1_21 sourceacademy.org.
[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. https://doi.org/10.1145/12130.12142 Department of Computer Science, University of Warwick, 2ś9.
81