The Formal Semantics of Rascal Light
Ahmad Salim Al-Sibahi

arXiv:1703.02312v4 [] 6 Feb 2018

February 7, 2018

1

Introduction

Rascal (Klint et al., 2009, 2011) is a high-level transformation language that aims to simplify
software language engineering tasks like deﬁning program syntax, analyzing and transforming
programs, and performing code generation. The language provides several features including built-in collections (lists, sets, maps), algebraic data-types, powerful pattern matching
operations with backtracking, and high-level traversals supporting multiple strategies.
Interaction between diﬀerent language features can be diﬃcult to comprehend, since most
features are semantically rich. My goal is to provide a well-deﬁned formal semantics for a
large subset of Rascal called Rascal Light—in the spirit of (core) Caml Light (Leroy, 1997),
Clight (Blazy and Leroy, 2009), and Middleweight Java (Bierman et al., 2003)—suitable for
developing formal techniques, e.g., type systems and static analyses.

Scope
Rascal Light aims to model a realistic set of high-level transformation language features,
by capturing a large subset of the Rascal operational language. Rascal Light targets being
practically usable, i.e., it should be possible to translate many realistic pure Rascal programs
to this subset by an expert programmer without losing the high level of abstraction. The
following Rascal features are captured in Rascal Light:
• Fundamental deﬁnitions including algebraic data-types, functions with type parameters, and global variables.
• Basic expressions, including variable assignment, deﬁnition and access, exceptions, collections (including sets, lists and maps), if-expressions, switch-statements, for-loops
and while-loops including control ﬂow operators.
• Powerful pattern matching operations including type patterns, non-linear pattern matching, (sub)collection patterns, and descendant pattern matching.
• Backtracking using the fail operator, including roll-back of state.
• Traversals using generic visit-expressions, supporting the diﬀerent kinds of available
strategies: bottom-up(-break), top-down(-break), innermost, and outermost.
1

• Fixed-point iteration using the solve-loop.
The following Rascal features are considered out of scope:
• Concrete syntax declaration and literals, string interpolation, regular expression matching, date literals and path literals
• The standard library including Input/Output and the Java foreign function interface
• The module system, include modular extension of language elements such as datatypes
and functions
• Advanced type system features, like parametric polymorphism, the numerical hierarchy
and type inference
In Rascal, Boolean expressions can contain pattern matching subexpressions and backtracking is aﬀected by the various Boolean operators (conjunction, disjunction, implication). In
Rascal Light, backtracking is more restricted, which I believe heavily simpliﬁes the semantics
while losing little expressiveness in practice; most programs could be rewritten to support
the required backtracking at the cost of increased verbosity.

Method
I have used the language documentation,1 and the open source implementation of Rascal,2
to derive the formalism. The syntax is primarily based on the μRascal syntax description (CWI Amsterdam, 2017), but altered to focus on the high-level features. The semantics
is based on the description of individual language features in the documentation. In case
of under-speciﬁcation or ambiguity, I used small test programs to check what the expected
behavior is. I thank the Rascal developers for our personal correspondence which further
clariﬁed ambiguity and limitations of the semantics compared to Rascal.
To discover possible issues, the semantics has been implemented as a prototype and tested
against a series of Rascal programs. To strengthen the correctness claims, I have proven a
series of theorems of interest in Section 4, since as Milner et al. (1990) states:
The robustness of the semantics depends upon theorems
— The Deﬁnition of Standard ML

Notation
A sequence of es is represented by either e or more explicitly e1 , . . . , en , the empty sequence
is denoted by ε and the concatenation of sequences e1 and e2 is denoted e1 , e2 . We overload
notation in an intuitive manner for operations on sequences, so given a sequence v, vi denotes
the ith element in the sequence, and v : t denotes the sequence v1 : t1 , . . . , vn : tn .
1
2

http://tutor.rascal-mpl.org/Rascal/Rascal.html
https://github.com/usethesource/rascal

2

Overview
The abstract syntax of Rascal Light is presented in Section 2, and the dynamic (operational)
semantics is presented in Section 3. Finally, Section 4 presents relevant theorems regarding
the soundness of the semantics.

2

Abstract Syntax

Rascal Light programs are organized into modules that consist of deﬁnitions of global variables, functions and algebraic data types. I will in the rest of this report assume that modules
are well-formed: top-level deﬁnitions and function parameters have unique names, all function calls, constructors and datatypes used have corresponding deﬁnitions, and all variables
are well-scoped with no shadowing. To maintain a clean presentation, I will not write the
deﬁnition environment explicitly, but mention the necessary deﬁnitions as premises when
required.
Rascal Light has three kinds of deﬁnitions: global variables, functions and algebraic
data-types. Global variables are typed and are initialized with a target expression at module
loading time. Functions have a return type, a unique name, a list of typed uniquely named
parameters, and have an expression as a body. Algebraic data-types have unique names
and declare a set of possible alternative constructors, each taking a list of typed ﬁelds as
arguments.
d ::= global t y = e

(Global variables)

| fun t f (t x) = e

(Function Definition)

| data at = k1 (t x)| . . . |kn (t x) (Algebraic Data Type Definition)

The operational part of Rascal consists of syntactically distinct categories of statements and
expressions; I have chosen to collapse the two categories in Rascal Light since statements
also have result values that can be used inside expressions. Most constructs are standard
imperative ones, such as blocks, assignment, branching and loops (including control operations); I have chosen to use local-in for representing blocks in Rascal Light instead of curly
braces like in Rascal, to distinguish them from set literal expressions; blocks contain locally
declared variables and a sequence of expressions to evaluate.
Notable Rascal-speciﬁc constructs include a generalized version of the switch-expression
that supports rich pattern matching over both basic values and algebraic data types, the visitexpression which allows traversing data types using various strategies (Example 1), and the
solve-expression which continuously evaluates its body expression until target variables reach
a ﬁxed-point in assigned values (Example 2). The fail control operator allows backtracking
inside switch and visit statements to try other possible matches (Example 3).
e ::= vb

(Basic Values , vb ∈ {1, “foo”, 3.14, . . .})

|x

(Variables, x, y ∈ Var)

|⊖e

(Unary Operations, ⊖ ∈ {−, . . .})

3

| e1 ⊕ e2
| k(e)

(Binary Operations, ⊕ ∈ {+, −, ×, . . .})
(Constructor Applications, k ∈ Constructor)

| [e]

(List Expressions)

| {e}

(Set Expressions)
′

(Map Expressions)

| e1 [e2 ]

(Map Lookup)

| e1 [e2 = e3 ]

(Map Update)

| (e : e )

(Function Calls, f ∈ Function)

| f (e)
| return e

(Return Expressions)

|x=e

(Variable Update Assignments)

| if e then e1 else e2

(Conditionals)

| switch e do cs

(Case Matching)

| st visit e do cs

(Deep Traversal)

| break | continue | fail

(Control Operations)

| local t x in e end

(Blocks)

| for g e

(Iteration)

| while e e

(While Expressions)

| solve x e

(Fixedpoint Expressions)

| throw e

(Exception Throwing)

| try e1 catch x ⇒ e2

(Exception Catching)

| try e1 finally e2
cs ::= case p ⇒ e

(Exception Finalization)
(Case)

Example 1 (Expression simpliﬁer). An expression simpliﬁer can use visit to completely simplify all sub-expressions no matter where they are in the input expression:
1

data Expr = intlit(int v) | plus(Expr lop, Expr rop) | ...;

2
3
4
5
6
7

Expr simplify(Expr e) =
bottom-up visit(e) {
case plus(intlit(0), y) => y
case plus(x, intlit(0)) => x
};

Example 2 (Lattice ﬁxed-point). The Kleene ﬁxed-point of a continuous function in a lattice
for a domain V al with functions for the bottom element and least-upper bound can be
computed using solve:
1
2
3
4
5
6

Val fix(Fun f) = {
Val v = bottom();
solve(v) {
v = lub(v, apply(f, v))
};
}

4

Example 3 (Knapsack problem). The knapsack problem concerns ﬁnding a subset of items
with greatest value under a speciﬁed maximum weight. The function below uses backtracking
to (slowly) ﬁnd the optimal solution.
1
2
3
4
5
6
7
8
9
10
11
12

set[Item] slowknapsack(set[Item] items, int maxWeight) = {
set[Item] res = {};
solve(res) {
switch(items) {
case {*xs, *ys}:
if (sumweights(xs) > maxWeight
|| sumvalues(xs) < sumvalues(res)) fail;
else res = xs;
};
res
};
}

There are two kinds of generator expressions: enumerating assignment where the range
variable is assigned to each element in the result of a collection-producing expression, and
matching assignment that produces all possible assignments that match target patterns (deﬁned later).
g ::= x ← e (Enumerating Assignment)
| p := e
(Matching Assignment)

The visit-expression supports various strategies that determine the order a particular value is
traversed w.r.t. its contained values. The top-down strategy traverses the value itself before
contained values, and conversely bottom-up traverses contained values before itself. The
break versions stop the traversal at ﬁrst successful match, and the outermost and innermost
respectively apply the top-down and bottom-up until a ﬁxed-point is reached.
st ::= top-down

(Preorder Traversal)

| bottom-up

(Postorder Traversal)

| top-down-break

(First-match Preorder Traversal)

| bottom-up-break

(First-match Postorder Traversal)

| outermost

(Fixedpoint Preorder Traversal)

| innermost

(Fixedpoint Postorder Traversal)

Like Rascal, Rascal Light has a rich pattern language that not only includes matching on
basic values and constructors, but also powerful matching inside collections and descendant
patterns that allow matching arbitrarily deeply contained values.
p ::= vb
|x
| k(p)

(Basic Value Patterns)
(Variable Patterns)
(Deconstructor Patterns)

| t x : p (Typed Labelled Patterns)
| [⋆p]

(List Patterns)

5

| {⋆p}

(Set Patterns)

| !p

(Negation pattern)

| /p

(Descendant Patterns)

Patterns inside collections can be either ordinary patterns or star patterns that match a
subcollection with arbitrary number of elements.
⋆p ::= p (Ordinary Pattern)
| ⋆x

(Star Pattern)

Rascal Light programs expressions evaluate to values, which either are basic values, constructor values, collections or the undeﬁned value ().
v ::= vb

(Basic Values)
(Constructor Values, k ∈ Constructor)

| k(v)
| [v]

(List Values)

| {v}

(Set Values)

| (v : v ′ )

(Map Values)

|

3

(Undefined Value)

Semantics

I present a formal development of the dynamic aspects of Rascal Light, using a natural
semantics speciﬁcation. Natural (big-step) semantics (Kahn, 1987) is particularly suitable
for Rascal, because it closely mimics semantics of an interpreter and the high-level features—
exceptions, backtracking, traversals—introduce a rich control-ﬂow that depends not only on
the structure of the program but also on the provided input. There is no concurrency or
interleaving in Rascal, and so there is no need for a more ﬁne-grained operational semantics
like (small-step) structural operational semantics (SOS) (Plotkin, 2004).

Value Typing
Rascal (Light) is strongly typed and so all values are typed. The types are fairly straightforward in the sense that most values have a canonical type and there is a subtyping hierarchy
(explained shortly) with a bottom type void and a top type value.
t ::= tb

(Base Types, tb ∈ {Int, Rational, String, . . .})

| at

(Algebraic Data Types, at ∈ DataType)

| sethti

(Sets)

| listhti

(Lists)

6

| mapht1 , t2 i

(Maps)

| void

(Bottom Type)

| value

(Top Type)

I provide a typing judgment for values of form v : t, which states that value v has type t.
Basic values are typed by their deﬁning basic type, the undeﬁned value () has the bottom
type void, and constructor values are typed by their corresponding data type deﬁnition
assuming the contained values are well-typed. The type of collections is determined by the
contained values, and so a least upper bound operator is deﬁned in types—following the
subtype ordering—which is used to infer a precise type for the value parameters.
T-Basic

vb ∈ JtbK
vb : tb

T-Bot

 : void
v : t′

data at = . . . | k(t) | . . .
T-Constructor

k(v1 , . . . , vn ) : at
v ′ : t′
F F
T-Map
(v : v ′ ) : maph t, t′ i

v:t

v:t

v:t

F
T-List
[v] : listh ti

F
T-Set
{v} : seth ti

t′ <: t

The subtyping relation has form t <: t′ , stating t is a subtype of t′ . We let t 6<: t′ denote the
negated form where none of the given cases below matches. subtyping is reﬂexive, so every
type is a sub-type of itself; void and value act as bottom type and top type respectively.
ST-Refl

ST-Void

t <: t

ST-Value

void <: t

t <: value

Collections are covariant in their type parameters, which is safe since all values are immutable.

ST-List

t <: t′
listhti <: listht′ i

ST-Map

ST-Set

tkey <: t′key

t <: t′
sethti <: setht′ i

tval <: t′val

maphtkey , tval i <: mapht′key , t′val i

The least upper bound on types is deﬁned as follows:
G

ε = void



t1




t2



listht′ ⊔ t′ i
2
1
t1 ⊔ t2 =
′ ⊔ t′ i

setht

1
2



′ ⊔ t′ , t′′ ⊔ t′′ i

mapht

2
2 1
1


value

G

t, t′ = t ⊔

G

t′

if t2 = void ∨ t1 = t2
if t1 = void
if t1 = listht′1 i ∧ t2 = listht′2 i
if t1 = setht′1 i ∧ t2 = setht′2 i
if t1 = mapht′1 , t′′1 i ∧ t2 = mapht′2 , t′′2 i
otherwise

7

Expression Evaluation
The main judgment for Rascal Light expressions has the form e; σ ==⇒ vres; σ ′ , where the
expr

expression e is evaluated in an initial store σ ∈ Var → Val—mapping variables to values—
returning a result vres and updated store σ ′ as a side-eﬀect. The result vres is either an
ordinary success v signifying successful execution or an exceptional result exres.
vres ::= success v | exres

An exceptional result is either a control operation (break, continue, fail), an error that happened during execution, a thrown exception throw v or an early return value return v. The
diﬀerence between success v and return v is that the latter should propagate directly from
sub-expressions to the surrounding function call boundary, while the value in the former can
be used further in intermediate computations (Example 4).
exres ::= return v | throw v | break | continue | fail | error

Example 4 (Early Return). The function that calculates producs, uses the early return functionality to short-circuit the rest of the calculation when a factor in the provided list is zero.
If this branch is hit during execution, evaluating the expression produces return 0 as result,
which is then propagated directly to function call boundary, skipping the rest of the loop
and sequenced expressions.
1
2
3
4
5
6
7
8

int prod(list[int] xs) {
int res = 1;
for (x <- xs) {
if (x == 0) return 0;
else res *= x;
};
res
}

Basic values evaluate to their semantic equivalent result values without any side eﬀect (EVal).
E-Val

vb; σ ==⇒ success vb; σ
expr

A variable evaluates to the value it is assigned to in the store if available (E-Var-Sucs),
and otherwise result in an error (E-Var-Err).
E-Var-Sucs

x ∈ dom σ
x; σ ==⇒ success σ(x); σ

x∈
/ dom σ

E-Var-Err x; σ ==⇒ error; σ
expr

expr

Unary expressions evaluate their operands, applying possible side-eﬀects; if successful the
corresponding semantic unary operator J⊖K is applied on the result value (E-Un-Sucs), and
otherwise it propagates the exceptional result (E-Un-Exc).
e; σ ==⇒ exres; σ ′

e; σ ==⇒ success v; σ ′
E-Un-Sucs

expr

⊖ e; σ ==⇒
expr

E-Un-Exc

J⊖K(v); σ ′

expr

⊖ e; σ ==⇒ exres; σ ′
expr

8

Example 5 (Unary operator semantics). J−K(3) will evaluate to success −3, while J−K({})
will evaluate to error.
Evaluating binary expressions is similar to unary expressions, requiring both operands to
evaluate successfully (E-Bin-Sucs) to apply the corresponding semantic binary operator
J⊕K; otherwise the exceptional results of the operands are propagated in order from left
(E-Bin-Exc1) to right (E-Bin-Exc2).
e1 ; σ ==⇒ success v1 ; σ ′′

e2 ; σ ′′ ==⇒ success v2 ; σ ′

expr

E-Bin-Sucs

expr

e1 ⊕ e2 ; σ ==⇒ J⊕K(v1 , v2 ); σ ′
expr

e1 ; σ ==⇒ exres 1 ; σ ′′
E-Bin-Exc1

expr

e1 ⊕ e2 ; σ ==⇒ exres 1 ; σ ′
expr

e1 ; σ ==⇒ success v1 ; σ ′′
E-Bin-Exc2

e2 ; σ ′′ ==⇒ exres 2 ; σ ′

expr

e1 ⊕ e2 ; σ ==⇒ exres 2
expr

expr
; σ′

Constructor expressions evaluate their arguments ﬁrst, and if they all successfully evaluate
to values, then check whether the types of values match those expected in the declaration.
If the result values have the right types and are not , a constructor value is constructed
(E-Cons-Sucs), and otherwise a (type) error is produced (E-Cons-Err). In case any of
the arguments has an exceptional result the evaluation of the rest of the arguments halts
and the exceptional result is propagated (E-Cons-Exc).
e; σ ===⇒ success v; σ ′

data at = . . . | k(t) | . . .
v : t′
E-Cons-Sucs

expr⋆

t′ <: t

v 6= 
k(e); σ ==⇒ success k(v); σ ′
expr

e; σ ===⇒ success v; σ ′

data at = . . . | k(t) | . . .
E-Cons-Err

expr⋆

∃i.vi =  ∨ t′i 6<: ti

v : t′

k(e); σ ==⇒ error; σ ′
expr

e; σ ===⇒ exres; σ ′
E-Cons-Exc

expr⋆

k(e); σ ==⇒ exres; σ ′
expr

Evaluating list expressions also requires evaluating all subexpressions to a series of values;
because of sequencing and necessity of early propagation of exceptional results, evaluation
of series of subexpressions is done using a mutually recursive sequence evaluation judgment
(see page 17). If the evaluation is successful then a list value is constructed (E-List-Sucs),
unless any value is undeﬁned () in which case we produce an error (E-List-Err), and
otherwise the exceptional result is propagated (E-List-Exc).
e; σ ===⇒ success v; σ ′
E-List-Sucs

expr⋆

v 6= 

[e]; σ ==⇒ success [v]; σ ′
expr

9

e; σ ===⇒ success v; σ ′
E-List-Err

[e]; σ ==⇒
expr

e; σ ===⇒ exres; σ ′

∃i.vi = 

expr⋆

E-List-Exc

error; σ ′

expr⋆

[e]; σ ==⇒ exres; σ ′
expr

Set expression evaluation mirror the one for lists, except that values are constructed using
a set constructor (E-Set-Sucs), which may reorder values and ensures that there are no
duplicates. If any contained value was undeﬁned () then an error is produced instead
(E-Set-Err), and exceptional results are propagated (E-Set-Exc).
e; σ ===⇒ success v; σ ′

v 6= 

expr⋆

E-Set-Sucs

{e}; σ ==⇒ success {v}; σ ′
expr

e; σ ===⇒ success
E-Set-Err

expr⋆

v; σ ′

{e}; σ ==⇒
expr

e; σ ===⇒ exres; σ ′

∃i.vi = 
E-Set-Exc

error; σ ′

expr⋆

{e}; σ ==⇒ exres; σ ′
expr

Map expressions evaluate their keys and values in the declaration sequence, and if successful construct a map (E-Map-Sucs). Similarly to other collection expressions, errors are
produced if any value is undeﬁned (E-Map-Err) and exceptional results are propagated
(E-Map-Exc).
e, e′ ; σ ===⇒ success v, v ′ ; σ ′
expr⋆

E-Map-Sucs

v 6= 

v ′ 6= 

(e : e′ ); σ ==⇒ success (v : v ′ ); σ ′
expr

e, e′ ; σ ===⇒ success v, v ′ ; σ ′
E-Map-Err

expr⋆

∃.vi =  ∨ vi′ = 

(e : e′ ); σ ==⇒ error; σ ′
expr

′

e, e ; σ ===⇒ exres; σ ′
E-Map-Exc

expr⋆

′

(e : e ); σ ==⇒ exres; σ ′
expr

Lookup expressions require evaluating the outer expression to a map—otherwise producing
an error (E-Lookup-Err)—and the index expression to a value. If the index is an existing
key then the corresponding value is produced as result (E-Lookup-Sucs) and otherwise
the nokey exception is thrown (E-Lookup-NoKey); here, I assume that data NoKey =
nokey(value key) is a built-in data-type deﬁnition. Exceptional results are propagated from
sub-terms (E-Lookup-Exc1, E-Lookup-Exc2).
e1 ; σ ==⇒ success (. . . , v : v ′ , . . . ); σ ′′
expr

e2 ; σ ′′ ==⇒ success v; σ ′
E-Lookup-Sucs

expr

e1 [e2 ]; σ ==⇒ success v ′ ; σ ′
expr

e1 ; σ ==⇒ success (v : v ′ ); σ ′′
expr

e2 ; σ ′′ ==⇒ success v ′′ ; σ ′
E-Lookup-NoKey

expr

∀i.v ′′ 6= vi

e1 [e2 ]; σ ==⇒ throw nokey(v ′′ ); σ ′
expr

10

e1 ; σ ==⇒ success v; σ ′

v 6= (v ′ : v ′′ )

expr

E-Lookup-Err

e1 [e2 ]; σ ==⇒ error; σ ′
expr

e1 ; σ ==⇒ exres; σ ′
E-Lookup-Exc1

expr

e1 [e2 ]; σ ==⇒ exres; σ ′
expr

e1 ; σ ==⇒ success (v : v ′ ); σ ′′

e2 ; σ ′′ ==⇒ exres; σ ′

expr

E-Lookup-Exc2

e1 [e2 ]; σ ==⇒
expr

expr

exres; σ ′

Map update expressions also require the outer expression to evaluate to a map—otherwise
producing an error (E-Update-Err1)—and the index and target expressions to evaluate to
values. On succesful evaluation of both index and target value the map is updated, overriding
the old value of the corresponding index if necessary (E-Update-Sucs) unless the index or
target value is equal to  in which case an error is produced (E-Update-Err2). Finally,
exceptional results are propagated left-to-right if necessary (E-Update-Exc1, E-UpdateExc2, E-Update-Exc3).
e1 ; σ ==⇒ success (v : v ′ ); σ ′′′
expr
e3 ; σ ′′ ==⇒
expr

E-Update-Sucs

e2 ; σ ′′′ ==⇒ success v ′′ ; σ ′′
expr

success v ′′′ ; σ ′

v ′′ 6= 

v ′′′ 6= 

e1 [e2 = e3 ]; σ ==⇒ success (v : v ′ , v ′′ : v ′′′ ); σ ′
expr

e1 ; σ ==⇒ success v; σ ′

v 6= (v ′ : v ′′ )

expr

E-Update-Err1

e1 [e2 = e3 ]; σ ==⇒ error; σ ′
expr

e1 ; σ ==⇒ success (v : v ′ ); σ ′′′
E-Update-Err2

expr
e3 ; σ ′′ ==⇒
expr

e2 ; σ ′′′ ==⇒ success v ′′ ; σ ′′
expr

success v ′′′ ; σ ′

v ′′ =  ∨ v ′′′ = 

e1 [e2 = e3 ]; σ ==⇒ error; σ ′
expr

e1 ; σ ==⇒ exres; σ ′
E-Update-Exc1

expr

e1 [e2 = e3 ]; σ ==⇒ exres; σ ′
expr

e1 ; σ ==⇒ success (v : v ′ ); σ ′′
E-Update-Exc2

e2 ; σ ′′ ==⇒ exres; σ ′

expr

e1 [e2 = e3 ]; σ ==⇒
expr

expr
exres; σ ′

e1 ; σ ==⇒ success (v : v ′ ); σ ′′
expr

e2 ; σ ′′′ ==⇒ success v ′′ ; σ ′′
E-Update-Exc3

expr

e3 ; σ ′′ ==⇒ exres; σ ′

e1 [e2 = e3 ]; σ ==⇒
expr

expr
exres; σ ′

Evaluation of function calls is more elaborate. Function deﬁnitions are statically scoped, and
the semantics is eager, so arguments are evaluated using call-by-value. The initial step is
11

thus to evaluate all the arguments to values if possible—propagating the exceptional result
otherwise (E-Call-Arg-Exc)—and then check whether the values have the right type
(otherwise producing an error, E-Call-Arg-Err). The evaluation proceeds by evaluating
the body of the function with a fresh store that contains the values of global variables and
the parameters bound to their respective argument values. There are then four cases:
1. If the body successfully evaluates to a correctly typed value, then that value is provided
as the result (E-Call-Sucs).
2. If the body evaluates to a value that does not have the expected type, then it produces
an error (E-Call-Res-Err1).
3. If the result is a thrown exception or error, then it is propagated (E-Call-Res-Exc).
4. Otherwise if the result is a control operator, then an error is produced (E-Call-ResErr2).
In all cases the resulting store of executing the body is discarded—since local assignments
fall out of scope—except the global variable values which are added to the store that was
there before the function call.
fun t′ f (t x) = e′
v : t′′
t′′ <: t

global ty y
e; σ ===⇒ success v; σ ′′
expr⋆

[y 7→ σ ′′ (y), x 7→ v]; e′ ==⇒ vres; σ ′
expr

vres = return v ′ ∨ vres = success v ′
v ′ : t′′′
t′′′ <: t′
E-Call-Sucs
f (e); σ ==⇒ success v ′ ; σ ′′ [y 7→ σ ′ (y)]
expr

fun t′ f (t x) = e′

e; σ ===⇒ success v; σ ′
expr⋆

t′′i 6<: ti

v : t′′
E-Call-Arg-Err

f (e); σ ==⇒ error; σ ′
expr

e; σ ===⇒ exres; σ ′
E-Call-Arg-Exc

expr⋆

f (e); σ ==⇒ exres; σ ′
expr

global ty y
e; σ ===⇒ success v; σ ′′
expr⋆

fun t′ f (t x) = e′
v : t′′
t′′ <: t

[y 7→ σ ′′ (y), x 7→ v]; e′ ==⇒ exres; σ ′
E-Call-Res-Exc

expr

exres = throw v ′

f (e); σ ==⇒ exres; σ ′′ [y 7→ σ ′ (y)]
expr

global ty y
e; σ ===⇒ success v; σ ′′
expr⋆

fun t′ f (t x) = e′
v : t′′
t′′ <: t

[y 7→ σ ′′ (y), x 7→ v]; e′ ==⇒ vres; σ ′
expr

vres = return v ′ ∨ vres = success v ′
v ′ : t′′′
E-Call-Res-Err1
f (e); σ ==⇒ error; σ ′′ [y 7→ σ ′ (y)]
expr

12

t′′′ 6<: t′

fun t′ f (t x) = e′
global ty y
e; σ ===⇒ success v; σ ′′
v : t′′
t′′ <: t
expr⋆

[y 7→ σ ′′ (y), x 7→ v]; e′ ==⇒ exres; σ ′
expr

exres ∈ {break, continue, fail, error}
f (e); σ ==⇒ error; σ ′′ [y 7→ σ ′ (y)]

E-Call-Res-Err2

expr

The return-expression evaluates its argument expression ﬁrst, and if it successfully produces
a value then the result would be an early return with that value (E-Ret-Sucs); recall
that early returns are treated as exceptional values and so propagated through most evaluation rules, except at function call boundaries (rules E-Call-Sucs and E-Call-Res-Err1).
Otherwise, the exceptional result is propagated (E-Ret-Exc).
e; σ ==⇒ success v; σ ′
E-Ret-Sucs

e; σ ==⇒ exres; σ ′

expr

return e; σ ==⇒ return
expr

E-Ret-Exc

v; σ ′

expr

return e; σ ==⇒ exres; σ ′
expr

In Rascal Light, variables must be declared before being assigned, and declarations are unique
since shadowing is disallowed. Evaluating an assignment proceeds by evaluating the righthand side expression—propagating exceptional results (E-Asgn-Exc)—and then checking
whether the produced value is compatible with the declared type. If it is compatible then
the store is updated (E-Asgn-Sucs), and otherwise an error is produced (E-Asgn-Err).
e; σ ==⇒ success v; σ ′

local t x ∨ global t x
E-Asgn-Sucs

expr

v : t′
t′ <: t
′
x = e; σ ==⇒ success v; σ [x 7→ v]
expr

e; σ ==⇒ success v; σ ′

local t x ∨ global t x

expr

v : t′
t′ 6<: t
x = e; σ ==⇒ error; σ ′

E-Asgn-Err

expr

e; σ ==⇒ exres; σ ′
E-Asgn-Exc

expr

x = e; σ ==⇒ exres; σ ′
expr

The if-expression works like other languages: the then-branch is evaluated if the condition is
true (E-If-True), otherwise the else-branch is evaluated (E-If-False). If the conditional
produces a non-Boolean value then an error is raised (E-If-Err) and otherwise exceptional
results are propagated (E-If-Exc).
econd ; σ ==⇒ success true(); σ ′′
E-If-True

expr

e1 ; σ ′′ ==⇒ vres 1 ; σ ′
expr

if econd then e1 else e2 ; σ ==⇒ vres 1 ; σ ′
expr

econd ; σ ==⇒ success
E-If-False

expr

false(); σ ′′

e2 ; σ ′′ ==⇒ vres 2 ; σ ′
expr

if econd then e1 else e2 ; σ ==⇒ vres 2 ; σ ′
expr

13

econd ; σ ==⇒ success v; σ ′

v 6= true()

expr

E-If-Err

v 6= false()

if econd then e1 else e2 ; σ ==⇒ error; σ ′
expr

econd ; σ ==⇒ exres; σ ′
expr

E-If-Exc

if econd then e1 else e2 ; σ ==⇒ exres; σ ′
expr

The switch-expression initially evaluates the scrutinee expression (e), and then proceeds
to execute the cases (discussed on page 18) on the result value (E-Switch-Sucs). The
evaluation of cases is allowed to fail, in which case the evaluation is successful and has
the special value  (E-Switch-Fail); other exceptional results are propagated as usual
(E-Switch-Exc1, E-Switch-Exc2).
e; σ ==⇒ success v; σ ′′

cs; v; σ ′′ ===
⇒ success v ′ ; σ ′

expr

E-Switch-Sucs

switch e cs; σ ==⇒
expr

e; σ ==⇒ success
expr

E-Switch-Fail

v; σ ′′

cases
success v ′ ; σ ′

cs; v; σ ′′ ===⇒ fail; σ ′

switch e cs; σ ==⇒ success
expr

cases
; σ ′

e; σ ==⇒ exres; σ ′
E-Switch-Exc1

expr

switch e cs; σ ==⇒ exres; σ ′
expr

e; σ ==⇒ success v; σ ′′

cs; v; σ ′′ ===⇒ exres; σ ′

expr

E-Switch-Exc2

cases

exres 6= fail

switch e cs; σ ==⇒ exres; σ ′
expr

The visit-expression has similar evaluation cases to switch (E-Visit-Sucs, E-Visit-Fail,
E-Visit-Exc1, E-Visit-Exc2), except that the cases are evaluated using the visit relation
that traverses the produced value of target expression given the provided strategy.
st

e; σ ==⇒ success v; σ ′′

cs; v; σ ′′ ==⇒ success v ′ ; σ ′

expr

E-Visit-Sucs

visit

st visit e cs; σ ==⇒ success v ′ ; σ ′
expr

st

e; σ ==⇒ success v; σ ′′
E-Visit-Fail

cs; v; σ ′′ ==⇒ fail; σ ′

expr

visit

st visit e cs; σ ==⇒ success v; σ ′
expr

e; σ ==⇒ exres; σ ′
E-Visit-Exc1

expr

st visit e cs; σ ==⇒ exres; σ ′
expr

e; σ ==⇒ success v; σ ′′
E-Visit-Exc2

expr

st

cs; v; σ ′′ ==⇒ exres; σ ′
visit

st visit e cs; σ ==⇒ exres; σ ′
expr

14

exres 6= fail

The control operations break, continue and fail evaluate to themselves without any side-eﬀects
(E-Break, E-Continue, E-Fail).
E-Break

E-Fail

break; σ ==⇒ break; σ
expr

E-Continue

fail; σ ==⇒ fail; σ
expr

continue; σ ==⇒ continue; σ
expr

Blocks allow evaluating inner expressions using a local declaration of variables, which are then
afterwards removed from the resulting store (E-Block-Sucs, E-Block-Exc). Recall, that
we consider an implicit deﬁnition environment based on scoping, and so the local declarations
in the block will be implicitly available in the evaluation of the body subexpression sequence.
e; σ ===⇒ success v; σ ′
E-Block-Sucs

expr⋆

local t x in e end; σ ==⇒ success last(v); (σ ′ \ x)
expr

e; σ ===⇒ exres; σ ′
E-Block-Exc

expr⋆

local t x in e end; σ ==⇒ exres; (σ ′ \ x)
expr

The auxiliary function last is here used to extract the last element in the sequence (or return
 if empty).
last(v1 , . . . , vn , v ′ ) = v ′
last(ε) = 

The for-loop evaluates target generator expression to a set of possible environments that
represent possible assignments of variables to values—propagating exceptions if necessary
(E-For-Exc)—and then it iterates over each possible assignment using the each-relation
(E-For-Sucs).
g; σ ===⇒ success ρ; σ ′′
gexpr

g; σ ===⇒ exres; σ ′

e; ρ; σ ′′ ==⇒ vres; σ ′
E-For-Sucs

each

for g e; σ ==⇒
expr

E-For-Exc

vres; σ ′

gexpr

for g e; σ ==⇒ exres; σ ′
expr

The evaluation of while-loops is analogous to other imperative languages with control operations, in that the body of the while loop is continuously executed until the target condition
does not hold (E-While-False). If the body successfully ﬁnishes with an value or continue
then iteration continues (E-While-True-Sucs), if the body ﬁnishes with break the iteration
stops with value  (E-While-True-Break), if the conditional evaluates to a non-Boolean
value it errors out (E-While-Err) and otherwise if another kind of exceptional result is
produced then it is propagated (E-While-Exc1, E-While-Exc2).

15

econd ; σ ==⇒ success false(); σ ′
expr

E-While-False

while econd e; σ ==⇒ success ; σ ′
expr

econd ; σ ==⇒ success true(); σ ′′

e; σ ′′ ==⇒ vres; σ ′′′

expr

expr

vres = success v ∨ vres = continue
while econd e; σ ′′′ ==⇒ vres ′ ; σ ′
expr

E-While-True-Sucs

while econd e; σ ==⇒ vres ′ ; σ ′
expr

econd ; σ ==⇒ success true(); σ ′′
expr

E-While-True-Break

e; σ ′′ ==⇒ break; σ ′

while econd e; σ ==⇒ success
expr

expr
; σ ′

econd ; σ ==⇒ exres; σ ′
expr

E-While-Exc1

while econd e; σ ==⇒ exres; σ ′
expr

econd ; σ ==⇒ success true(); σ ′′

e; σ ′′ ==⇒ exres; σ ′

expr

expr

exres ∈ {throw v, return v, fail, error}
while econd e; σ ==⇒ exres; σ ′

E-While-Exc2

expr

econd ; σ ==⇒ success v; σ ′

v 6= true()

expr

E-While-Err

v 6= false()

while econd e; σ ==⇒ error; σ ′
expr

The solve-loop keeps evaluating the body expression until the provided variables reach a ﬁxedpoint. Initially, the body expression is evaluated and then the values of target variables is
compared from before and after iteration; if the values are equal after an iteration, then
evaluation stops (E-Solve-Eq) and otherwise the iteration continues (E-Solve-Neq). If
any of the variables do not have a value assigned, an error is produced (E-Solve-Err), and
otherwise if an exceptional result is produced, it is propagated (E-Solve-Exc).
e; σ ==⇒ success v; σ ′
E-Solve-Eq

expr

x ⊆ dom σ ∩ dom σ ′

σ(x) = σ ′ (x)

solve x e; σ ==⇒ success v; σ ′
expr

e; σ ==⇒ success v; σ ′′
expr

solve x e; σ ′′ ==⇒ vres; σ ′

∃i.σ(xi ) 6= σ ′′ (xi )
E-Solve-Neq

x ⊆ dom σ ∩ dom σ ′′

solve x e; σ ==⇒
expr

expr
vres; σ ′

e; σ ==⇒ exres; σ ′
E-Solve-Exc

expr

solve x e; σ ==⇒ exres; σ ′
expr

e; σ ==⇒ success v; σ ′
E-Solve-Err

expr

xi 6∈ dom σ ∩ dom σ ′

solve x e; σ ==⇒ error; σ ′
expr

16

The throw-expression, evaluates its inner expression ﬁrst—propagating exceptional results if
necessary (E-Thr-Exc)—and then produces a throw result with result value (E-Thr-Sucs).
e; σ ==⇒ exres; σ ′

e; σ ==⇒ success v; σ ′
E-Thr-Sucs

expr

throw e; σ ==⇒ throw
expr

E-Thr-Exc

v; σ ′

expr

throw e; σ ==⇒ exres; σ ′
expr

The try-finally expression executes the try-body ﬁrst and then the finally-body. If the finallybody produces an exceptional result during execution then that result is propagated (E-FinExc) and otherwise the try-body result value is used (E-Fin-Sucs).
e1 ; σ ==⇒ vres 1 ; σ ′′
expr

E-Fin-Sucs

e2 ; σ ′′ ==⇒ success v2 ; σ ′
expr

try e1 finally e2 ; σ ==⇒ vres 1 ; σ ′
expr

e1 ; σ ==⇒ vres 1 ; σ ′′

e2 ; σ ′′ ==⇒ exres 2 ; σ ′

expr

E-Fin-Exc

expr

try e1 finally e2 ; σ ==⇒ exres 2 ; σ ′
expr

The try-catch expression evaluates the try-body and if it produces a thrown value, then it
binds the value in the body of catch and continues evaluation (E-Try-Catch). For all other
results, it simply propagates them without evaluating the catch-body (E-Try-Ord).
e1 ; σ ==⇒ throw v1 ; σ ′′

e2 ; σ ′′ [x 7→ v1 ] ==⇒ vres 2 ; σ ′

expr

E-Try-Catch

try e1 catch x ⇒ e2 ; σ ==⇒ vres 2
expr

e1 ; σ ==⇒ vres 1 ; σ ′
E-Try-Ord

expr
; (σ ′ \

x)

vres 1 6= throw v1

expr

try e1 catch x ⇒ e2 ; σ ==⇒ vres 1 ; σ ′
expr

Expression Sequences Evaluating a sequence of expressions proceeds by evaluating each
expression, combining the results if successful (ES-Emp, ES-More) and otherwise propagating the ﬁrst exceptional result encountered (ES-Exc1, ES-Exc2).
e; σ ==⇒ success v; σ ′′
ES-More

expr

e, e′ ; σ

e′ ; σ ′′ ===⇒ success v ′ ; σ ′

===⇒ success
expr⋆

expr⋆
v, v ′ ; σ ′

e; σ ==⇒ exres; σ ′
ES-Emp success ε; σ ===⇒ ε; σ

ES-Exc1

expr⋆

e; σ ==⇒ success
ES-Exc2

expr

v; σ ′′

e, e′ ; σ

===⇒

17

expr⋆

expr

e, e′ ; σ

e′ ; σ ′′

===⇒ exres; σ ′
expr⋆

===⇒ exres; σ ′

expr⋆
exres; σ ′

Cases The evaluation relation for evaluating a series of cases has the form cs; v; σ ==⇒ vres; σ ′ ,
cases

and intuitively proceeds by sequentially evaluating each case (in cs) against value v until
one of them produces a non-fail result. For each case, the ﬁrst step is to match the given
value against target pattern and then evaluate the target expression under the set of possible matches; if the evaluation of the target expression produces a fail as result, the rest
of the cases are evaluated in a restored initial state (ECS-More-Fail) and otherwise the
result is propagated (ECS-More-Ord). If all possible cases are exhausted, the result is fail
(ECS-Emp).
ECS-Emp

ε; v; σ ===
⇒ fail; σ
cases

?

ρ; e; σ ==⇒ fail; σ ′′

σ ⊢ p := v ===⇒ ρ

case

match

cs; v; σ ===⇒ vres; σ ′
ECS-More-Fail

cases

case p ⇒ e, cs; v; σ ===
⇒ vres; σ ′
cases

?

ρ; e; σ ==⇒ vres; σ ′

σ ⊢ p := v ===⇒ ρ

case

match

ECS-More-Ord

vres 6= fail
case p ⇒ e, cs; v; σ ===
⇒ vres; σ ′
cases

Evaluating a single case—with relation ρ; e; σ ==⇒ vres; σ ′ —requires trying each possible
case

binding (in ρ) sequentially, producing fail if no binding is available (EC-Emp). If evaluating
target expression produces a non-fail value then it is propagated (EC-More-Ord), otherwise
the rest of the possible bindings are tried in a restored initial state (EC-More-Fail).
e; σρ ==⇒ fail; σ ′′
EC-More-Fail

expr

ρ, ρ′ ; e; σ

ρ′ ; e; σ ==⇒ vres; σ ′
==⇒
case

case
vres; σ ′

e; σρ ==⇒ vres; σ ′
EC-Emp

ε; e; σ ==⇒ fail; σ

EC-More-Ord

case

expr

vres 6= fail

ρ, ρ′ ; e; σ ==⇒ vres; (σ ′ \ dom ρ)
case

Traversals One of the key features of Rascal is visit-expressions which provide generic
traversals over data values and collections, allowing for multiple strategies to determine the
traversal ordering and halting conditions. In a traditional object-oriented language or functional language, transforming large structures is cumbersome and requires a great amount
of boilerplate, requiring a function for each type of datatype, where each function must
deconstruct the input data, applying target changes, recursively calling the right traversal
functions for traversal of further contained data and reconstructing the data with new values. Precisely, the ﬁrst-class handling of these aspects makes Rascal particularly suitable as
a high-level transformation language.
st
The main traversal relation cs; v; σ ==⇒ vres; σ ′ delegates execution to the correct strategyvisit

dependent traversal, and performs ﬁxed-point calculation if necessary. For the top-down-break

18

br

and top-down strategies it uses the top-down traversal relation cs; v; σ ====⇒ vres; σ ′ spectd−visit

ifying break and no no-break as breaking strategies respectively (EV-TD and EV-TDB);
this works analogously with the bottom-up-break (EV-BU and EV-BUB) and bottom-up
br

strategies using the cs; v; σ ====⇒ vres; σ ′ relation.
bu−visit

no-break

break

cs; v; σ ====⇒ vres; σ ′
EV-TD

cs; v; σ ====⇒ vres; σ ′

td−visit

td−visit

EV-TDB

top-down

cs; v; σ =====⇒ vres; σ ′

top-down-break

cs; v; σ =========⇒ vres; σ ′

visit

visit

no-break

break

cs; v; σ =====⇒ vres; σ ′
EV-BU

cs; v; σ =====⇒ vres; σ ′

bu−visit

bu−visit

EV-BUB

bottom-up

cs; v; σ ======⇒ vres; σ ′

bottom-up-break

cs; v; σ =========⇒ vres; σ ′

visit

visit

The innermost streatgy evaluates the bottom-up traversal as long as it produces a resulting
value not equal to the one from the previous iteration (EV-IM-Neq), returning the result
value when a ﬁxed-point is reached (EV-IM-Eq); if any exceptional result happens during
evaluation it will be propagated (EV-IM-Exc). Analogous evaluation steps happens with
outermost streatgy and top-down traversal (EV-OM-Neq, EV-OM-Eq, EV-OM-Exc).
no-break

no-break

cs; v; σ =====⇒ success v; σ ′
EV-IM-Eq

cs; v; σ =====⇒ exres; σ ′

bu−visit

bu−visit

EV-IM-Exc

innermost

cs; v; σ =====⇒ success v; σ ′

innermost

cs; v; σ =====⇒ exres; σ ′

visit

visit

no-break

cs; v; σ =====⇒ success v ′ ; σ ′′
EV-IM-Neq

bu−visit
innermost
cs; v ′ ; σ ′′ =====⇒
visit

v 6= v ′

vres; σ ′

innermost

cs; v; σ =====⇒ vres; σ ′
visit

no-break

no-break

cs; v; σ ====⇒ success v; σ ′
EV-OM-Eq

cs; v; σ ====⇒ exres; σ ′

td−visit

td−visit

EV-OM-Exc

outermost

cs; v; σ =====⇒ success v; σ ′
visit

visit

no-break

cs; v; σ ====⇒ success v ′ ; σ ′′
EV-OM-Neq

outermost

cs; v; σ =====⇒ exres; σ ′

td−visit
outermost
cs; v ′ ; σ ′′ =====⇒
visit
outermost

v 6= v ′

vres; σ ′

cs; v; σ =====⇒ vres; σ ′
visit

The top-down traversal strategy starts by executing all cases on the target value, scrutinee, applying possible replacements and eﬀects to produce an intermediate result value; the
traversal then continues on the sequence of contained values of the this intermediate result,
19

ﬁnally reconstructing a new output containing the possible replacement values obtained
(ETV-Ord-Sucs1, ETV-Ord-Sucs2). If using the break strategy, the traversal will stop
at the ﬁrst value that produces a successful result (ETV-Break-Sucs); otherwise, if any
sub-result produces a non-fail exceptional result it is propagated (ETV-Exc1, ETV-Exc2).
⇒ success v ′ ; σ ′
cs; v; σ ===

br = break

cases

ETV-Break-Sucs

br

cs; v; σ ====⇒ success v ′ ; σ ′
td−visit

cs; v; σ ===⇒ vfres; σ ′′
v ′′

br 6= break ∨ vfres = fail

cases

v ′′′ = children(v ′′ )

= if-fail(vfres, v)
br

cs; v ′′′ ; σ ′′ =====⇒ fail; σ ′
td−visit⋆

ETV-Ord-Sucs1

br

cs; v; σ ====⇒ vfres; σ ′
td−visit

cs; v; σ ===⇒
v ′′

cases

vfres; σ ′′

br 6= break ∨ vfres = fail
v ′′′ = children(v ′′ )

= if-fail(vfres, v)
br

cs; v ′′′ ; σ ′′ =====⇒ success v ′′′′ ; σ ′

recons v ′′ using v ′′′′ to rcres

td−visit⋆

ETV-Ord-Sucs2

br

cs; v; σ ====⇒ rcres; σ ′
td−visit

cs; v; σ ===⇒ exres; σ ′

exres 6= fail

cases

ETV-Exc1

br

cs; v; σ ====⇒ exres; σ ′
td−visit

cs; v; σ ===⇒ vfres; σ ′′
v ′′

br 6= break ∨ vfres = fail

cases

v ′′′ = children(v ′′ )

= if-fail(vfres, v)
br

cs; v ′′′ ; σ ′′ =====⇒ exres; σ ′
td−visit⋆

ETV-Exc2

exres 6= fail

br

cs; v; σ ====⇒ exres; σ ′
td−visit

Evaluating a sequence of top-down traversals, requires executing a top-down traversal for
each element, failing if the input sequence is empty (ETVS-Emp) and otherwise combining
the results (ETVS-More). If the break strategy is used, then the iteration will instead stop
at ﬁrst succesful result (ETVS-Break), and any non-fail exceptional result is propagated
(ETVS-Exc1, ETVS-Exc2).
ETVS-Emp

br

cs; ε; σ =====⇒ fail; σ
td−visit⋆

br

cs; v; σ ====⇒ success v ′′ ; σ ′
ETVS-Break

td−visit

br

br = break

cs; v, v ′ ; σ =====⇒ success v ′′ , v ′ ; σ ′
td−visit⋆

20

br

cs; v; σ ====⇒ vfres; σ ′′

br 6= break ∨ vfres = fail

td−visit

br

cs; v ′ ; σ ′′ =====⇒ vfres⋆′ ; σ ′
td−visit⋆

ETVS-More

br

cs; v, v ′ ; σ

=====⇒ vcombine(vfres, vfres⋆′ , v, v ′ ); σ ′
td−visit⋆
br

cs; v; σ ====⇒ exres; σ ′

exres 6= fail

td−visit

ETVS-Exc1

br

cs; v, v ′ ; σ =====⇒ exres; σ ′
td−visit⋆

br

cs; v; σ ====⇒ vfres; σ ′′

ETVS-Exc2

td−visit
br
′
cs; v ; σ ′′ =====⇒
td−visit⋆

br 6= break ∨ vfres = fail

exres; σ ′

exres 6= fail

br

cs; v, v ′ ; σ =====⇒ exres; σ ′
td−visit⋆

Bottom-up traversals work analogously to top-down traversals, except that traversal of
children and reconstruction happens before traversing the ﬁnal reconstructed value (EBUBreak-Sucs, EBU-No-Break-Sucs, EBU-Fail-Sucs). The analogy also holds with
propagation of exceptional results and errors (EBU-Exc, EBU-No-Break-Err, EBUNo-Break-Exc).
br

cs; v ′′ ; σ =====⇒ success v ′ ; σ ′

v ′′ = children(v)

bu−visit⋆

recons v using v ′ to rcres

br = break
EBU-Break-Sucs

br

cs; v; σ =====⇒ rcres; σ ′
bu−visit

br

cs; v ′′ ; σ =====⇒ success v ′′′ ; σ ′′

v ′′ = children(v)
br = no-break

bu−visit⋆
using v ′′′

recons v
to success v ′
⇒ vfres ′ ; σ ′
cs; v ′ ; σ ′′ ===
cases

EBU-No-Break-Sucs

br

cs; v; σ =====⇒ success if-fail(vfres ′ , v ′ ); σ ′
bu−visit

br

v ′′ = children(v)

cs; v ′′ ; σ =====⇒ fail; σ ′′

⇒
cs; v; σ ′′ ===
cases

EBU-Fail-Sucs

bu−visit⋆
vres; σ ′

br

cs; v; σ =====⇒ vres; σ ′
bu−visit

v ′ = children(v)

br

cs; v ′ ; σ =====⇒ exres; σ ′
bu−visit⋆

EBU-Exc

exres 6= fail

br

cs; v; σ =====⇒ exres; σ ′
bu−visit

br

v ′′ = children(v)

cs; v ′′ ; σ =====⇒ success v ′′′ ; σ ′

br = no-break

recons v using v ′′′ to error

EBU-No-Break-Err

bu−visit⋆

br

cs; v; σ =====⇒ error; σ ′
bu−visit

21

br

cs; v ′′ ; σ =====⇒ success v ′′′ ; σ ′′

v ′′ = children(v)

bu−visit⋆

recons v using v ′′′ to success v ′
cs; v ′ ; σ ′′ ===⇒ exres; σ ′

br = no-break

cases

EBU-No-Break-Exc

br

cs; v; σ =====⇒ exres; σ ′
bu−visit

Evaluating a sequence of bottom-up traversals is analogous to evaluating a sequence of topdown traversals. Each element in the sequence is evaluated and their results is combined
(EBUS-Emp,EBUS-More), stopping at the ﬁrst succesful result when using the break
strategy (EBUS-Break). Otherwise, non-fail exceptional results are propagated (EBUSExc1, EBUS-Exc2).
EBUS-Emp

br

cs; ε; σ =====⇒ fail; σ
bu−visit⋆

br

cs; v; σ =====⇒ success v ′′ ; σ
bu−visit

EBUS-Break

br = break

br

cs; v, v ′ ; σ =====⇒ success v ′′ , v ′ ; σ ′
bu−visit⋆

br

cs; v; σ =====⇒ vfres; σ ′′

br 6= break ∨ vfres = fail

bu−visit

br

cs; v ′ ; σ ′′ =====⇒ vfres⋆′ ; σ ′
bu−visit⋆

EBUS-More

cs; v, v ′ ; σ

br

=====⇒ vcombine(vfres, vfres⋆′ , v, v ′ ); σ ′
bu−visit⋆
br

cs; v; σ =====⇒ exres; σ ′
bu−visit

EBUS-Exc1

exres 6= fail

br

cs; v, v ′ ; σ =====⇒ exres; σ ′
bu−visit⋆

br

cs; v; σ =====⇒ vfres; σ ′′

EBUS-Exc2

bu−visit
br
′
cs; v ; σ ′′ =====⇒
bu−visit⋆

br 6= break ∨ vfres = fail

exres; σ ′

exres 6= fail

br

cs; v, v ′ ; σ =====⇒ exres; σ ′
bu−visit⋆

Auxiliary The children function extracts the directly contained values of the given input
value.
children(k(v)) = v

children(vb) = ε
children([v]) = v
′

children((v : v )) = v, v

children({v}) = v
′

children() = ε

vfres ::= success v | fail

22

The if-fail function will return a provided default value if the ﬁrst argument is fail, and
otherwise it will use the provided value in the ﬁrst argument.
if-fail(fail, v) = v

if-fail(success v ′ , v) = v ′

The vcombine function will combine success and fail results from visitor, producing fail if both
result arguments are fail otherwise producing success result, possibly using default values

vcombine(vfres, vfres⋆′ , v, v ′ ) =




fail

if



success



if-fail(vfres, v),
if-fail(vfres⋆′ , v ′ )



vfres = fail ∧
vfres ′ = fail

otherwise

The reconstruction relation recons v using v ′ to rcres tries to update the elements of a
value, checking whether provided values are type correct and deﬁned (not ), otherwise
producing an error.
rcres ::= success v | error

RC-Val-Sucs

recons vb using ε to success vb

RC-Val-Err

recons vb using v ′ , v ′′ to error

data at = . . . | k(t) | . . .
RC-Cons-Sucs

v ′ 6= 

t′ <: t

recons k(v) using v ′ to success k(v ′ )
data at = . . . | k(t) | . . .

RC-Cons-Err

v ′ : t′

vi =  ∨ t′i 6<: ti

recons k(v) using v ′ to error
v ′ 6= 

RC-List-Sucs

recons [v] using v ′ to success [v ′ ]

RC-List-Err

RC-Set-Sucs

vi′ = 
recons [v] using v ′ to error
v′ = 

recons {v} using v ′ to success {v ′ }

RC-Set-Err

RC-Map-Sucs

v ′ : t′

vi′ = 
recons {v} using v ′ to error
v ′′ 6= 

v ′′′ 6= 

recons (v : v ′ ) using v ′′ , v ′′′ to success (v ′′ : v ′′′ )

23

vi′′ =  ∨ vi′′′ = 
recons (v : v ′ ) using v ′′ , v ′′′ to error

RC-Map-Err

RC-Bot-Sucs

recons  using ε to success 

RC-Bot-Err

recons  using v ′ , v ′′ to error

Enumeration The enumeration relation e; ρ; σ ==⇒ vres; σ ′ iterates over all provided bindeach

ings (EE-More-Sucs) until there are none left (EE-Emp) or the result is neither an ordinary
value or continue from one of the iterations (EE-More-Exc); in case the result is break the
evaluation will terminate early with a succesful result (EE-More-Break).
EE-Emp

e; ε; σ ==⇒ success ; σ
each

e; σρ ==⇒
expr

vres; σ ′′

vres = success v ∨ vres = continue

e; ρ′ ; (σ ′′ \ dom ρ) ==⇒ vres ′ ; σ ′
each

EE-More-Sucs

e; ρ, ρ′ ; σ

==⇒ vres ′ ; σ ′
each

e; σρ ==⇒ break; σ ′
EE-More-Break

e; σρ ==⇒
expr

EE-More-Exc

expr

e; ρ, ρ′ ; σ
exres; σ ′

==⇒ success ; (σ ′ \ dom ρ)
each

exres ∈ {throw v, return v, fail, error}

e; ρ, ρ′ ; σ ==⇒ exres; (σ ′ \ dom ρ)
each

Generator expressions The evaluation relation for generator expressions has form
g; σ ===⇒ envres; σ ′ . For matching assignments the target right-hand side expression is evalgexpr

uated ﬁrst—propagating possible exceptional results (G-Pat-Exc) and then the value is
matched against target pattern (G-Pat-Sucs).
envres ::= success ρ
~ | exres
e; σ ==⇒ success v; σ ′
G-Pat-Sucs

expr

?

σ ′ ⊢ p := v ===⇒ ρ~
match

p := e; σ ===⇒ success ρ
~; σ ′
gexpr

e; σ ==⇒ exres; σ ′
G-Pat-Exc

expr

p := e; σ ==⇒ exres; σ ′
expr

For enumerating assignments, each possible value in a collection is provided as a possible
binding to the range variable in the output (G-Enum-List, G-Enum-Set); for maps in
24

particular, only the keys are bounds (G-Enum-Map). An error is raised if the result value is
not a collection (G-Enum-Err), and exceptions are propagated as always (G-Enum-Exc).
e; σ ==⇒ success [v1 , . . . , vn ]; σ ′
G-Enum-List

expr

x ← e; σ ===⇒ success [x 7→ v1 ], . . . , [x 7→ vn ]; σ ′
gexpr

e; σ ==⇒ success {v1 , . . . , vn }; σ ′
expr

G-Enum-Set

x ← e; σ ===⇒ success [x 7→ v1 ], . . . , [x 7→ vn ]; σ ′
gexpr

e; σ ==⇒ success (v1 : v1′ , . . . , vn : vn′ ); σ ′
G-Enum-Map

expr

x ← e; σ ===⇒ success [x 7→ v1 ], . . . , [x 7→ vn ]; σ ′
gexpr

e; σ ==⇒ success v; σ ′
expr

G-Enum-Err

v = vb ∨ v = k(v ′ ) ∨ v = 

x ← e; σ ===⇒ error; σ ′
gexpr

e; σ ==⇒ exres; σ ′
expr

G-Enum-Exc

x ← e; σ ===⇒ exres; σ ′
gexpr

Pattern Matching
?

The pattern matching relation σ ⊢ p := v ===⇒ ρ takes as input the current store σ, a pattern
match

p and a target value v and produces a sequence of compatible environments that represent
possible bindings of variables to values. Pattern matching a basic value against target value
produces a single environment that does not bind any variable ([]) if the target value is the
same basic value (P-Val-Sucs) and otherwise does not produce any binding environment
(ε), (P-Val-Fail).
P-Val-Sucs

v 6= vb

P-Val-Fail

?

σ ⊢ vb := vb ===⇒ []

?

σ ⊢ vb := v ===⇒ ε

match

match

Pattern matching against a variable depends on whether the variable already exists in the
current store. If it is assigned in the current store, then the target value must the assigned
value to return a possible binding (P-Var-Uni) and otherwise failing with no bindings (PVar-Fail); if it is not in the current store, it will simply bind the variable to the target
value (P-Var-Bind).
P-Var-Uni

x ∈ dom σ

v = σ(x)

?

P-Var-Fail

σ ⊢ x := v ===⇒ []

v 6= σ(x)

?

σ ⊢ x := v ===⇒ ε

match

P-Var-Bind

x ∈ dom σ

match

x∈
/ dom σ
?

σ ⊢ x := v ===⇒ [x 7→ v]
match

25

When pattern matching against a constructor pattern, it is ﬁrst checked whether the target
value has the same constructor. If it does, then the sub-patterns are matched against the
contained values of the target value, merging their resulting environments (P-Cons-Sucs),
and otherwise failing with no bindings (P-Cons-Fail). The merging procedure is described
formally later in this section, but it intuitively it takes the union of all bindings that have
consistent assignments to the same variables.
?

σ ⊢ p1 := v1 ===⇒ ρ1
match

P-Cons-Sucs

?

σ ⊢ pn := vn ===⇒ ρn

...

match

?

σ ⊢ k(p) := k(v) ===⇒ merge(ρ1 , . . . , ρn )
match

v 6= k(v ′ )
P-Cons-Fail

?

σ ⊢ k(p) := v ===⇒ ε
match

When pattern matching against a typed labeled pattern, the target value is checked to have
a compatible type—failing with no bindings otherwise (P-Type-Fail)— and then then the
inner pattern is matched against the same value. The result of the sub-pattern match is
merged with the environment where the target value is bound to the label variable (PType-Sucs).
v : t′

?

t′ <: t

P-Type-Sucs

σ ⊢ p := v ===⇒ ρ
match

?

σ ⊢ t x : p := v ===⇒ merge([x 7→ v], ρ)
match

v : t′

P-Type-Fail

t′ 6<: t
?

σ ⊢ t x : p := v ===⇒ ε
match

Pattern matching against a list pattern ﬁrst checks whether the target value is a list—
otherwise failing (P-List-Fail)—and then pattern matches against the sub-patterns returning their result (P-List-Sucs).
?

[]

,

σ ⊢ ⋆p := v | ∅ ====⇒ ρ

v 6= [v ′ ]

match⋆

P-List-Sucs

P-List-Fail

?

σ ⊢ [⋆p] := [v] ===⇒ ρ

?

σ ⊢ [⋆p] := v ===⇒ ε

match

match

Pattern matching against a set pattern is analogous to pattern matching against list patterns
(P-Set-Sucs, P-Set-Fail).
?

{}

⊎

σ ⊢ ⋆p := v | ∅ ====⇒ ρ
P-Set-Sucs

v 6= {v ′ }

match⋆

P-Set-Fail

?

σ ⊢ {⋆p} := {v} ===⇒ ρ
match

26

?

σ ⊢ {p} := v ===⇒ ε
match

Negation pattern !p matching succeeds with no variables bound if the sub-pattern p produces
no binding environment (P-Neg-Sucs), and otherwise fails (P-Neg-Fail).
?

?

σ ⊢ p := v ===⇒ ε

σ ⊢ p := v ===⇒ ρ

match

P-Neg-Sucs

match

P-Neg-Fail

?

ρ 6= ε

?

σ ⊢!p := v ===⇒ []

σ ⊢!p := v ===⇒ ε

match

match

Descendant pattern matching applies the sub-pattern against target value, and keeps applying the deep matching pattern against the children values, concatenating their results
(P-Deep).
?

v1′ , . . . , vn′ = children(v)

σ ⊢ p := v ===⇒ ρ
match

?

σ ⊢ /p := v1′ ===⇒ ρ′1
match

P-Deep

?

σ ⊢ /p := vn′ ===⇒ ρ′n

...

match

?

σ ⊢ /p := v ===⇒ ρ, ρ′1 , . . . , ρ′n
match

?

hi

⊗

The star pattern matching relation has form σ ⊢ ⋆p := v | V ====⇒ ρ which tries to match
match⋆

the sequence of patterns ⋆p on the left-hand side with sequence of provided values v on the
right-hand side. The relations is parameterized over the construction function (hi) and the
partition relation (⊗), and because matching is non-deterministic we keep track of a set of
value sequences V that have already been tried for each element in the pattern sequence.
If both the pattern sequence and the value sequence is empty, then we have successfully
ﬁnished matching (PL-Emp-Both). Otherwise if the pattern sequence ﬁnishes while there
are still values left to match (PL-Emp-Pat) we fail, producing no bindings.
PL-Emp-Both

?

hi

PL-Emp-Pat

⊗

?

hi

⊗

σ ⊢ ε := v, v ′ | V ====⇒ ε

σ ⊢ ε := ε | V ====⇒ []

match⋆

match⋆

The PL-More-Pat-Re rule tries to partition the input sequence of values into a single
v ′ element that is matched against target pattern p, and a sequence of elements v ′′ that
are matched against the rest of the pattern sequence ⋆p. Additionally the rule will try to
backtrack, excluding the selected value v ′ from the values tried for pattern p; in practice
there is only one valid partition for elements of a list, but for elements of sets there can
be many due to commutativity of partitioning. If all valid partitions have been tried, the
PL-More-Pat-Exh rule is used to end the backtracking for the pattern p.
v = v ′ ⊗ v ′′
?

σ ⊢ ⋆p :=

v ′′

hi

⊗

| ∅ ====⇒

PL-More-Pat-Re

?

σ ⊢ p := v ′ ===⇒ ρ

v′ ∈
/V
match⋆

ρ′

?

σ ⊢ p, ⋆p := v | V ∪

?

hi

⊗

match
hi ⊗
′
{v } ====⇒
match⋆

σ ⊢ p, ⋆p := v | V ====⇒ merge(ρ, ρ′ ), ρ′′
match⋆

∄v ′ , v ′′ .v = v ′ ⊗ v ′′ ∧ v ′ ∈
/V
PL-More-Pat-Exh

?

hi

⊗

σ ⊢ p, ⋆p := v | V ====⇒ ε
match⋆

27

ρ′′

Like ordinary variables, arbitrary matching patterns depend on whether the binding variable
already exists in the current store. If the variable is assigned in the current store then either
there must exist a partition of values that has a matching subcollection (PL-More-StarUni), or the matching fails producing any consistent binding environment (PL-More-StarPat-Fail, PL-More-Star-Val-Fail).
x ∈ dom σ

v = v ′ ⊗ v ′′

σ(x) = hv ′ i
?

hi

⊗

σ ⊢ ⋆p := v ′′ | ∅ ====⇒ ρ
match⋆

PL-More-Star-Uni

?

hi

⊗

σ ⊢ ⋆x, ⋆p := v | V ====⇒ ρ
match⋆

x ∈ dom σ

σ(x) = hv ′ i

PL-More-Star-Pat-Fail

∄v ′′ .v = v ′ ⊗ v ′′

?

hi

⊗

σ ⊢ ⋆x, ⋆p := v | V ====⇒ ε
match⋆

x ∈ dom σ

v 6= hv ′ i

σ(x) = v

PL-More-Star-Val-Fail

?

hi

⊗

σ ⊢ ⋆x, ⋆p := v ′′ | V ====⇒ ε
match⋆

If the variable is not in the current store then there are two options: either i) there still
exist a partition that is possible to try, or ii) we have exhausted all possible partitions of
the value sequence. In the ﬁrst case, an arbitrary partition is bound to the target variable
and the rest of the patterns are matched against the rest of the values, merging their results;
additionally, the other partitions are also tried concatenating their results with the merged
one (PL-More-Star-Re). In the exhausted case, the pattern match produces no bindings
(PL-More-Star-Exh).
v = v ′ ⊗ v ′′

x∈
/ dom σ
?

hi

⊗

σ ⊢ ⋆p := v ′′ | ∅ ====⇒ ρ
match⋆

PL-More-Star-Re

?

v′ ∈
/V
?

hi

⊗

σ ⊢ ⋆x, ⋆p := v | V ∪ {v ′ } ====⇒ ρ′
match⋆

hi

⊗

σ ⊢ ⋆x, ⋆p := v | V ====⇒ merge([x 7→ hv ′ i], ρ), ρ′
match⋆

x∈
/ dom σ
PL-More-Star-Exh

∄v ′ , v ′′ .v = v ′ ⊗ v ′′ ∧ v ′ ∈
/V
?

hi

⊗

σ ⊢ ⋆x, ⋆p := v | V ====⇒ ε
match⋆

Merging a sequence of possible variable bindings produces a sequence containing consistent
variable bindings from the sequence: that is, all possible environments that assign consistent
values to the same variables are merged.
merge(ε) = []
merge(ρ, ρ′1 , . . . , ρ′n )

= merge-pairs(ρ × merge(ρ′1 , . . . , ρ′n ))

merge-pairs(hρ1 , ρ′1 i, . . . , hρn , ρ′n i) = merge-pair(ρ1 , ρ′1 ), . . . , merge-pair(ρn , ρ′n )

28

(
ρρ′
merge-pair(ρ, ρ ) =
ε
′

4

if ∀x ∈ dom ρ ∩ dom ρ′ .ρ(x) = ρ′ (x)
otherwise

Semantics Properties

Backtracking is pure in Rascal (Light) programs, and so if evaluating a set cases produces
fail as result, the initial state is restored.
CS
Theorem 1 (Backtracking purity). If cs; v; σ ==⇒ fail; σ ′ then σ ′ = σ
cases

Strong typing is an important safety property of Rascal, which I capture by specifying a
theorems with two result properties: one about the well-typedness of state, and the other
about well-typedness of resulting values.
Theorem 2 (Strong typing). Assume that semantic unary J⊖K and binary operators J⊕K
E
T
for each
are strongly typed. If e; σ ==⇒ vres; σ ′ and there exists a type t such that
v
:t
expr
value in the input store v ∈ img σ, then
1. There exists a type t′ such that v ′ : t′ for each value in the result store v ′ ∈ img σ ′ .
2. If the result value vres is either success v ′′ , return v ′′ , or throw v ′′ , then there exists a
type t′′ such that v ′′ : t′′ .
Consider an augmented version of the operational semantics where each execution relation
is annotated with partiality fuel (Amin and Rompf, 2017)—represented by a superscript natural number n—which speciﬁes the maximal number of recursive premises allowed in the
derivation. The fuel is subtracted on each recursion, resulting in a timeout value when it
reaches zero, and the rule set is amended by congruence rules which propagate timeout results
from the recursive premises to the conclusion.
vtres ::= vres | timeout

For this version of the semantics, we can specify the property that execution will either
produce a result or it will timeout; that is, the semantics does not get stuck.
Theorem 3 (Partial progress). It is possible to construct a derivation e; σ ==⇒n vtres; σ ′ for
expr

any input expression e, well-typed store σ and fuel n.
Finally, consider a subset of the expression language described by syntactic category efin ,
where while-loops, solve-loops and function calls are disallowed, and similarly with all traversal strategies except bottom-up and bottom-up-break. This subset is known to be terminating:

29

Theorem 4 (Terminating expressions). There exists n such that derivation
E
efin ; σ ==⇒n vres; σ ′ has a result vres which is not timeout for expression efin in the
expr

terminating subset.
Remark 1. Why is the top-down traversal strategy potentially non-terminating while the
bottom-up traversal strategy is terminating? The answer lies in that the top-down traverses the children of the target expression after evaluating the required case, which makes
it possible to keep add children ad inﬁnitum as illustrated by the following example:
1

data Nat = zero() | succ(Nat pred);

2
3
4
5
6

5

Nat infincrement(Nat n) =
top-down visit(n) {
case succ(n) => succ(succ(n))
}

Formal Semantics, Types and Intented Semantics

This formal speciﬁcation of Rascal Light was largely performed when the oﬃcial type checker
of Rascal (developed by CWI Amsterdam) was only at the experimental stage. Useful
extension of this formalization include a deductive type system that includes polymorphic
aspects of Rascal to prove the consistency of the type system, and type safety with regards
to the dynamic semantics provided in this formalization.
The presented semantics was checked against the Rascal implementation in various ways:
the existing implementation was used as a reference point, rules for individual were held
up against the documentation, and correspondence with the Rascal developers was used to
clarify remaining questions. A more formal way to check whether the captured semantics
is the intended one, is to construct an independent formal semantics which is related to
the natural semantics presented in this report. This could be an axiomatic semantics Hoare
(1969), which modularly speciﬁes for each construct the intented eﬀects using logical formulae
as pre and post-conditions, without necessarily specifying how each construct is evaluated.
The natural semantics would then be checked to satisfy the axiomatic semantics for each
construct, which will further increase conﬁdence that the captured semantics is the intented
one.

6

Conclusion

I presented the formalization of a large subset of the operational part of Rascal Klint et al.
(2009, 2011), called Rascal Light. The formalization was primarily based on the available
open source implementation3 and the accompanying documentation4 , and personal correspondence with the developers further clariﬁed previous ambiguities and mismatches.
3
4

https://github.com/usethesource/rascal
http://tutor.rascal-mpl.org/

30

Acknowledgments
This report is partially funded by by Danish Council for Independent Research, grant no.
0602-02327B. I would like to thank Paul Klint and the Rascal team at CWI Amsterdam for
answering my questions about Rascal and provide corrections to this report. I would also
like to thank Aleksandar Dimovski and Andrzej Wąsowski for proofreading and commenting
on this report.

References
Nada Amin and Tiark Rompf. Type soundness proofs with deﬁnitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages,
POPL 2017, Paris, France, January 18-20, 2017, pages 666–679, 2017. URL http://dl.
acm.org/citation.cfm?id=3009866.
G.M. Bierman, M.J. Parkinson, and A.M. Pitts. An imperative core calculus for Java and
Java with eﬀects. Technical Report 563, University of Cambridge Computer Laboratory,
April 2003.
Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C
language. J. Autom. Reasoning, 43(3):263–288, 2009. doi: 10.1007/s10817-009-9148-3.
URL http://dx.doi.org/10.1007/s10817-009-9148-3.
CWI Amsterdam.
Abstract syntax tree of muRascal.
online, February 2017.
URL
https://web.archive.org/web/20170726155735/https://raw.
githubusercontent.com/usethesource/rascal/master/src/org/
rascalmpl/library/experiments/Compiler/muRascal/AST.rsc.
C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):
576–580, 1969. doi: 10.1145/363235.363259. URL http://doi.acm.org/10.1145/
363235.363259.
Gilles Kahn. Natural semantics. In STACS 87, 4th Annual Symposium on Theoretical Aspects
of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, pages 22–39,
1987. doi: 10.1007/BFb0039592. URL https://doi.org/10.1007/BFb0039592.
Paul Klint, Tijs van der Storm, and Jurgen J. Vinju. RASCAL: A domain speciﬁc language for source code analysis and manipulation. In Ninth IEEE International Working
Conference on Source Code Analysis and Manipulation, SCAM 2009, Edmonton, Alberta,
Canada, September 20-21, 2009, pages 168–177, 2009. doi: 10.1109/SCAM.2009.28. URL
https://doi.org/10.1109/SCAM.2009.28.
Paul Klint, Tijs van der Storm, and Jurgen Vinju. EASY Meta-programming with Rascal. In
JoãoM. Fernandes, Ralf Lämmel, Joost Visser, and João Saraiva, editors, Generative and
Transformational Techniques in Software Engineering III, volume 6491 of Lecture Notes

31

in Computer Science, pages 222–289. Springer Berlin Heidelberg, 2011. ISBN 978-3-64218022-4. doi: 10.1007/978-3-642-18023-1_6. URL http://dx.doi.org/10.1007/
978-3-642-18023-1_6.
Xavier Leroy. The Caml Light system, documentation and user’s guide 0.74. https://
caml.inria.fr/pub/docs/manual-caml-light/, December 1997.
Robin Milner, Mads Tofte, and Robert Harper. Definition of standard ML. MIT Press, 1990.
ISBN 978-0-262-63132-7.
Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program.,
60-61:17–139, 2004.

A

Semantics Properties Proofs

CS
Theorem 1 (Backtracking purity). If cs; v; σ ==⇒ fail; σ ′ then σ ′ = σ
cases

Proof. By induction on the derivation CS:
• Case CS = ECS-Emp

ε; v; σ ===⇒ fail; σ

, so cs = ε and σ ′ = σ. Holds by deﬁnition.

cases

M

C
ρ; e; σ ==⇒ fail; σ ′′

?

σ ⊢ p := v ===⇒ ρ

case

match

CS ′
′
cs ; v; σ ===⇒ fail; σ ′

• Case CS

=

ECS-More-Fail

cases

case p ⇒ e, cs ′ ; v; σ ===⇒ fail; σ ′

, so cs

=

cases

(case p ⇒ e, cs ′ ) and vres = fail.
– By inductive hypothesis of CS ′ we get σ ′ = σ.

• Note: the rule ECS-More-Ord is inapplicable since its premise states that the result
value vres 6= fail.

In order to prove Theorem 2, we need to state some helper lemmas about sub-derivations.
We have a lemma for the auxiliary merge function:
Lemma 1. If we have ρ′ = merge(ρ1 , . . . , ρn ) and for each value v ∈ img ρi,j in an environment in the input sequence of environment sequences ρ1 , . . . , ρn there exists a type t so
that v : t, then we have that for each value v ′ ∈ img ρ′k in an environment in the resulting
environment sequence ρ′ we have a type t′ so that v ′ : t′
Proof. Follows directly from the premises by induction of the input sequence of environment
sequences ρ1 , . . . , ρn
32

We have a lemma for the auxiliary children function:
Lemma 2. For a value v such that we have v ′ = children(v) and

T
, then there exists a
v:t

type sequence t′ such that v ′ : t′
Proof. By induction on the syntax of v:
• Cases v = vb and v = , so v ′ = ε. Holds trivially.
• Case v = k(v ′ )
– By inversion we get
T′
v : t′

data at = . . . | k(t′′ ) | . . .
T-Constructor

ST′
t <: t′′
′

k(v ′ ) : at

so t = at
– Here, T′ exactly represents our target goal
• Case v = [v ′ ]
T′
v : t′
F
T-List
[v ′ ] : listh t′ i
′

– By inversion we get T =

– Here, T′ exactly represents our target goal

F
, so t = listh t′ i

• Case v = {v ′ }
T′
v : t′
′

– By inversion we get T = T-Set

′

F
{v } : seth t′ i

– Here, T′ exactly represents our target goal

F
, so t = seth t′ i

• Case v = (v ′′ : v ′′′ ), so v ′ = v ′′ , v ′′′
– By inversion we get
T′′
v : t′′

T′′′
v : t′′′
T-Map
F F
(v ′′ : v ′′′ ) : maph t′′ , t′′′ i
′′

T=

′′′

– Here we take the concatenation of the premises T′′ , T′′′ to fulﬁll our goal.

We have two mutually recursive lemmas on pattern matching: Lemma 3 and Lemma 4.

33

M
Lemma 3. If

and there exists a type t such that

?

σ ⊢ p := v ===⇒ ρ
match

′

T
and a type t′
v:t

′

such that v : t for each value in the input store v ′ ∈ img σ, then we have a type t′′ for each
value v ′′ ∈ img ρi in an environment in the output sequence ρ.
Proof. By induction on the derivation M:
• Cases M = P-Val-Sucs, M = P-Val-Fail, M = P-Var-Uni, M = P-Var-Fail,
M = P-Cons-Fail, M = P-Type-Fail, M = P-List-Fail, M = P-Set-Fail,
M = P-Neg-Sucs, M = P-Neg-Fail hold trivially since we have that the output
environment sequence ρ = [] or ρ = ε, in both cases containing no values.
• Case M = P-Var-Bind holds by the premise derivation T.
?

M1′

...

σ ⊢ p′1 := v1′ ===⇒ ρ′1

?

σ ⊢ p′n := vn′ ===⇒ ρ′n

match

• Case M = P-Cons-Sucs

?

Mn′
match

, so p = k(p′ ),

′

σ ⊢ k(p′ ) := k(v ) ===⇒ merge(ρ′1 , . . . , ρ′n )
match

v = k(v ′ ) and ρ = merge(ρ′1 , . . . , ρ′n )
– By inversion we get
data at = . . . | k(t′′ ) | . . .

T = T-Constructor

T′
v : t′

ST′
t′ <: t′′

k(v1′ , . . . , vn′ ) : at

so t = at
– Now by induction hypotheses of M′ using T′ , and then using Lemma 1 we get
that ρ has well-typed values.
• Case M = P-Type-Sucs holds by the premise derivation T and Lemma 1.
MS ′
σ ⊢ ⋆p

?
′ :=

• Case M = P-List-Sucs
′

[]

,

v ′ | ∅ ====⇒ ρ
match⋆

?

, so p = [⋆p′ ] and v = [v ′ ]

′

σ ⊢ [⋆p ] := [v ] ===⇒ ρ
match

T′
v : t′
F
T-List
[v ′ ] : listh t′ i
′

– By inversion we get T =

F
, so t = listh t′ i

– Partitioning lists by splitting on concatenation , preserves typing since we can for
each value pick the corresponding type derivation in the sequence.
– By induction hypothesis (using Lemma 4) of MS ′ using T′ and above fact we get
that ρ has well-typed values.
MS ′
σ ⊢ ⋆p

?
′ :=

• Case M = P-Set-Sucs
′

[]

,

v ′ | ∅ ====⇒ ρ
match⋆

?

′

σ ⊢ {⋆p } := {v } ===⇒ ρ
match

34

, so p = {⋆p′ } and v = {v ′ }

T′
v : t′
′

– By inversion we get T = T-Set

′

F
{v } : seth t′ i

F
, so t = seth t′ i

– Partitioning sets using disjoint union ⊎ preserves typing of value sub-sequences,
since we can for each value vi in a subsequence pick the corresponding typing
derivation Ti ′
– By induction hypothesis (using Lemma 4) of MS ′ using T′ and above fact we get
that ρ has well-typed values.
M′
σ⊢p

?
′ :=

v1′ , . . . , vn′ = children(v)

v ===⇒ ρ′
match

M1′′

σ ⊢ /p

?
′ :=

• Case M = P-Deep

...

v1′ ===⇒ ρ′′1
match

σ ⊢ /p

?
′ :=

Mn′′

σ ⊢ /p

?
′ :=

vn′ ===⇒ ρ′′n
match

v ===⇒ ρ′ , ρ′′1 , . . . , ρ′′n
match

– By induction hypothesis on M′ , we get that ρ′ has well-typed values
– By using Lemma 2 on v ′ , we get

T′
v ′ : t′

– By induction hypotheses on M′′ using T′ we get that ρ′′1 , . . . , ρ′′n is well-typed
– Now, we can show that ρ′ , ρ′′1 , . . . , ρ′′n is well-typed using above facts

MS
Lemma 4. If

?

hi

⊗

σ ⊢ ⋆p := v | V ====⇒ ρ

and the following properties hold:

match⋆

1. There exists a type sequence t such that v : t
2. There exists a type t′ such that v ′ : t′ for each value in the input store v ′ ∈ img σ
3. There exists a type t′ such that v ′ : t′ for each value in the visited value set v ′ ∈ V
4. If for all value sequences v ′ , v ′′ , v ′′′ where we have v ′ = v ′′ ⊗ v ′′′ and there exists a type
sequence t′ so v ′ : t′ , then we have that there exists two type sequences t′′ and t′′′ so that
v ′′ : t′′ and v ′′′ : t′′′
Then we have a type t′ so that v ′ : t′ for each value v ′ ∈ img ρi in an environment in the
output sequence ρ.
Proof. By induction on the derivation MS:
• Cases MS = PL-Emp-Both, MS = PL-Emp-Pat, MS = PL-More-Pat-Exh,
MS = PL-More-Star-Pat-Fail, MS = PL-More-Star-Val-Fail, and MS =
PL-More-Star-Exh hold trivially since we have ρ = [] or ρ = ε, and there are no
values in either [] or ε.
35

• Case MS = PL-More-Pat-Re holds by induction hypotheses (including Lemma 3),
and Lemma 1.
x ∈ dom σ

v = v ′ ⊗ v ′′

σ(x) = hv ′ i
MS ′
?

hi

⊗

σ ⊢ ⋆p′ := v ′′ | ∅ ====⇒ ρ
match⋆

• Case MS = PL-More-Star-Uni
σ ⊢ ⋆x, ⋆p

?
′ :=

hi

⊗

, so ⋆p = ⋆x, ⋆p′ .

v | V ====⇒ ρ
match⋆

By property 4 we can derive that there exists a type sequence t′′ such that v ′′ : t′′ . Then
we can apply induction hypothesis on derivation MS ′ , and get our target result.
• Case MS = PL-More-Star-Re holds by induction hypotheses (including Lemma 3),
and Lemma 1.

We have a lemma on the auxiliary function if-fail:
Lemma 5. If we have v ′ = if-fail(vfres, v ′′), and:
1. If vfres = success v, then we have v : t for some type t
2. We have v ′′ : t′′ for somet type t′′
Then there exists a type t′ such that v ′ : t′
Proof. Straightforwardly by case analysis on vfres
Similarly, we have a lemma on the auxiliary function vcombine
Lemma 6. If we have vfres⋆′′ = vcombine(vfres, vfres⋆′ , v, v ′), and:
1. If vfres = success v ′′′ , then we have v ′′′ : t′′′ for some type t
2. If vfres⋆′ = success v ′′′′ , then we v ′′′′ : t′′′′ for some typing sequence t′′′′
3. We have v : t for somet type t
4. We have v ′ : t′ for somet type t′
Then if vfres⋆′′ = success v ′′ there exists a type sequence t′′ such that v ′′ : t′′
Proof. Straightforwardly by case analysis on vfres and vfres⋆′ and using Lemma 5.
We have a lemma on the reconstruct derivation:
RC
, v : t for some type t, and v ′ : t′ for
recons v using v ′ to rcres
some type sequence t′ , then when rcres = success v ′′ there exists a type t′′ such that if v ′′ : t′′
Lemma 7. If we have

Proof. By induction on the derivation RC:
36

• Cases RC = RC-Val-Err, RC = RC-Cons-Err, RC = RC-List-Err, RC =
RC-Set-Err, RC = RC-Map-Err, RC = RC-Bot-Err hold trivially.
• Case RC = RC-Val-Sucs holds using the premises.
• Case RC = RC-Cons-Sucs holds using the premises and rule T-Constructor.
• Case RC = RC-List-Sucs holds using the premises and rule T-List.
• Case RC = RC-Set-Sucs holds using the premises and rule T-Set.
• Case RC = RC-Map-Sucs holds using the premises and rule T-Map.
• Case RC = RC-Bot-Sucs holds using the premises and rule T-Bot.

We now have a series of mutually inductive lemmas with our Theorem 2, since the
operational semantics rules are mutually inductive themselves. The lemmas are Lemma 8,
Lemma 9, Lemma 10, Lemma 11, Lemma 12, Lemma 13, Lemma 14, Lemma 15, Lemma 16,
and Lemma 17.
ES
Lemma 8. If e; σ ===⇒ vres⋆; σ ′ and there exists a type t such that v : t for each value in
expr⋆

the input store v ∈ img σ, then
1. There exists a type t′ such that v ′ : t′ for each value in the result store v ′ ∈ img σ ′ .
2. If the result value vres⋆ is success v ′′ , then there exists a type sequence t′′ such that
v ′′ : t′′ .
3. If the result value vres⋆ is either return v ′′ , or throw v ′′ , then there exists a type t′′ such
that v ′′ : t′′
Proof. By induction on the derivation ES:
• Case ES = ES-Emp holds directly using premises.
• Cases ES = ES-More, ES = ES-Exc1 and ES = ES-Exc2 hold directly from the
induction hypotheses (including the one given by Theorem 2).

EE
Lemma 9. If e; ρ; σ ==⇒ vres; σ ′ , there exists a type t such that v : t for each value in
each

the input store v ∈ img σ, and there exists a type t such that v : t for each value in an
environment v ∈ img ρi in the environment sequence ρ then
1. There exists a type t′ such that v ′ : t′ for each value in the result store v ′ ∈ img σ ′ .
2. If the result value vres is either success v ′′ , return v ′′ , or throw v ′′ , then there exists a
type t′′ such that v ′′ : t′′
37

Proof. By induction on the derivation EE:
• Case EE = EE-Emp holds directly using the premises.
• Cases EE = EE-More-Sucs, EE = EE-More-Break and EE = EE-More-Exc hold
directly from the induction hypotheses (including Theorem 2), and the (trivial) facts
that if any store σ is well-typed then σ \ X is well-typed for any set of variables X and
σρ is well-typed for any well-typed environment ρ.

G
Lemma 10. If g; σ ===⇒ envres; σ ′ , and there exists a type t such that v : t for each value
gexpr

in the input store v ∈ img σ then
1. There exists a type t′ such that v ′ : t′ for each value in the result store v ′ ∈ img σ ′ .
2. If the result value envres is success ρ, then there exists a type t′′ for each value in an
environment v ′′ ∈ ρi in the environment sequence ρ such that v ′′ : t′′
3. If the result value envres is either return v ′′′ , or throw v ′′′ , then there exists a type t′′′
such that v ′′′ : t′′′
Proof. By induction on the derivation G:
• Cases G = G-Pat-Sucs and G = G-Pat-Exc hold directly by induction hypothesis
given by Theorem 2, and then using Lemma 3 if necessary.
• Cases G = G-Enum-List, G = G-Enum-Set and G = G-Enum-Map hold by the induction hypothesis given by Theorem 2 and then using inversion on the type derivation
of the result collection value to extract the type derivations of the contained values in
the result environments (from rules T-List, T-Set, and T-Map respectively).
• Cases G = G-Enum-Err and G = G-Enum-Exc hold directly by the induction
hypothesis given by Theorem 2.

C
Lemma 11. If ρ; e; σ ==⇒ vres; σ ′ , there exists a type t such that v : t for each value in an
case

environment v ∈ img ρi in the environment sequence ρ, and there exists a type t such that
v : t for each value in the input store v ∈ img σ, then
1. There exists a type t′ such that v ′ : t′ for each value in the result store v ′ ∈ img σ ′ .
2. If the result value vres is either success v ′′ , return v ′′ , or throw v ′′ , then there exists a
type t′′ such that v ′′ : t′′
Proof. By induction on derivation C:
• Case C = EC-Emp holds directly using the premises.
38

• Case C = EC-More-Fail and C = EC-More-Ord hold directly using induction
hypotheses (including Theorem 2) and the facts of well-typedness of store extension
by well-typed environments and well-typedness of variable removals from stores.

CS
Lemma 12. If cs; v; σ ==⇒ vres; σ ′ , there exists a type t such that v : t , and there exists
cases

a type t′ such that v ′ : t′ for each value in the input store v ′ ∈ img σ, then
1. There exists a type t′′ such that v ′′ : t′′ for each value in the result store v ′′ ∈ img σ ′ .
2. If the result value vres is either success v ′′′ , return v ′′′ , or throw v ′′′ , then there exists a
type t′′′ such that v ′′′ : t′′′
Proof. By induction on the derivation CS:
• Case CS = ECS-Emp holds directly using the premises.
• Cases CS = ECS-More-Fail and CS = ECS-More-Fail hold using Lemma 3 and
the induction hypotheses (including Lemma 11).

Lemma 13. If

V
st
, there exists a type t such that v : t , and there exists
cs; v; σ ==⇒ vres; σ ′
visit

a type t′ such that v ′ : t′ for each value in the input store v ′ ∈ img σ, then
1. There exists a type t′′ such that v ′′ : t′′ for each value in the result store v ′′ ∈ img σ ′ .
2. If the result value vres is either success v ′′′ , return v ′′′ , or throw v ′′′ , then there exists a
type t′′′ such that v ′′′ : t′′′
Proof. By induction on the derivation V:
• Cases V = EV-TD, V = EV-TDB, V = EV-OM-Eq, V = EV-OM-Neq and V =
EV-OM-Exc hold by induction hypotheses (including Lemma 14).
• Cases V = EV-BU, V = EV-BUB, V = EV-IM-Eq, V = EV-IM-Neq and V =
EV-IM-Exc hold by induction hypotheses (including Lemma 16).

Lemma 14. If

VT
br
, there exists a type t such that v : t , and there exists
cs; v; σ ====⇒ vres; σ ′
td−visit

a type t′ such that v ′ : t′ for each value in the input store v ′ ∈ img σ, then
1. There exists a type t′′ such that v ′′ : t′′ for each value in the result store v ′′ ∈ img σ ′ .
2. If the result value vres is either success v ′′′ , return v ′′′ , or throw v ′′′ , then there exists a
type t′′′ such that v ′′′ : t′′′
39

Proof. By induction on the derivation VT:
• All cases (VT = ETV-Break-Sucs, VT = ETV-Ord-Sucs1, VT =
ETV-Ord-Sucs2, VT = ETV-Exc1 and VT = ETV-Exc2) hold by induction hypotheses (including Lemma 11 and Lemma 15), Lemma 5, Lemma 2 and Lemma 7.

Lemma 15. If

VTS
br
, there exists a type sequence t such that v : t , and
cs; v; σ =====⇒ vres⋆; σ ′
td−visit⋆

there exists a type t′ such that v ′ : t′ for each value in the input store v ′ ∈ img σ, then
1. There exists a type t′′ such that v ′′ : t′′ for each value in the result store v ′′ ∈ img σ ′ .
2. If the result value vres⋆ is success v ′′′ then there exists a type sequence t′′′ such that
v ′′′ : t′′′
3. If the result value vres⋆ is either return v ′′′ , or throw v ′′′ , then there exists a type t′′′
such that v ′′′ : t′′′
Proof. By induction on the derivation VTS
• Case VTS = ETVS-Emp holds using the premises.
• Cases VTS = ETVS-Break, VTS = ETVS-More, VTS = ETVS-Exc1 and
VTS = ETVS-Exc2 holds using the induction hypotheses (including Lemma 14) and
Lemma 6.

Lemma 16. If

VB
br
, there exists a type t such that v : t , and there
cs; v; σ ====⇒ vres; σ ′
bu−visit

exists a type t′ such that v ′ : t′ for each value in the input store v ′ ∈ img σ, then
1. There exists a type t′′ such that v ′′ : t′′ for each value in the result store v ′′ ∈ img σ ′ .
2. If the result value vres is either success v ′′′ , return v ′′′ , or throw v ′′′ , then there exists a
type t′′′ such that v ′′′ : t′′′
Proof. By induction on the derivation VB:
• All cases (VB = EBU-No-Break-Sucs, VB = EBU-Break-Sucs, VB =
EBU-Fail-Sucs, VB = EBU-No-Break-Exc, VB = EBU-Exc, and VB =
EBU-No-BreakErr) hold by induction hypotheses (including Lemma 11 and
Lemma 17), Lemma 5, Lemma 2 and Lemma 7.

Lemma 17. If

VBS
br
, there exists a type sequence t such that v : t , and
cs; v; σ =====⇒ vres⋆; σ ′
bu−visit⋆

there exists a type t′ such that v ′ : t′ for each value in the input store v ′ ∈ img σ, then
40

1. There exists a type t′′ such that v ′′ : t′′ for each value in the result store v ′′ ∈ img σ ′ .
2. If the result value vres⋆ is success v ′′′ then there exists a type sequence t′′′ such that
v ′′′ : t′′′
3. If the result value vres⋆ is either return v ′′′ , or throw v ′′′ , then there exists a type t′′′
such that v ′′′ : t′′′
Proof. By induction on the derivation VBS
• Case VBS = EBUS-Emp holds using the premises.
• Cases VBS = EBUS-Break, VBS = EBUS-More, VBS = EBUS-Exc1 and
VBS = EBUS-Exc2 holds using the induction hypotheses (including Lemma 16) and
Lemma 6.

Theorem 2 (Strong typing). Assume that semantic unary J⊖K and binary operators J⊕K
E
T
for each
are strongly typed. If e; σ ==⇒ vres; σ ′ and there exists a type t such that
v:t
expr
value in the input store v ∈ img σ, then
1. There exists a type t′ such that v ′ : t′ for each value in the result store v ′ ∈ img σ ′ .
2. If the result value vres is either success v ′′ , return v ′′ , or throw v ′′ , then there exists a
type t′′ such that v ′′ : t′′ .
Proof. By induction on the derivation E:
• Cases E = E-Val, E = E-Var-Sucs, E = E-Var-Err, E = E-Break, E =
E-Continue and E = E-Fail hold directly using the premises.
• Cases E = E-Un-Exc1, E = E-Bin-Exc1, E = E-Bin-Exc2, E = E-Cons-Err, E =
E-Cons-Exc, E = E-List-Err, E = E-List-Exc, E = E-Set-Err, E = E-Set-Exc,
E = E-Map-Err, E = E-Map-Exc, E = E-Lookup-Err, E = E-Lookup-Exc1,
E = E-Lookup-Exc2, E = E-Update-Err1, E = E-Update-Err2,
E = E-Update-Exc1, E = E-Update-Exc2, E = E-Update-Exc3, E =
E-Call-Arg-Err, E = E-Call-Arg-Exc, E = E-Ret-Sucs, E = E-Ret-Exc,
E = E-Asgn-Err, E = E-Asgn-Exc, E = E-If-True, E = E-If-False, E =
E-If-Err, E = E-If-Exc, E = E-Switch-Sucs, E = E-Switch-Exc1, E =
E-Switch-Exc2, E = E-Visit-Sucs, E = E-Visit-Fail, E = E-Visit-Exc1, and
E = E-Visit-Exc2, E = E-For-Sucs, E = E-For-Exc, E = E-While-True-Sucs,
E = E-While-Exc1, E = E-While-Exc2, E = E-While-Err, E = E-Solve-Eq,
E = E-Solve-Neq, E = E-Solve-Exc, E = E-Solve-Err, , E = E-Thr-Sucs,
E = E-Thr-Err, E = E-Fin-Sucs, E = E-Fin-Exc, and E = E-Try-Ord hold by
induction hypotheses (including Lemma 8, Lemma 10, Lemma 12 and Lemma 13).
• Case E = E-Un-Sucs holds by its induction hypothesis and strong typing of J⊖K.
41

• Case E = E-Bin-Sucs holds by its induction hypothesis and strong typing of J⊕K.
• Case E = E-Cons-Sucs holds by its induction hypothesis given by Lemma 8, and
then by using T-Constructor with the provided typing premises.
• Case E = E-List-Sucs holds by its induction hypothesis given by Lemma 8, and then
by using T-List.
• Case E = E-Set-Sucs holds by its induction hypothesis given by Lemma 8, and then
by using T-Set.
• Case E = E-Map-Sucs holds by its induction hypothesis given by Lemma 8, and then
by using T-Map.
• Case E = E-Lookup-Sucs holds by its induction hypotheses and inversion of T to
T-Map.
• Case E = E-Lookup-NoKey holds by its induction hypotheses and using T-Cons
on the deﬁnition of NoKey.
• Case E = E-Update-Sucs holds by its induction hypotheses and by using T-Map to
reconstruct the type derivation for the result.
• Cases E = E-Call-Sucs, E = E-Call-Res-Exc, E = E-Call-Res-Err1, and
E = E-Call-Res-Err2 hold by induction hypotheses (including Lemma 8) and by
using the fact that extracting variables from and extending well-typed stores produces
well-typed stores.
• Cases E = E-Asgn-Sucs and E = E-Try-Catch hold by induction hypotheses and
the fact that extending well-typed stores with well-typed environments preserves welltypedness.
• Cases E = E-Switch-Fail, E = E-While-False, and E = E-While-True-Break
hold by induction hypotheses and using T-Void.
• Cases E = E-Block-Sucs, E = E-Block-Exc hold by the induction hypothesis given
by Lemma 8 and the fact that removing variables from a well-typed store produces a
well-typed store.

We will for Theorem 3, also need to state some lemmas. We will for the proof focus mainly
on cases where the induction hypothesis does not timeout, since if it does it is trivially possible
to construct a timeout derivation for the result syntax.
First, we need a lemma that speciﬁes that the sequence of values produced by the children
is strictly smaller than the input value. Let v ≺ v ′ denote the relation that v is syntactically
contained in v ′ , then our target property is speciﬁed in Lemma 18.
Lemma 18. If v ′ = children(v) then vi′ ≺ v for all i.
42

Proof. Directly by induction on v.
We have a lemma for progress on reconstruction:
Lemma 19. It is possible to construct a derivation recons v using v ′ to rcres for any
well-typed value v and well-typed value sequence v ′ .
Proof. Straightforwardly by case analysis on v.
We have two mutually recursive lemmas for pattern matching: Lemma 20 and Lemma 21.
?

Lemma 20. It is possible to construct a derivation σ ⊢ p := v ===⇒ ρ for any pattern p,
match
well-typed value v, well-typed store σ.
Proof. By induction on syntax of p:
• Case p = vb: We proceed by testing whether v is equal to vb:
– Case v = vb then use P-Val-Sucs.
– Case v 6= vb then use P-Val-Fail.
• Case p = x: We proceed by testing whether x is in dom σ
– Case x ∈ dom σ: we proceed to test whether v is equal to σ(x)
* Case v = σ(x) then use P-Var-Uni.
* Case v 6= σ(x) then use P-Var-Fail.
– Case x ∈
/ dom σ then use P-Var-Bind.
• Case p = k(p′ ): We proceed to test whether v is equal to k(v ′ ) for some v ′
– Case v = k(v ′ ) then use P-Cons-Sucs using the induction hypotheses of p′ with
v′.
– Case v 6= k(v ′ ) then use P-Cons-Fail.
• Case p = t x : p′ : From our premise we know that v is well-typed, i.e. that there exists
a t′ such that v : t′ . We proceed to test whether t′ <: t.
– Case t′ <: t then use P-Type-Sucs using the induction hypothesis on p′ with v.
– Case t′ 6<: t then use P-Type-Fail.
• Case p = [⋆p′ ]:
We proceed to test whether v = [v ′ ] for some value sequence v ′ .
– Case v = [v ′ ] then use P-List-Sucs induction hypothesis given by Lemma 21 on
⋆p′ with v ′
– Case v 6= [v ′ ] then use P-List-Fail
43

• Case p = {⋆p′ }:
We proceed to test whether v = {v ′ } for some value sequence v ′ .
– Case v = {v ′ } then use P-Set-Sucs induction hypothesis given by Lemma 21 on
⋆p′ with v ′
– Case v 6= {v ′ } then use P-Set-Fail
• Case p = /p′ :
?

– Using the induction hypothesis on p′ with v, we get σ ⊢ p′ := v ===⇒ ρ.
match

′

– Now, let v = children(v). In order to handle the self-recursive calls using /p′ , we
proceed by inner well-founded induction on the relation ≺ using value sequence
v′:
?

* Using the inner induction hypothesis we get derivations σ ⊢ /p′ := vi′ ===⇒ ρi
match
for all i
– Finally, we use P-Deep on the derivations we got from the outer and inner induction hypotheses.

?

hi

⊗

Lemma 21. It is possible to construct a derivation σ ⊢ ⋆p := v | V ====⇒ ρ for any pattern p,
match⋆
well-typed value v, well-typed store σ, well-typed visited value set V, type-preserving partition
operator ⊗.
Proof. By induction on the syntax of ⋆p:
• Case ⋆p = ε
By case analysis on v:
– Case v = ε then use PL-Emp-Both
– Case v = v ′ , v ′′ then use PL-Emp-Pat
• Case ⋆p = p′ , ⋆p′′ :
Because of backtracking we need to do an innerninduction to handle
o the cases which
′
′′
′
′′
recurse to the same pattern sequence. Let Vall = v ∃v .v = v ⊗ v , then we proceed
by inner induction on |Vall | − |V|:
– Case |Vall | − |V| = 0 then we have |Vall | = |V| and thus we have to use
PL-More-Pat-Exh.
– Case |Vall | − |V| > 0: Then there exists a V′ 6= ∅ such that Vall = V′ ⊎ V,
and we can pick a v ′ ∈ V′ such that v = v ′ ⊗ v ′′ for some v ′ . We can ﬁnally
use PL-More-Pat-Re using Lemma 20 with p, v ′ and σ, the outer induction
hypothesis with ⋆p′′ , v ′′ and σ, and the inner induction hypothesis on V ∪ {v ′ }
44

• Case ⋆p = ⋆x, ⋆p′′ :
We proceed to test whether x is in dom σ
– Case x ∈ dom σ: By case analysis on σ(x) = v ′ :
* Case v ′ = hv ′′ i:
By checking whether there exists v ′′′ such that v = v ′′ ⊗ v ′′′
· Case ∃v ′′′ .v = v ′′ ⊗ v ′′′ then use PL-More-Star-Uni with induction
hypothesis applied to ⋆p′′ and v ′′′ .
· Case ∄v ′′′ .v = v ′′ ⊗ v ′′′ : then use rule PL-More-Star-Pat-Fail.
* Case v ′ 6= hv ′′ i: then use PL-More-Star-Val-Fail.
– Case x ∈
/ dom σ:
Similarly to the ordinary pattern case, we need to do an inner induction to
handle the cases which
recurse to the same star pattern sequence. Let Vall =
n
o
′
′
′′
′′
v ∃v .v = v ⊗ v , then we proceed by inner induction on |Vall | − |V|

* Case |Vall | − |V| = 0:
Then we have V = Vall and so the only applicable rule is
PL-More-Star-Exh since Vall covers all partitions and thus ∄v ′ , v ′′ .v =
v ′ ⊗ v ′′ ∧ v ′ ∈
/ V holds.
* Case |Vall | − |V| > 0:
Then there exists V′ 6= ∅ such that Vall = V′ ⊎ V and we can pick v ′ ∈ V′
such that v = v ′ ⊗ v ′′ for some v ′′ .
We can now use PL-More-Star-Re by using the outer hypothesis on ⋆p
with v ′′ and ∅, and the inner hypothesis on V ∪ {v ′ } (since the size decreases
by 1)

We now have a series of lemmas that are mutually recursive with Theorem 3: Lemma 22,
Lemma 23, Lemma 24, Lemma 25, Lemma 26, Lemma 27, Lemma 28, Lemma 29, Lemma 30,
and Lemma 31.
Lemma 22. It is possible to construct a derivation e; σ ===⇒n vres⋆; σ ′ , for any expression
expr⋆

sequence e, well-typed store σ and fuel n.
Proof. By induction on n:
• Case n = 0 then use corresponding timeout-rule.
• Case n > 0, then by case analysis on the expression sequence e:
– Case e = ε then use ES-Emp.
– Case e = e′ , e′′ :

45

* Using induction hypothesis given by Theorem 3 on n − 1 with e′ and σ we
get a derivation e′ ; σ ==⇒n−1 vres ′ ; σ ′′
expr

By case analysis on vres ′ :
· Case vres ′ = success v ′ :
By Theorem 2 we get that σ ′′ is well-typed.
By induction hypothesis on n − 1 with e′′ and σ ′′ we get a derivation
e′′ ; σ ′′ ===⇒n−1 vres⋆′′ ; σ ′
expr⋆

By case analysis on vres⋆′′ :
• Case vres⋆′′ = success v ′′ then use ES-More
• Case vres⋆′′ = exres then use ES-Exc2
· Case vres ′ = exres then use ES-Exc1

Lemma 23. It is possible to construct a derivation e; ρ; σ ==⇒n vres; σ ′ for any expression
each

e, well-typed environment sequence ρ, well-typed store σ and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
By case analysis on the environment sequence ρ:
– Case ρ = ε then use EE-Emp
– Case ρ = ρ′ , ρ′′ :
By induction hypothesis given by Theorem 3 on n − 1 with e and σρ we get a
derivation e; σρ ==⇒n−1 vres ′ ; σ ′′ .
expr

By case analysis on vres ′ :
* Cases vres ′ = success v ′ and vres ′ = continue then use EE-More-Sucs
with above derivation and the induction hypothesis on n − 1 with ρ′′ , e, and
σ ′′′ = σ ′′ \ dom ρ′ .
* Cases vres ′ = break then use EE-More-Break
* Cases vres ′ = throw v ′ , vres ′ = return v ′ , vres ′ = fail, and vres ′ = error then
use EE-More-Exc

Lemma 24. It is possible to construct a derivation g; σ ===⇒n envres; σ ′ for any generator
gexpr

expression g, well-typed store σ and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
46

• Case n > 0:
By case analysis on g:
– Case g = p := e:
By induction hypothesis given by Theorem 3 on n − 1 with e and σ we get a
derivation e; σ ==⇒n−1 vres ′ ; σ ′
expr

By case analysis on vres ′ :
* Case vres ′ = success v ′ then use G-Pat-Sucs with above derivation and the
derivation from applying Lemma 20 on p with σ ′ and v ′ .
* Case vres ′ = exres then use G-Pat-Exc:
– Case g = x ← e:
By induction hypothesis given by Theorem 3 on n − 1 with e and σ we get a
derivation e; σ ==⇒n−1 vres ′ ; σ ′
expr

By case analysis on vres ′
* Case vres ′ = success v ′
By case analysis on v ′ :
· Case v ′ = [v ′′ ] then use G − Enum − List
· Case v ′ = {v ′′} then use G − Enum − Set
· Case v ′ = (v ′′ : v ′′′ ) then use G − Enum − Map
· Cases v ′ = vb, v ′ = k(v ′′ ) and v ′ =  then use G-Enum-Err
* Case vres ′ = exres then use G-Enum-Exc

Lemma 25. It is possible to construct a derivation ρ; e; σ ==⇒n vres; σ ′ for any well-typed
case

environment sequence ρ, expression e, well-typed store σ and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
By case analysis on the environment sequence ρ
– Case ρ = 0 then use EC-Emp.
– Case ρ = ρ′ , ρ′′ :
Using the induction hypothesis given by Theorem 3 on n − 1 with e and σ we get
a derivation e; σ ==⇒n−1 vres ′ ; σ ′ .
expr

By case analysis on vres ′
* Case vres ′ = fail then use EC-More-Fail on above derivation and the derivation from applying the induction hypothesis on n − 1 with ρ′′ , e and σ.
47

* Case vres ′ 6= fail then use EC-More-Ord.

Lemma 26. It is possible to construct a derivation cs; v; σ ==⇒n vres; σ ′ for any case secases

quence cs, well-typed value v, well-typed store σ and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
By case analysis on the case sequence cs
– Case cs = ε then use ECS-Emp
– Case cs = case p ⇒ e, cs ′ :
?

Using Lemma 20 on p with v and σ gives us a derivation σ ⊢ p := v ===⇒ ρ. By
match

Lemma 3 we know that ρ is well-typed.
Using induction hypothesis given by Lemma 25 on n − 1 with ρ, e and σ we get
a derivation ρ; e; σ ==⇒n−1 vres ′ ; σ ′ .
case

By case analysis on vres ′ :
* Case vres ′ = fail then use ECS-More-Fail using above derivation and the
derivation given by the induction hypothesis on n − 1 with cs ′ , v and σ.
* Case vres ′ 6= fail then use ECS-More-Ord

st n

Lemma 27. It is possible to construct a derivation cs; v; σ ==⇒ vres; σ ′ for any case sevisit

quence cs, well-typed value v, well-typed store σ, traversal strategy st and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
By case analysis on syntax of st
– Case st = top-down then use EV-TD with the derivation from the induction
hypothesis given by Lemma 28 on n − 1 with cs, v, σ and no-break.
– Case st = top-down-break then use EV-TDB with the derivation from the induction hypothesis given by Lemma 28 on n − 1 with cs, v, σ and break.
– Case st = bottom-up then use EV-BU with the derivation from the induction
hypothesis given by Lemma 30 on n − 1 with cs, v, σ and no-break.

48

– Case st = bottom-up-break then use EV-BUB with the derivation from the induction hypothesis given by Lemma 30 on n − 1 with cs, v, σ and break.
– Case st = outermost:
Using the induction hypothesis by Lemma 28 on n − 1 with cs, v, σ and no-break
no-break n−1

we get a derivation cs; v; σ ====⇒
td−visit

vres ′ ; σ ′′ . We know the well-typedness of

the output components from Lemma 14.
By case analysis on vres ′ :
* Case vres ′ = success v ′ :
We proceed by checking whether v = v ′ :
· Case v = v ′ then use EV-OM-Eq using above derivation.
· Case v 6= v ′ then use EV-OM-Neq using above derivation and the derivation from the induction hypothesis given by Lemma 28 on n − 1 with cs,
v ′ , σ ′′ and no-break.
* Case vres ′ = exres then use EV-OM-Exc using above derivation.
– Case st = innermost: Using the induction hypothesis by Lemma 30 on n − 1 with
no-break n−1

cs, v, σ and no-break we get a derivation cs; v; σ ====⇒
bu−visit

vres ′ ; σ ′′ . We know

the well-typedness of the output components from Lemma 16.
By case analysis on vres ′ :
* Case vres ′ = success v ′ :
We proceed by checking whether v = v ′ :
· Case v = v ′ then use EV-IM-Eq using above derivation.
· Case v 6= v ′ then use EV-IM-Neq using above derivation and the derivation from the induction hypothesis given by Lemma 30 on n − 1 with cs,
v ′ , σ ′′ and no-break.
* Case vres ′ = exres then use EV-IM-Exc using above derivation.

br

n

Lemma 28. It is possible to construct a derivation cs; v; σ ====⇒ vres; σ ′ for any cs,
td−visit

well-typed value v, well-typed store σ, breaking strategy br and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
Applying the induction hypothesis given by Lemma 26 on n − 1 with cs, v and sigma
CS
we get a derivation cs; v; σ ==⇒n−1 vres ′ ; σ ′′
cases

We proceed to check whether vres ′ has syntax vfres ′ for some vfres ′ :
49

– Case vres ′ = vfres ′ :
We proceed to check whether vfres ′ = success v ′ and br = break
* Case vfres ′ = success v ′ and br = break then use ETV-Break-Sucs with
CS.
* Case vfres ′ 6= success v ′ or br 6= break:
By Boolean logic, we have that br 6= break ⇒ vfres ′ = fail is satisﬁed.
Let v ′′ = if-fail(vfres, v) and v ′′′ = children(v ′′ ) (all well-typed from Lemma 5
and Lemma 2).
By induction hypothesis given by Lemma 15 on n − 1 with cs, v ′′′ and σ ′′ , we
CS ′
n−1
.
get a derivation
br
vres ′′ ; σ ′
cs; v ′′′ ; σ ′′ =====⇒
td−visit⋆

We know that the results are well typed from Lemma 15.
By case analysis on vres ′′ :
· Case vfres ′′ = success v ′′′′ then use ETV-Ord-Sucs2 with CS, CS ′ and
the result derivation from applying Lemma 19.
· Case vfres ′′ = fail then use ETV-Ord-Sucs1 with CS, CS ′ .
· Case vfres ′′ = exres where exres 6= fail then use ETV-Exc2 with CS,
CS ′ .
– Case vres ′ 6= vfres ′ : Necessarily, we then have that vres ′ = exres where exres 6= fail
and so we use ETV-Exc1 with CS.

br

n

Lemma 29. It is possible to construct a derivation cs; v; σ =====⇒ vres⋆; σ ′ for any cs,
td−visit⋆

well-typed value sequence v, well-typed store σ, breaking strategy br and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0: By case analysis on v:
– Case v = ε then use ETVS-Emp.
– Case v = v ′ , v ′′ :
By induction hypothesis given by Lemma 28 on n − 1 with cs, v and σ we get a
VT
n−1
.
derivation
br
vres ′′ ; σ ′′
cs; v; σ ====⇒
td−visit

We proceed by checking whether vres ′′ is syntactically a vfres ′′ for some vfres ′′ :
* Case vres ′′ = vfres ′′ :
We proceed by checking whether vfres ′′ = success v ′′′ and br = break:
· Case vfres ′′ = success v ′′′ and br = break then use ETVS-Break with
VT.
50

· Case vfres ′′ 6= success v ′′′ or br 6= break:
By Boolean logic, we have that br 6= break ⇒ vfres ′′ = fail is satisﬁed.
By induction hypothesis on n − 1 with cs, v ′′ and σ ′′ we get a derivation
VTS
n−1
.
br
vres⋆′′′ ; σ ′
cs; v ′′ ; σ ′′ =====⇒
td−visit⋆

By case analysis on vres⋆′′′ :
• Case vres⋆′′′ = vfres⋆′′′ then use ETVS-More with VT and VTS.
• Case vres⋆′′′ = exres where exres 6= fail then use ETVS-Exc2 with VT
and VTS.
* Case vres ′′ 6= vfres ′′ :
Here we then have that vres ′′ = exres, where exres 6= fail and so we use
ETVS-Exc1.

br

n

Lemma 30. It is possible to construct a derivation cs; v; σ ====⇒ vres; σ ′ for any cs,
bu−visit

well-typed value v, well-typed store σ, breaking strategy br and fuel n.
Proof. By case analysis on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
Let v ′′ = children(v). We know that v ′′ is well-typed from Lemma 2.
By induction hypothesis given by Lemma 31 on n − 1 with cs, v ′′ and σ we get a
VBS
n−1
derivation
. Recall that the output is well-typed from
br
cs; v ′′ ; σ =====⇒
vres ′′ ; σ ′′
bu−visit⋆

Lemma 17.
By case analysis on vres⋆′′ :
– Case vres⋆′′ = vfres ′′ :
We proceed by case analysis on vfres ′′
* Case vfres ′′ = success v ′′′ : We proceed by case analysis on br :
· Case br = break then use EBU-Break-Sucs with VBS and the derivation from applying Lemma 19 on v and v ′′′ .
· Case br = no-break:
By applying Lemma 19 on v and v ′′′ we get a derivation
RC
.
recons v using v ′′′ to rcres
By case analysis on rcres:

51

• Case rcres = success v ′ :
By induction hypothesis given by Lemma 26 on n − 1 with cs, v ′ and
CS
σ ′′ we get a derivation cs; v ′ ; σ ′′ ==⇒n−1 vres ′ ; σ ′
cases

By case analysis on vres ′ :
– Case vres ′ = vfres ′ then use EBU-No-Break-Sucs with VBS, RC
and CS .
– Case exres then use EBU-No-Break-Exc with VBS, RC and CS .
• Case rcres = error then use EBU-No-Break-Err.
* Case vfres ′′ = fail then use EBU-Fail-Sucs with the induction hypothesis
given by Lemma 26 on n − 1 with cs, v and σ ′′ .
– Case vres⋆′′ = exres where exres 6= fail then use EBU-Exc with VBS.

br

n

Lemma 31. It is possible to construct a derivation cs; v; σ =====⇒ vres⋆; σ ′ for any cs,
bu−visit⋆

well-typed value sequence v, well-typed store σ, breaking strategy br and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
By case analysis on v:
– Case v = ε then use EBUS-Emp.
– Case v = v ′ , v ′′ : By induction hypothesis given by Lemma 30 on n − 1 with cs, v ′
VB
n−1
and σ we get a derivation
.
br
cs; v ′ ; σ ====⇒
vres ′′ ; σ ′′
bu−visit

′′

By case analysis on vres :
* Case vres ′′ = vfres ′′ :
By case analysis on vfres ′′ and br :
· Case vfres ′′ = success v ′′′ and br = break: then use EBUS-Break with
VB.
· Case vfres ′′ 6= success v ′′′ or br 6= break:
By Boolean logic we have br = break ⇒ vfres = fail.
By induction hypothesis on n − 1 with cs, v ′′ and σ we get a derivation
VBS
n−1
.
br
vres⋆′ ; σ ′
cs; v ′′ ; σ ′′ =====⇒
bu−visit⋆

By case analysis on vres⋆′ :
• Case vres⋆′ = vfres⋆′ then use EBUS-More with VB and VBS
• Case vres⋆′ = exres then use EBUS-Exc2 with VB and VBS
52

* Case vres ′′ = exres then use EBUS-Exc1 with VB.
Theorem 3 (Partial progress). It is possible to construct a derivation e; σ ==⇒n vtres; σ ′ for
expr

any input expression e, well-typed store σ and fuel n.
Proof. By induction on n:
• Case n = 0 then use the corresponding timeout-derivation.
• Case n > 0:
By case analysis on syntax e:
– Case e = vb then use T-Basic.
– Case e = x
We proceed by checking x ∈ dom σ:
* Case x ∈ dom σ then use E-Var-Sucs.
* Case x ∈
/ dom σ then use E-Var-Err.
– Case e = ⊖ e′ :
By induction hypothesis on n − 1 with e′ and σ we get a derivation e′ ; σ ==⇒n−1
expr

′

′

vres ; σ .
By case analysis on vres ′ :
* Case vres ′ = successv then use E-Un-Sucs with above derivation.
* Case vres ′ = exres then use E-Un-Exc with above derivation.
– Case e = e1 ⊕ e2 : By induction hypothesis on n − 1 with e1 and σ we get a
E1
derivation e ; σ ==⇒n−1 vres ; σ ′′ .
1
1
expr

By case analysis on vres 1 :
* Case vres 1 = success v1 : By induction hypothesis on n − 1 with e2 and σ ′′ we
E2
get a derivation e ; σ ′′ ==⇒n−1 vres ; σ ′ .
2
2
expr

By case analysis on vres 2 :
· Case vres 2 = success v2 then use E-Bin-Sucs with E1 and E2 .
· Case vres 2 = exres then use E-Bin-Exc2 with E1 and E2 .
* Case vres 1 = exres then use E-Bin-Exc1 with E1.
– Case e = k(e′ ):
Recall that all derivations in our paper are assumed to be well-scoped so there
must exist a corresponding data-type at that has k(t) as a constructor.
By using induction hypothesis given by Lemma 22 on n − 1 with e′ and σ we get
ES
a derivation e′ ; σ ===⇒n−1 vres⋆′ ; σ ′ .
expr⋆

By case analysis on vres⋆′ :
53

* Case vres⋆′ = success v ′ :
By Lemma 8 we know that v ′ is well-typed, i.e. that we have v ′ : t′ for some
type sequence t′ . We proceed to check whether all values in the sequence are
non- and each have a type t′i that is a subtype of the target type ti .
· Case v 6=  and t′ <: t then use E-Cons-Sucs with ES and the required
typing derivations.
· Case vi =  or t′i <: ti for some i then use E-Cons-Err with ES.
* Case vres⋆′ = exres then use E-Cons-Exc with ES
– Case e = [e′ ]:
By induction hypothesis given by Lemma 22 on n − 1 with e′ and σ we get a
derivation e′ ; σ ===⇒n−1 vres⋆′ ; σ ′ .
expr⋆

By case analysis on vres⋆′ :
* Case vres⋆′ = success v:
We proceed by checking whether all values v are non-:
· Case v 6=  then use E-List-Sucs with above derivation.
· Case vi 6=  for some i then use E-List-Err with above derivation.
* Case vres⋆′ = exres then use E-List-Exc with above derivation.
– Case e = {e′ }
By induction hypothesis given by Lemma 22 on n − 1 with e′ and σ we get a
derivation e′ ; σ ===⇒n−1 vres⋆′ ; σ ′ .
expr⋆

By case analysis on vres⋆′ :
* Case vres⋆′ = success v:
We proceed by checking whether all values v are non-:
· Case v 6=  then use E-Set-Sucs with above derivation.
· Case vi 6=  for some i then use E-Set-Err with above derivation.
* Case vres⋆′ = exres then use E-Set-Exc with above derivation.
– Case e = (e′ : e′′ )
By induction hypothesis given by Lemma 22 on n − 1 with e′ , e′′ and σ we get a
derivation e′ , e′′ ; σ ===⇒n−1 vres⋆′ ; σ ′ .
expr⋆

By case analysis on vres⋆′ :
* Case vres⋆′ = success v, v ′ :
We proceed by checking whether all values v and v ′ are non-:
· Case v 6=  and v ′ 6=  then use E-Map-Sucs with above derivation.
· Case vi 6=  or vi′ 6=  for some i then use E-Map-Err with above
derivation.
* Case vres⋆′ = exres then use E-Map-Exc with above derivation.
– Case e = e1 [e2 ]

54

By induction hypothesis on n − 1 with e1 and σ we get a derivation
E
e1 ; σ ==⇒n−1 vres 1 ; σ ′′ .
expr

By case analysis on vres 1 :
* Case vres 1 = success v1 :
By case analysis on v1 :
· Case v1 = (v ′ : v ′′ ):
By induction hypothesis on n − 1 with e2 and σ ′′ we get a derivation
E′
′′
e2 ; σ ==⇒n−1 vres 2 ; σ ′ .
expr

By case analysis on vres 2 :
• Case vres 2 = success v2 :
We proceed to check whether ∃i.vi′ = v2 :
– Case vi′ = v2 then use E-Lookup-Sucs with E and E ′ .
– Case ∄i.vi′ = v2 then use E-Lookup-NoKey with E and E ′ .
• Case vres 2 = exres then use E-Lookup-Exc2 with E and E ′ .
· Case v1 6= (v ′ : v ′′ ) then use E-Lookup-Err with E.
* Case vres 1 = exres then use E-Lookup-Exc1 with E.
– Case e = e1 [e2 = e3 ]
By induction hypothesis on n − 1 with e1 and σ we get a derivation
E
n−1
e1 ; σ ==⇒
vres 1 ; σ ′′′ .
expr

By case analysis on vres 1 :
* Case vres 1 = success v1
By case analysis on v1 :
· Case v1 = (v ′ : v ′′ ):
By induction hypothesis on n − 1 with e2 and σ ′′′ we get a derivation
E′
e2 ; σ ′′′ ==⇒n−1 vres 2 ; σ ′′ .
expr

By case analysis on vres 2 :
• Case vres 2 = success v2 :
By induction hypothesis on n − 1 with e3 and σ ′′ we get a derivation
E ′′
e3 ; σ ′′ ==⇒n−1 vres 3 ; σ ′ .
expr

By case analysis on vres 3 :
– Case vres 3 = success v3 :
We proceed to check whether v2 and v3 are non-:
* Case v2 6=  and v3 6=  then use E-Update-Sucs with E, E ′ and
E ′′ .
* Case v2 =  or v3 =  then use E-Update-Err2 with E, E ′ and
E ′′ .
55

– Case vres 3 = exres then use E-Update-Exc3 with E and E ′ .
• Case vres 2 = exres then use E-Update-Exc2 on E and E ′ .
· Case v1 6= (v ′ : v ′′ ) then use E-Update-Err1 with E.
* Case vres 1 = exres then use E-Update-Exc1 with E.
– Case e = f (e′ )
By induction hypothesis given by Lemma 22 on n − 1 with e′ and σ we get a
ES
derivation e′ ; σ ===⇒n−1 vres⋆′′ ; σ ′′
expr⋆

By case analysis on vres⋆′′ :
* Case vres⋆′′ = success v ′′
Recall that we assume that our function calls are well-scoped and so there
must exist a corresponding function deﬁnition fun t′ f (t x) = e′′ . By Lemma 8
we know that we have v ′′ : t′′ for some type sequence t′′ .
We proceed to check whether t′′ <: t:
· Case t′′ <: t
Let global ty y represent all global variable deﬁnitions.
By induction hypothesis on n − 1 with e′′ and [y 7→ σ ′′ (y), x 7→ v ′′ ] we get
E
a derivation e′ ; [y 7→ σ ′′ (y), x 7→ v ′′ ] ==⇒n−1 vres ′ ; σ ′′′ .
expr

By case analysis on vres ′ :
• Case vres ′ = success v ′ or vres ′ = return v ′ .
By Theorem 2 we know that v ′ : t′′′ for some type t′′′ . We proceed to
check whether t′′′ <: t′ :
– Case t′′′ <: t′ then use E-Call-Res-Sucs with ES and E.
– Case t′′′ 6<: t′ then use E-Call-Res-Err1 with ES and E.
• Case vres ′ = throw v ′ then use E-Call-Res-Exc with ES and E
• Case vres ′ ∈ {break, continue, fail, error} then use E-Call-Res-Err2
with ES and E.
· Case t′′i 6<: ti for some i then use E-Call-Arg-Err with ES.
* Case vres⋆′′ = exres then use E-Call-Arg-Exc with ES.
– Case e = return e′
By induction hypothesis on n − 1 with e′ and σ we get a derivation e′ ; σ ==⇒n−1
expr

vres ′ ; σ ′ .
* Case vres ′ = success v then use E-Ret-Sucs with above derivation.
* Case vres ′ = exres then use E-Ret-Exc with above derivation.
– Case e = (x = e′ )
Recall that our deﬁnitions are assumed to be well-scoped and so there must exists
either a local t x or global t x declaration for the variable (with no overshadowing).

56

By induction hypothesis on n − 1 with e′ and σ we get a derivation e′ ; σ ==⇒n−1
expr

vres ′ ; σ ′′ .
By case analysis on vres ′ :
* Case vres ′ = success v: By Theorem 2 we know that there exists a t′ such
that v : t′ .
We proceed by checking whether t′ <: t:
· Case t′ <: t then use E-Asgn-Sucs with above evaluation and typing
derivations.
· Case t′ 6<: t then use E-Asgn-Err with above evaluation and typing
derivations.
* Case vres ′ = exres then use E-Asgn-Exc with above derivation.
– Case e = if e1 then e2 else e3
By induction hypothesis on n − 1 with e1 and σ we get a derivation
E
n−1
e1 ; σ ==⇒
vres ′′ ; σ ′′ .
expr

By case analysis on vres ′′ :
* Case vres ′′ = success v ′′
By case analysis on v ′′ :
· Case v ′′ = false() then use E-If-False with E and the derivation from
the induction hypothesis on n − 1 with e2 and σ ′′ .
· Case v ′′ = true() then use E-If-True with E and the derivation from the
induction hypothesis on n − 1 with e3 and σ ′′ .
· Case v ′′ 6= true() and v ′′ 6= false() then use E-If-Err with E.
* Case vres ′′ = exres then use E-If-Exc with E.
– Case e = switch e′ do cs
By induction hypothesis on n − 1 with e′ and σ we get a derivation
E
′
n−1
e ; σ ==⇒
vres ′′ ; σ ′′ .
expr

By case analysis on vres ′′ :
* Case vres ′′ = success v ′′
By induction hypothesis given by Lemma 26 on n − 1 with cs, v ′′ and σ ′′ we
CS
get a derivation cs; v ′′ ; σ ′′ ==⇒n−1 vres ′ ; σ ′ .
cases

case analysis on vres ′ :
Case vres ′ = success v ′ then use E-Switch-Sucs with E and CS.
Case vres ′ = fail then use E-Switch-Fail with E and CS.
Case vres ′ = exres where exres 6= fail then use E-Switch-Exc2 with E
and CS.
* Case vres ′′ = exres then use E-Switch-Exc1 with E.
By
·
·
·

57

– Case e = st visit e′ do cs:
By induction hypothesis on n − 1 with e′ and σ we get a derivation
E
′
n−1
e ; σ ==⇒
vres ′′ ; σ ′′ .
expr

By case analysis on vres ′′ :
* Case vres ′′ = success v ′′
By induction hypothesis given by Lemma 27 on n − 1 with cs, v ′′ and σ ′′ we
V
n−1
get a derivation
.
st
cs; v ′′ ; σ ′′ ==⇒
vres ′ ; σ ′
visit

case analysis on vres ′ :
Case vres ′ = success v ′ then use E-Visit-Sucs with E and V.
Case vres ′ = fail then use E-Visit-Fail with E and V.
Case vres ′ = exres where exres 6= fail then use E-Visit-Exc2 with E and
V.
* Case vres ′′ = exres then use E-Visit-Exc1 with E.
By
·
·
·

– Case e = break then use E-Break.
– Case e = continue then use E-Continue.
– Case e = fail then use E-Fail.
– Case e = local t x in e′ end then use either E-Block-Sucs (when it produces a
successful result) or E-Block-Exc (otherwise) with the derivation of the induction hypothesis given by Lemma 22 on n − 1 with e′ and σ.
– Case e = for g e′ :
By induction hypothesis given by Lemma 24 on n − 1 with g and σ we get a
derivation g; σ ===⇒n−1 envres; σ ′′ .
gexpr

By case analysis on envres:
* Case envres = success ρ then use E-For-Sucs with above derivation and the
derivation from the induction hypothesis given by Lemma 23 on n − 1 with
e′ , ρ and σ ′′ .
* Case envres = exres then use E-For-Exc with above derivation.
– Case e = while e1 e2
By induction hypothesis on n − 1 with e1 and σ we get a derivation:
E
n−1
e1 ; σ ==⇒
vres ′′ ; σ ′′ .
expr

By case analysis on vres ′′ :
* Case vres ′′ = success v ′′
By case analysis on v ′′ :
· Case v ′′ = false() then use E-While-False with E.

58

· Case v ′′ = true():
By induction hypothesis on n − 1 with e2 and σ ′′ we get a derivation
E′
e2 ; σ ′′ ==⇒n−1 vres ′′′ ; σ ′′′ .
expr

By case analysis on vres ′′′ :
• Case vres ′′′ = success v ′′′ or vres ′′′ = continue then use
E-While-True-Sucs with E, E ′ and the derivation from the induction hypothesis on n − 1 with while e1 e2 and σ ′′′ .
• Case vres ′′′ = break then use E-While-True-Break with E and E ′ .
• Case vres ′′′ = exres ∈ {throw v ′′′ , return v ′′′ , fail, error} then use
E-While-Exc2 with E and E ′ .
· Case v ′′ 6= true() and v ′′ 6= false() then use E-While-Err
* Case vres ′′ = exres then use E-While-Exc1 with E.
– Case e = solve x e′ :
By induction hypothesis on n − 1 with e′ and σ we get a derivation
E
′
n−1
e ; σ ==⇒
vres ′′ ; σ ′′ .
expr

By case analysis on vres ′′
* Case vres ′′ = success v ′′ :
We proceed by checking whether the variable sequence x is both in old and
new stores.
· Case x ⊆ dom σ ∩ dom σ ′′ :
We then check whether any value in x has changed:
• Case σ(x) = σ ′′ (x) then use E-Solve-Eq with E.
• Case σ(xi ) 6= σ ′′ (xi ) for some i then use E-Solve-Neq with E and the
derivation from the induction hypothesis on n − 1 with solve x e′ and
σ ′′ .
· Case xi ∈
/ dom σ ∩ dom σ ′′ for some i then use E-Solve-Err with E.
* Case vres ′′ = exres then use E-Solve-Exc with E.
– Case e = throw e′ :
By induction hypothesis on n − 1 with e′ and σ we get a derivation e′ ; σ ==⇒n−1
expr

vres ′ ; σ ′ .
* Case vres ′ = success v then use E-Thr-Sucs with above derivation.
* Case vres ′ = exres then use E-Thr-Exc with above derivation.
– Case e = try e1 catch x ⇒ e2 :
By induction hypothesis on n − 1 with e1 and σ we get a derivation
E
n−1
e1 ; σ ==⇒
vres 1 ; σ ′′ .
expr

By case analysis on vres 1 :
59

* Case vres 1 = throw v1 then use E-Try-Catch with E and the derivation
from the induction hypothesis on n − 1 with e2 and σ ′′ [x 7→ v1 ].
* Case vres 1 6= throw v1 then use E-Try-Ord with E.
– Case e = try e1 finally e2
By induction hypothesis on n − 1 with e1 and σ we get a derivation
E
e1 ; σ ==⇒n−1 vres 1 ; σ ′′ .
expr

By induction hypothesis on n − 1 with e2 and σ ′′ we get a derivation
E′
e2 ; σ ′′ ==⇒n−1 vres 2 ; σ ′ .
expr

By case analysis on vres 2 :
* Case vres 2 = success v2 then use E-Fin-Sucs with E and E ′
* Case vres 2 = exres then use E-Fin-Exc with E and E ′.

Theorem 4 (Terminating expressions). There exists n such that derivation
E
efin ; σ ==⇒n vres; σ ′ has a result vres which is not timeout for expression efin in the
expr

terminating subset.
Proof. The proof proceeds similarly to Theorem 3, except that instead of doing the induction
on n—which we know need to provide—we do the induction on the relevant syntactic element
starting with the efin for this theorem. The only major complication is that for the bottom-up
visit rules, we need to do an inner well-founded induction on the ≺ relation on values when
traversing the children in order to terminate.
The result n is simply taking to be n′ = 1 + n where n is the maximal fuel used in a
sub-term.

60

