Specification of Source §2 Stepper—2022 edition
Martin Henz, Tan Yee Jian, Zhang Xinyi, Zhao Jingjing,
Zachary Chua, Peter Jung, Poomklao Teerawatthanaprapha,
Hao Sitong
National University of Singapore
School of Computing
September 1, 2024
Reduction
The reducer ⇒ is a partial function from programs/statements/expressions to programs/state-
ments/expressions (with slight abuse of notation via overloading) and ⇒
∗
is its reflexive transitive
closure. A reduction is a sequence of programs p
1
⇒ · · · ⇒ p
n
, where p
n
is not reducible, i.e. there
is no program q such that p
n
⇒ q. Here, the program p
n
is called the result of reducing p
1
.
If p
n
, the result of reducing a program, is of the form v;, we call v the result of the program
evaluation. If p
n
is the empty sequence of statements, we declare the result of the program
evaluation to be the value undefined. Reduction can get "stuck": the result can be a program
that has neither of these two forms, which corresponds to a runtime error.
A value is a primitive number expression, primitive boolean expression, a primitive string ex-
pression, a function definition expression or a function declaration expression.
The substitution function p[n := v] on programs/statements/expressions replaces every free oc-
currence of the name n in statement p by value v. Care must be taken to introduce and preserve
co-references in this process; substitution can introduce cyclic references in the result of the
substitution. For example, n may occur free in v, in which case every occurrence of n in p will be
replaced by v such that n in v refers cyclically to the node at which the replacement happens.
Programs
Program-intro: In a sequence of statements, we can always reduce the first one that isn’t a
value statement.
statement ⇒ statement
′
[value;] statement . . . ⇒ [value;] statement
′
. . .
Program-reduce: When the first two statements in a program are value statements, the first one
can be removed.
v1, v2 are values
v1; v2; statement . . . ⇒ v2; statement . . .
Eliminate-function-declaration: Function declarations as the first statement optionally after one
value statement are substituted in the remaining statements.
f = function name ( parameters ) block
[value;] f statement . . . ⇒ [value;] statement . . . [name := f ]
Eliminate-constant-declaration: Constant declarations as the first statement optionally after
one value statement are substituted in the remaining statements.
c = const name = v
[value;] c statement . . . ⇒ [value;] statement . . . [name := v]
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 2
Statements: Expression statements
Expression-statement-reduce: An expression statement is reducible if its expression is reducible.
e ⇒ e
′
e; ⇒ e
′
;
Statements: Constant declarations
Evaluate-constant-declaration: The right-hand expressions in constant declarations are evalu-
ated.
expression ⇒ expression
′
const name = expression ⇒ const name = expression
′
Statements: Conditionals
Conditional-statement-predicate: A conditional statement is reducible if its predicate is reducible.
e ⇒ e
′
if ( e ) { · · · } else { · · · } ⇒ if ( e
′
) { · · · } else { · · · }
SICP-JS Exercise 4.8 specifies that a conditional statement where the taken branch is non-value-
producing is value-producing, with its value being undefined.
Conditional-statement-consequent: Immediately within a program or block statement, a condi-
tional statement whose predicate is true reduces to the consequent block.
if ( true ) { program
1
} else { program
2
} ⇒ { undefined; program
1
}
Conditional-statement-alternative: Immediately within a program or block statement, a condi-
tional statement whose predicate is false reduces to the alternative block.
if ( false ) { program
1
} else { program
2
} ⇒ { undefined; program
2
}
We can remove the undefined; if the conditional statement is in a block expression without
affecting the return value of the block expression. This is performed to reduce the surprise
factor.
Conditional-statement-blockexpr-consequent: Immediately within a block expression, a condi-
tional statement whose predicate is true reduces to the consequent block.
{ [value;] if ( true ) { program
1
} else { program
2
} } ⇒ {[value;] { program
1
}}
Conditional-statement-blockexpr-alternative: Immediately within a block expression, a condi-
tional statement whose predicate is false reduces to the alternative block.
{ [value;] if ( false ) { program
1
} else { program
2
} } ⇒ {[value;] { program
2
}}
Statements: Blocks
Block-statement-intro: A block statement is reducible if its body is reducible.
program ⇒ program
′
{ program } ⇒ { program
′
}
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 3
Block-statement-single-reduce: A block statement consisting of a single value statement re-
duces to that value statement.
{value;} ⇒ value;
Block-statement-empty-reduce: An empty block statement (or a non-value- producing one, which
will reduce to the empty block statement) is non-value-producing, i.e. reduces to ε.
{} ⇒ ε
Expresssions: Blocks
Block-expression-intro: A block expression is reducible if its body is reducible.
program ⇒ program
′
{ program } ⇒ { program
′
}
Block-expression-single-reduce: A block expression consisting of a single value statement re-
duces to undefined.
{value;} ⇒ undefined
Block-expression-empty-reduce: An empty block expression reduces to undefined.
{} ⇒ undefined
Block-expression-return-reduce-1: In a block expression starting with a value statement and
then a return statement, the value statement can be removed.
{value; return return-expression; statement. . .} ⇒ {return return-expression; statement. . .}
Block-expression-return-reduce-2: A block expression starting with a return statement reduces
to the expression of the return statement.
{return return-expression; statement. . . } ⇒ return-expression
Block expressions are currently used only as expanded forms of functions.
Expressions: Binary operators
Left-binary-reduce: An expression with binary operator can be reduced if its left sub-expression
can be reduced.
e
1
⇒ e
′
1
e
1
binary-operator e
2
⇒ e
′
1
binary-operator e
2
And-shortcut-false: An expression with binary operator && whose left sub-expression is false
can be reduced to false.
false && e ⇒ false
And-shortcut-true: An expression with binary operator && whose left sub-expression is true can
be reduced to the right sub-expression.
true && e ⇒ e
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 4
Or-shortcut-true: An expression with binary operator || whose left sub-expression is true can
be reduced to true.
true || e ⇒ true
Or-shortcut-false: An expression with binary operator || whose left sub-expression is false can
be reduced to the right sub-expression.
false || e ⇒ e
Right-binary-reduce: An expression with binary operator can be reduced if its left sub-expression
is a value and its right sub-expression can be reduced.
e
2
⇒ e
′
2
, and binary-operatoris not && or ||
v binary-operator e
2
⇒ v binary-operator e
′
2
Prim-binary-reduce: An expression with binary operator can be reduced if its left and right sub-
expressions are values and the corresponding function is defined for those values.
v is result of v
1
binary-operator v
2
v
1
binary-operator v
2
⇒ v
Expressions: Unary operators
Unary-reduce: An expression with unary operator can be reduced if its sub-expression can be
reduced.
e ⇒ e
′
unary-operator e ⇒ unary-operator e
′
Prim-unary-reduce: An expression with unary operator can be reduced if its sub-expression is a
value and the corresponding function is defined for that value.
v
′
is result of unary-operator v
unary-operator v ⇒ v
′
Expressions: conditionals
Conditional-predicate-reduce: A conditional expression can be reduced, if its predicate can be
reduced.
e
1
⇒ e
′
1
e
1
? e
2
: e
3
⇒ e
′
1
? e
2
: e
3
Conditional-true-reduce: A conditional expression whose predicate is the value true can be
reduced to its consequent expression.
true ? e
1
: e
2
⇒ e
1
Conditional-false-reduce: A conditional expression whose predicate is the value false can be
reduced to its alternative expression.
false ? e
1
: e
2
⇒ e
2
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 5
Expressions: function application
Application-functor-reduce: A function application can be reduced if its functor expression can
be reduced.
e ⇒ e
′
e ( expressions ) ⇒ e
′
( expressions )
Application-argument-reduce: A function application can be reduced if one of its argument ex-
pressions can be reduced and all preceding arguments are values.
e ⇒ e
′
v ( v
1
. . . v
i
e . . . ) ⇒ v ( v
1
. . . v
i
e
′
. . . )
Function-declaration-application-reduce: The application of a function declaration can be re-
duced, if all arguments are values.
f = function n ( x
1
. . . x
n
) block
f ( v
1
. . . v
n
) ⇒ block[x
1
:= v
1
] . . . [x
n
:= v
n
][n := f ]
Function-definition-application-reduce: The application of a function definition can be reduced,
if all arguments are values.
f = ( x
1
. . . x
n
) => b, where b is an expression or block
f ( v
1
. . . v
n
) ⇒ b[x
1
:= v
1
] . . . [x
n
:= v
n
]
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 6
Substitution
Identifier: An identifier with the same name as x is substituted with e
x
.
x[x := e
x
] = e
x
name ̸= x
name[x := e
x
] = name
Expression statement: All occurrences of x in e are substituted with e
x
.
e;[x := e
x
] = e [x := e
x
];
Binary expression: All occurrences of x in the operands are substituted with e
x
.
(e
1
binary-operator e
2
)[x := e
x
] = e
1
[x := e
x
] binary-operator e
2
[x := e
x
]
Unary expression: All occurrences of x in the operand are substituted with e
x
.
(unary-operator e)[x := e
x
] = unary-operator e[x := e
x
]
Conditional expression: All occurrences of x in the operands are substituted with e
x
.
(e
1
? e
2
: e
3
)[x := e
x
] = e
1
[x := e
x
] ? e
2
[x := e
x
] : e
3
[x := e
x
]
Logical expression: All occurrences of x in the operands are substituted with e
x
.
(e
1
|| e
2
)[x := e
x
] = e
1
[x := e
x
] || e
2
[x := e
x
]
(e
1
&& e
2
)[x := e
x
] = e
1
[x := e
x
] && e
2
[x := e
x
]
Call expression: All occurrences of x in the arguments and the function expression of the appli-
cation e are substituted with e
x
.
(e ( x
1
. . . x
n
))[x := e
x
] = e[x := e
x
] ( x
1
[x := e
x
] . . . x
n
[x := e
x
] )
Function declaration: All occurrences of x in the body of a function are substituted with e
x
under
given circumstances.
1. Function declaration where x has the same name as a parameter.
∃ i ∈ {1, · · · , n} s.t. x = x
i
(function name ( x
1
. . . x
n
) block)[x := e
x
] = function name ( x
1
. . . x
n
) block
2. Function declaration where x does not have the same name as a parameter.
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 7
(a) No parameter of the function occurs free in e
x
.
∀ i ∈ {1, · · · , n} s.t. x ̸= x
i
, ∀ j ∈ {1, · · · , n} s.t. x
j
does not occur free in e
x
(function name ( x
1
. . . x
n
) block)[x := e
x
]
=
function name ( x
1
. . . x
n
) block[x := e
x
]
(b) A parameter of the function occurs free in e
x
.
∀ i ∈ {1, · · · , n} s.t. x ̸= x
i
, ∃ j ∈ {1, · · · , n} s.t. x
j
occurs free in e
x
(function name ( x
1
. . . x
j
. . . x
n
) block)[x := e
x
]
=
(function name ( x
1
. . . y . . . x
n
) block[x
j
:= y])[x := e
x
]
Substitution is applied to the whole expression again as to recursively detect and re-
name all parameters of the function declaration that clash with variables that occur
free in e
x
, at which point ( i ) takes place. Note that the name y is not declared in, nor
occurs in block and e
x
.
Lambda expression: All occurrences of x in the body of a lambda expression are substituted with
e
x
under given circumstances.
1. Lambda expression where x has the same name as a parameter.
∃ i ∈ {1, · · · , n} s.t. x = x
i
(( x
1
. . . x
n
) => block)[x := e
x
] = ( x
1
. . . x
n
) => block
2. Lambda expression where x does not have the same name as a parameter.
(a) No parameter of the lambda expression occurs free in e
x
.
∀ i ∈ {1, · · · , n} s.t. x ̸= x
i
, ∀ j ∈ {1, · · · , n} s.t. x
j
does not occur free in e
x
(( x
1
. . . x
n
) => block)[x := e
x
] = ( x
1
. . . x
n
) => block[x := e
x
]
(b) A parameter of the lambda expression occurs free in e
x
.
∀ i ∈ {1, · · · , n} s.t. x ̸= x
i
, ∃ j ∈ {1, · · · , n} s.t. x
j
occurs free in e
x
(( x
1
. . . x
j
. . . x
n
) => block)[x := e
x
] = (( x
1
. . . y . . . x
n
) => block[x
j
:= y])[x := e
x
]
Substitution is applied to the whole expression again as to recursively detect and re-
name all parameters of the lambda expression that clash with variables that occur free
in e
x
, at which point ( i ) takes place. Note that the name y is not declared in, nor occurs
in block and e
x
.
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 8
Block expression: All occurrences of x in the statements of a block expression are substituted
with e
x
under given circumstances.
1. Block expression in which x is declared.
x is declared in block
block[x := e
x
] = block
2. Block expression in which x is not declared.
(a) No names declared in the block occurs free in e
x
.
x is not declared in block, name declared in block does not occur free in e
x
block[x := e
x
] = [block[0][x := e
x
], . . . , block[n][x := e
x
]]
(b) A name declared in the block occurs free in e
x
.
x is not declared in block, name declared in block occurs free in e
x
block[x := e
x
] = [block[0][name := y], . . . , block[n][name := y]][x := e
x
]
Substitution is applied to the whole expression again as to recursively detect and re-
name all declared names of the block expression that clash with variables that occur
free in e
x
, at which point ( i ) takes place. Note that the name y is not declared in, nor
occurs in block and e
x
.
Variable declaration: All occurrences of x in the declarators of a variable declaration are substi-
tuted with e
x
.
declarations[x := e
x
] = [declarations[0][x := e
x
] . . . declarations[n][x := e
x
]]
Return statement: All occurrences of x in the expression that is to be returned are substituted
with e
x
.
(return e;)[x := e
x
] = return e[x := e
x
];
Conditional statement: All occurrences of x in the condition, consequent, and alternative expres-
sions of a conditional statement are substituted with e
x
.
(if ( e ) block else block)[x := e
x
] = if ( e[x := e
x
] ) block[x := e
x
] else block[x := e
x
]
Array expression: All occurrences of x in the elements of an array are substituted with e
x
.
[x
1
, . . . , x
n
][x := e
x
] = [x
1
[x := e
x
], . . . , x
n
[x := e
x
]]
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 9
Free names
Let be the relation that defines the set of free names of a given Source expression; the symbols
p
1
and p
2
shall henceforth refer to unary and binary operations, respectively. That is, p
1
ranges
over {!} and p
2
ranges over {||, &&, +, -,
*
, /, ===, >, <}.
Identifier:
x {x}
name ∅
Boolean:
true ∅
false ∅
Expression statement:
e S
e; S
Unary expression:
e S
p
1
(e) S
Binary expression:
e
1
S
1
, e
2
S
2
p
1
(e
1
, e
2
) S
1
∪ S
2
Conditional expression:
e
1
S
1
, e
2
S
2
, e
3
S
3
e
1
? e
2
: e
3
S
1
∪ S
2
∪ S
3
Call expression:
e S, e
k
T
k
e(e
1
, . . . , e
n
) S ∪ T
1
∪ . . . ∪ T
n
Function declaration:
block S
function name ( x
1
. . . x
n
) block S − {x
1
, . . . , x
n
}
Lambda expression:
block S
( x
1
. . . x
n
) => block S − {x
1
, . . . , x
n
}
SICP, JavaScript Adaptation, Source §2 Stepper, 2022 10
Block expression:
block[k] S
k
, T contains all names declared in block
block (S
1
∪ . . . ∪ S
n
) − T
Constant declaration:
e S
const name = e; S
Return statement:
e S
return e; S
Conditional statement:
e S, block
1
T
1
, block
2
T
2
if ( e ) block
1
else block
2
S ∪ T
1
∪ T
2
