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