From Syntactic Theories to Interpreters:
A Specification Language and Its Compilation
Yong Xiao1

Zena M. Ariola1

Michel Mauny2

arXiv:cs/0009030v1 [] 29 Sep 2000

1
2

University of Oregon, Eugene, OR 97403⋆⋆⋆
INRIA-Rocquencourt and New York University

Abstract. Recent years have seen an increasing need of high-level specification languages and tools generating code from specifications. In this
paper, we introduce a specification language, SL, which is tailored to
the writing of syntactic theories of language semantics. More specifically, the language supports specifying primitive notions such as dynamic
constraints, contexts, axioms, and inference rules. We also introduce a
system which generates interpreters from SL specifications. A prototype
system is implemented and has been tested on a number of examples,
including a syntactic theory for Verilog.

1

Introduction

Syntactic theories have been developed to reason about many aspects of modern
programming languages[AB97, AFM+ 95, LS97, SS99, FLS99]. Having roots in
the λ-calculus, these theories rely on transforming source programs to other
source programs. Only the syntax of the programming language is relevant.
Experience shows that the development of such theories is error-prone. In order to ensure that the theories are sensible, many properties need to be checked.
For example, we need to know if we have enough rules to rewrite a program to
its value, if the type of a program is preserved during evaluation, and whether
each program has a unique value. In many situations, the proofs of these properties do not require deep insight. In fact, many purported proofs suffer from
being incomplete, and usually the missed case is the problematic one. Thus, we
think that in order to rely on syntactic theories, it is of mandatory importance
to design tools that support their development. The work described in this paper
offers a first step towards that direction.
We introduce the specification language SL, which can directly reflect the
primitive notions of syntactic theories such as evaluation contexts and dynamic
constraints. An experimental system has been implemented that generates interpreters from SL specifications. Currently the generated interpreters are programs
in Caml[Cam] which is a dialect in the ML family. Various examples have been
tested, including the operational semantics of core-ML (lambda-calculus with
built-in operations, store operations, and exception handling), type inference
⋆⋆⋆

Supported by NSF grant CCR-9624711

for core-ML, a syntactic theory for a store encapsulation language[SS99], and a
syntactic theory for Verilog[FLS99].
The paper is organized as follows: Section 2 gives an overview of the SL
system using the call-by-value λ-calculus as an example. Section 3 describes some
issues in compiling SL programs, such as type checking for contexts, patternmatching, and code generation. Section 4 presents related work and concludes
the paper.

2

Overview of the SL System

We introduce the call-by-value λ-calculus[Plo75] and show how it is specified in
the SL language. By convention, we call the SL language the meta-language,
and call the call-by-value λ-calculus the object-language.
2.1

A Syntactic Theory for Call-by-value λ-calculus

The set of terms of the call-by-value lambda calculus is generated inductively
over an infinite set of variables (ranged over by x, y, etc): it includes λ-abstractions
and applications:
Terms

M ::= x | λx.M | M M

The semantics is based on the βv reduction rule which requires a syntactic
definition of the notion of value:
Values
βv

V ::= λx.M
(λx.M )V → M [x := V ]

where M [x := V ] is the term resulting from substituting free occurrences of
variable x with V .
A call-by-value computation consists of successively applying the βv reduction rule to a subterm. Positions of βv redexes are restricted by an evaluation
context which is defined as follows:
H ::= ✷ | HM | V H
where ✷ represents a “hole”. If H is an evaluation context, then H[M ] denotes
the term that results from placing M in the hole of H. The evaluation of a
program is then defined by a stepping relation, denoted by 7→, given as follows:
M → M′
H[M ] 7→ H[M ′ ]

SIGNATURE:
type M = Var of string | Lam of string*M | App of M*M;;
startfrom M;;
SPECIFICATION:
#open "namesupply";;
let rec subst (t1,x,t2) =
match t1 with
Var s -> if s = x then t2 else t1
| Lam(s,t1’) -> if s = x then t1
else let s’ = freshname() in
Lam(s’, subst(subst(t1’,s,Var s’),x,t2))
| App(t11,t12) -> App(subst(t11,x,t2),subst(t12,x,t2));;
dynamic V = Lam _;;
axiom betav: App(Lam(x,t1), (t2:V)) ==> subst(t1, x, t2);;
context H =

BOX | App(H,_) |

App(V,H);;

inference eval:
t1 ==> t2
------------------(h:H) t1 |==> h t2 ;;

Fig. 1. An SL Specification of a Simple CBV Language

2.2

Representation in SL

The specification of the call-by-value λ-calculus in SL is given in Fig. 1. The
SIGNATURE part describes the abstract syntax of the language using Caml type
definitions. In general, the SL type definitions may be polymorphic but are
restricted to first-order type expressions (no function types). To account for
cases in which the description needs more than one type, the type of programs
in the object language is explicitly given by the startfrom phrase.
The SPECIFICATION part describes the semantics of the language. A dynamic
definition defines a subset of a type with a semantic significance. The axioms
are conditional rewriting rules. The optional conditions are Caml expressions
following the keyword when. The meta-language also has a primitive notion of
contexts with BOX as the empty context. Each inference rule has one premise
clause and one conclusion clause, also with an optional condition expression.
Axioms and inference rules use a richer notion of pattern-matching than the
one used in most functional languages: they include dynamic constraints like
in t2:V, context constraints and context fillings like in h:H and h t2. Meta-

operations of the semantics like substitution are written directly in Caml as
auxiliary definitions.
2.3

Generating interpreters

The SL system is very domain-specific, targeting exactly the kind of semantic
specifications based on syntactic theories. In addition, it performs basic checks to
ensure the specifications are well-formed. Other than the basic syntactic checks,
the SL system has a (meta-)type system that ensures that contexts are used
appropriately, e.g., every context has one hole, and contexts are filled with expressions of the appropriate types, and both sides of each axiom have the same
type. After performing these basic checks, the SL system compiles the specification into a non-deterministic automaton, which is then transliterated into Caml
code; the code uses success continuations for encoding the sequencing of states;
and exceptions with handlers for encoding the non-deterministic selection of a
state.
Feeding the code in Fig. 1 to the SL system produces an interpreter. This
interpreter can then be invoked on terms of the language to evaluate them by
repeatedly decomposing them into evaluation contexts and redexes, and contracting the redexes, until an answer is reached. For example, if the input file
contains:
App(Lam("y",Var "y"),App(Lam("x",Var "x"),Lam("z",Var "z")));;

the generated interpreter produces:
App(Lam("y",Var "y"),App(Lam ("x",Var "x"),Lam("z",Var "z")))
==>
by betav,eval
App(Lam("y",Var "y"),Lam("z",Var "z"))
==>
by betav,eval
Lam("z",Var "z")

Interpreters generated by the SL system preserve the semantics of objectlanguages in the sense that if a specification is non-deterministic, the generated
interpreter evaluates input programs non-deterministically. The current version
does not employ backtracking in evaluation.

3

Compiling SL specifications

The compilation of an SL specification includes the usual phases such as lexing,
parsing, static checking, and code generation. For an object-language specified

by an SL program, a parser and a pretty-printer of the object-language are
generated from the signature part, and a reduction machine based on patternmatching automata is generated from the semantic rules. These parts work together as an interpreter for the object-language with the support of the SL
runtime libraries.
Next, we introduce some issues in the SL compilation such as typing contexts,
building automata, and transforming automata into Caml code.

3.1

Typing contexts

The type system for SL extends the type system for Caml. The extensions deal
with dynamic definitions and contexts. Here, we only present the idea of typing
contexts in a simply-typed framework. Typing dynamic definitions is similar.
First, we give definitions of meta-expressions, context expressions, and their
types.
Expressions
Context Expressions
Context Definitions
Types
Context Types

E ::= c0 | c1 E | (E, E) | x | λx.E | E E | N [E]
H ::= ✷ | N | c1 H | (H, E) | (E, H) | N [H]
L ::= N = H | · · · | H
T ::= a | T ∗ T | T → T
U ::= T ◦→ T

We write x for variables, c0 for nullary constructors, c1 for constructors of
arity one, a for constant types, and N for context names. Note that the symbol
“=” and the symbol “|” in a context definition are symbols of the SL language.
The expressions include context filling, and tuple expressions are represented as
nested pairs. Context expressions are distinguished from expressions, for they
always contains one hole. The type of a context expression has the form t1 ◦→ t2 ,
where t1 is the type for the hole and t2 is the type of the whole expression if the
hole is filled. For a context definition N = H1 | · · · | Hn , each Hi should have
the same type as the context type of N .
The typing rules are given in Table 1. Γ is a basis for type checking, which
contains type assignments for constructors, variables, and context names. It has
properties such as weakening where it may have unused assignments, strengthening where unused assignments can be removed, permutation where the order
of assignments is irrelevant, and contraction where assignments can be used
more than once. The first part in the table is the set of rules for expressions.
Most are standard except the rule for context filling which is similar to function
application. The second part is the set of rules for context expressions. These
rules express the “lifting” of the context type constructor ◦→ whenever possible,
so that context expressions preserve context types. The rule for filling contexts
with context expressions is similar to function composition. If a context N has
type τ1 ◦→ τ2 and a context expression h has type τ0 ◦→ τ1 , then the context
expression N [h] has type τ0 ◦→ τ2 .

Γ, c0 : τ ⊢ c0 :τ

Γ, c1 : τ1 → τ2 ⊢ c1 :τ1 → τ2

Γ, x : τ ⊢ x:τ

Γ, N : τ1 ◦→ τ2 ⊢ N :τ1 ◦→ τ2

Γ ⊢ c1 :τ1 → τ2
Γ ⊢ e:τ1
Γ ⊢ c1 e:τ2
Γ, x : τ1 ⊢ e:τ2
Γ ⊢ λx.e:τ1 → τ2

Γ ⊢ e1 :τ1
Γ ⊢ e2 :τ2
Γ ⊢ (e1 , e2 ):τ1 ∗ τ2
Γ ⊢ e1 :τ1 → τ2
Γ ⊢ e2 :τ1
Γ ⊢ e1 e2 :τ2

Γ ⊢ e1 :τ0 ◦→ τ1
Γ ⊢ e2 :τ0
Γ ⊢ e1 [e2 ]:τ1

Γ ⊢ ✷:τ ◦→ τ
Γ ⊢ h:τ0 ◦→ τ1
Γ ⊢ e:τ2
Γ ⊢ (h, e):τ0 ◦→ τ1 ∗ τ2

Γ ⊢ c1 :τ1 → τ2
Γ ⊢ h:τ0 ◦→ τ1
Γ ⊢ c1 h:τ0 ◦→ τ2
Γ ⊢ e:τ1
Γ ⊢ h:τ0 ◦→ τ2
Γ ⊢ (e, h):τ0 ◦→ τ1 ∗ τ2

Γ ⊢ N :τ1 ◦→ τ2
Γ ⊢ h:τ0 ◦→ τ1
Γ ⊢ N [h]:τ0 ◦→ τ2

Table 1. The type checking rules for SL expressions and context expressions

3.2

Building pattern-matching automata

Pattern-matching is the crucial part in compiling an SL specification. A naive
way is to check a list of patterns one by one. The obvious drawback of this
approach is inefficiency. Tree-like automata [GS84] address the efficiency issue.
The matching proceeds by making branches of different constructors and ascribing the list of patterns to those branches. This approach has the disadvantage of space explosion. The combination of tree automata with failures
is the basis for the current implementations of most common functional languages [Mar94, Ler90]. The pattern-matching of the SL system follows this approach, but the support of semantic notions and the non-determinism of rewriting require extensions to the existing algorithms.
1. SL Patterns
The SL patterns include common patterns such as wildcard patterns, variable patterns, alternative patterns, type constraint patterns, alias patterns,
and tuple patterns. The SL patterns are also enriched with dynamic constraint patterns and context filling patterns. The dynamic constraint (p :

dynamic name) and context filling (p : context name) p2 require p to be a
wildcard pattern or a variable pattern. The SL patterns are formally defined
as follows:
Patterns

Axioms
Inference Rules
Dynamic Definitions
Context Definitions

P ::= | x | c0 | c1 P | P |P | P as x
(P : type τ ) | (P, . . . , P ) |
(P : dynamic name) |
(P : context name) P
A ::= P when E ==> E
E ==> Q
I ::=
P when E |==> E
D ::= P
H(x) ::= P

where E denotes Caml expressions, and Q denotes restricted SL patterns
which do not contain dynamic constraints and context fillings.
The SL patterns are used in the left-hand sides of axioms and of conclusion
clauses of inference rules. Dynamic definitions can be considered as definitions of SL patterns, and context definitions are parametric patterns where
the parameters denote the holes. Both definitions can be recursively defined.
The dynamic definition, context definition, and rules in Fig. 1 can be represented in terms of SL patterns as follows:
V = Lam
βv : App(Lam(x, M ), (v : V ))==>M [x := v]
H(x) = x | App((h1 : H)(x), ) | App((v : V ), (h2 : H)(x))
t1 ==> t2
eval :
(h : H) t1 |==> h t2
where variables are introduced for dynamic constraint and context filling
patterns.
2. Automata
An automaton consists of states. Some states are final. Matching a term consists of traversing the states until reaching a final one. States are inductively
defined as follows:
States

S ::= branch (t, (test, S), . . . , (test, S)) | accept E |
S| · · · |S | fail | let vars = f E in S |
if E then S else S | let vars = vars in S

where vars denotes a variable or a tuple of variables.
The first four states are standard. branch (t, (test1 , S1 ), . . . , (testn , Sn )) is
a branch-test state, where t is the term under test, and each testi has the
form c0 , c1 x, or “ ” for otherwise. All tests are mutually disjoint. accept e
is a final state, where e is a Caml expression representing the action after acceptance. A choice state S1 | · · · |Sn has alternatives S1 , . . . , Sn . When
pattern-matching traverses this state, it non-deterministically chooses to enter an alternative. If a final state is reached, then traversing the choice state

is successful. Otherwise it backtracks to other alternatives. This semantics
differs from the usual choice state whose alternatives are ordered (lexically).
fail is a failure state. One new form, reference state let vars = f e in S1 , is
added to support dynamic values and contexts. It calls a function matching
the parameter as the corresponding dynamic value, context, or redex . If it
succeeds, it continues in state S1 , failures in S1 may cause backtracking to
other possibilities in the function call f e.
States are also extended with conditional expressions and let variable bindings. The reason for the former extension is that the semantic rules are
conditional. The latter extension is helpful for code generation. States are
annotated with terms to be matched, but we made them implicit in our
presentation.
3. Structures for pattern-matching
The SL compiler collects the inference rules and axioms with the same type
together. The patterns of the rules form a vector which can be considered as a
one-column matrix. Each rule contributes a row in the matrix. We introduce
parameters bound to the terms matching the patterns, and we keep track
of variable bindings in pattern-matching. There is also a state for each rule,
indicating what to do when the patterns of the rule have been matched. The
whole pattern-matching structure is represented as follows:


t1 · · · tn
 p11 · · · p1n

 ..
.
 . · · · ..

s1
..
.

pm1 · · ·pmn sm







The compilation of pattern-matching can be regarded as a function, C, which
maps such a structure to a state.
The initialization of the pattern-matching sets the states in the structure.
– For an axiom p1 when ec ==> er , the corresponding state is:
if ec then accept er else fail
– For an inference rule

e1 ==> p1
, the corresponding state is:
p2 when ec ==> e2

if ec then let p1 = rewrite1 e1 in accept e2 else fail
where rewrite1 is one-step rewriting function in the generated code.
4. Pattern-matching algorithm
The pattern-matching algorithm is a divide-and-conquer algorithm. It selects
one column of the pattern matrix to work on according to certain criteria.
Without loss of generality, we assume that the algorithm always chooses the
first column. The algorithm repeats the following steps until the pattern
matrix is empty:

(a) Preprocessing
This step canonicalizes the patterns in the first column. It removes the
type constraints since the type information is not useful at the current
stage. It binds variables in alias patterns to the corresponding parameters. It turns each alternative pattern into several rows having one alternative each. Formally, the preprocessing repeats the following simplifications.




t1
···
t1 · · ·

 ..
..
.
.

 . · · · .. 
.
· · · .. 




C
 −→ C  pi1 · · ·si 
 (pi1 : type τ )· · ·si 


..
..
..
..
.
· ·
·.

 . ··· .

t1
···
t1 · · ·

 ..

..
.
..

 . ···

.
· · · .. 
.




C
−→ C 


(p
as
x)·
·
·s
p
·
·
·let
x
=
t
in
s
i
1
i
 i1
 i1
..
..
..
..
.
··· .
 . ···  .


t1 · · ·
t1
···
 ..
.

 . · · · .. 
..
.. 




.
·
·
·
.


C
−→ C 
 pi1a |pi1b · · ·si 
 pi1a · · ·si 
 pi1b · · ·si 




..
.
..
.
.
· · · ..
. · · · ..
(b) Splitting the matrix
The algorithm splits the matrix horizontally, so that in each submatrix,
all first-column patterns are in one of the following groups:
– variable group: wildcard patterns or variable patterns,
– tuple group: tuple patterns,
– constructor group: constructor patterns,
– dynamic constraint group: dynamic constraint patterns on the same
dynamic definition,
– context filling group: context filling patterns on the same context
definition.
The result of the splitting is a choice state.


t1 · · ·
 p11 · · · s1

C .
.
 .. · · · ..

pm1 · · ·sm









 −→ C 



t1 · · ·
p11 · · · s1
..
.
. · · · ..
pk1 1 · · ·sk1










···
 p(k +1)1 · · ·skl +1 
 l

|···| C 
..
. 

.
· · · .. 
t1

pm1 · · · sm

(c) Analyzing different cases
For each submatrix, the compilation function C is inductively defined as
follows:

i. Base case:
When the pattern matrix is empty, pattern-matching is vacuously
successful. The function C creates a choice state.



s1


C  ...  −→ s1 | · · · |sm
sm
ii. Variable group:
Wildcard and variable patterns always match successfully. The function C removes the column of patterns. For variable patterns, bindings are added for further access to the variables.





t1 · · ·
t2 · · ·
 ..
 ..

. 
..
 . · · · .. 
 . ···

.




 · · ·si 
 pi2 · · ·

si




C .
−→ C  .


.
.
..
 .. · · · .. 
 .. · · ·





 x · · ·sj 
 pj2 · · ·let x = t1 in sj 




..
..
..
..
. ··· .
. ···
.
iii. Tuple group:
The function C treats each component of the tuple as an individual
pattern. It replaces the first column of patterns with columns of the
component patterns, and introduce parameters for the components.

let 
(t11 , · · · , t1k ) = t1 in
t1
···
t11 · · · t1k · · ·
 (p111 , · · · , p11k ) · · · s1 


 p111 · · · p11k · · · s1 
C

..
.  −→ C 
 ..

.
. 
.
· · · .. 
 . · · · .. · · · .. 
(pm11 , · · · , pm1k )· · ·sm
pm11 · · ·pm1k · · ·sm


iv. Constructor group:
The function C collects the rows which have the same constructor in
the first column into a group of new pattern-matching structures, and
it creates a branch-test state. The tests of the state are distinguished
by having different constructors as roots. The corresponding actions
for the tests are the results of compiling the new structures. In the
new structures, the first column is removed for the constructors of
zero arity, or it is replaced by the column of argument patterns for
the constructors of non-zero arity.




t2 · · ·
 pi1 2 · · ·si1 


C .
. )
 .. · · · .. 







 (c ,

0


t1 · · ·


.. 


 ..


 . ··· . 
p
·
·
·s
i
2
i
2
2






 c0 · · ·si 
..
..




.
−→ branch t1 , .
C .


.
′

 .. · · · .. 
let 
c1 t1 = t1 in 






 c1 p′ · · ·sj 
t′1 · · ·
j1




′




..
..
 (c1 t′1 ,
 pj1 1 · · ·sj1  ) 
. ··· .


C .

.

 .. · · · ..  
p′j2 1 · · ·sj2


v. Dynamic constraint group:
The function C creates a reference state. The reference will initiate
pattern-matching for the dynamic definition D with the value of t1 .
Its result is bound to a new parameter. The state in the let body is
the result of compiling a structure consisting of the patterns without
the constraint and the rest of the patterns.


let 
t′1 = match 
D t1 in
t′1 · · ·


 p′11 · · · s1 
 −→


C .

.. 
.
 . ··· . 
: D)· · ·sm
p′m1 · · ·sm

t1
···
 (p′11 : D) · · · s1

C
..
.

.
· · · ..
(p′m1



Pattern-matching for dynamic definitions will be presented later.
vi. Context filling group
Similar to the dynamic constraint group, the function C creates a
reference state. The reference will initiate pattern-matching for the
context definition H with the value of t1 . Its result is bound to a
pair of parameters which represent the context and the corresponding hole occurring in t1 . The state of the let body is the result of
compiling a structure consisting of the context patterns, the hole
patterns, as well as the rest of the patterns.


 (p′11

C

(p′m1

′ ′′

let (t
1 , t′1 ) =′′match H
 t1 in
t1
···
t
t
·
·
·
1
1
: H)p′′11 · · · s1 

 p′11 p′′11 · · · s1 


..
..  −→
C .
..
.. 
.
··· . 
..

. ··· . 
: H)p′′m1 · · ·sm
′
′′
pm1 pm1 · · ·sm

Pattern matching for context definitions will be presented next.

5. Matching dynamic definitions and context definitions
Pattern-matching for dynamic definitions and context definitions uses the
same form of structures and uses the same algorithm. Each definition corresponds to a structure which has only one pattern, one parameter and one
state. The pattern comes from the definition. Assume t is the term to be
matched, the state is initialized as follows:
– For a dynamic definition, the state is accept t.
– For a context definition, the state is accept (λx.body, x), where x is the
parameter for the context and the body is a placeholder. When the base
case in the algorithm is encountered, the SL compiler sets the contents
of body by reconstructing the term t with the variable x. Each body may
have different content if the final state is copied. The reconstruction
retrieves the bindings along the path from the start state to the final
state.
In other words, matching a context definition returns a pair with a constructing function and a term filling the hole. Applying the function to
the term results in the term t.
The state starting pattern-matching for a definition can be referred to by the
name of the definition. For example, the dynamic definition and the context
definition in Fig. 1 are associated with the following states:
match D t = branch(t, (Lam t′ , accept(t)))
match H t = let x = t in accept(λx.body1 , x) |
branch(t,
(App t′ , let (t1 , t2 ) = t′ in
(let (t′1 , t′′1 ) = match H t1 in
let h1 = t′1 in
let x = t′′1 in accept(λx.body2 , x)) |
(let t′1 = match D t1 in let v = t′1 in
let (t′2 , t′′2 ) = match H t2 in
let h2 = t′2 in
let x = t′′2 in accept(λx.body3 , x))))
where body1 , body2 and body3 are as follows:
body1 : let t = x in t
body2 : let t′′1 = x in let t′1 = h1 in let t1 = t′1 t′′1 in
let t′ = (t1 ,t2 ) in let t = App t′ in t
body3 : let t′′2 = x in let t′2 = h2 in let t2 = t′2 t′′2 in
let t′1 = v in let t1 = t′1 in let t′ = (t1 ,t2 ) in
let t = App t′ in t
3.3

Transforming automata into Caml code

The transformation of states in the pattern-matching automata into Caml code
is described in Fig. 2. Each state corresponds to a function with implicit parameters for the terms to be matched and a continuation expressing the remaining

pattern-matching work. The initial continuation for rewriting is the identity
function. State functions may raise an exception when matching of the state
fails. The branch-test state corresponds to the match · · · with · · · construct in
Caml. If the branch tests do not cover all constructors of the same type, a default test associated with a failure state is added. For a final state, the success
continuation is consumed by applying it to the expression. For a choice state,
a random alternative is tried. Failure exceptions may be caught and then other
alternatives can be tried. The failure state just raises a failure exception. For a
reference state, it calls the matching function with the continuation accepting
the result, then it continues with the state in the body of the let. The conditional expressions and variable bindings in states are considered atomic with
respect to continuation passing and exception handling. Transforming a conditional state is thus transforming both branch states, and transforming a let
state is transforming the in part.

[[ branch (t, (c0 , S0 ), . . . , (c1 x, S1 )) ]] k =
match t with
c0 -> [[ S0 ]] k
..
.
c1 x -> [[ S1 ]] k
-> raise failure
[[ accept e ]] k = k (e)
[[ S1 | · · · |Sm ]] k =
try [[ Si ]] k
with failure ->
[[ S1 | · · · |S1−i | Si+1 | · · · |Sm ]] k
[[ fail ]] k = raise failure
[[ let vars = f e in S ]] k =
f e (λt. let vars = t in [[ S ]] k )
[[ if ec then S1 else S2 ]] k =
if ec then [[ S1 ]] k else [[ S2 ]] k
[[ let vars1 = vars2 in S ]] k =
let vars1 = vars2 in [[ S ]] k

0≤i≤m

Fig. 2. Generating Caml code

4

Summary and Discussion

The SL system uses the first-order types of functional languages for specifying abstract syntax. We have not followed the approach of higher-order abstract
syntax (HOAS) [PE88]. The HOAS representation would allow the variables of
the object language to be represented as meta-variables, and hence alleviates

the need for explicitly reasoning about variable renaming and substitution of
variables. However, higher-order abstract syntax interacts poorly with the inductive reasoning techniques needed to reason about the properties of semantic
specifications [DPS97].
The SL system uses conditional rewriting rules for specifying semantic rules.
In other words, the system employs rewriting semantics (a.k.a. reduction semantics). Some systems[HM92, CDD+ 88] express rules in natural semantics[CDD+ 85].
Natural semantics is well adapted to describing static behaviors such as typing.
For transformational behaviors, such as dynamic semantics, rewriting semantics proves to be more modular[WF94], and should therefore be more tractable
when it comes to expressing full-size programming languages. Another advantage of rewriting semantics is that it allows one to observe intermediate states
of reductions, so that it is more suitable for non-terminating object-systems.
ELAN[ELA] is a system also based on first-order rewriting semantics. It has
more general application areas than the SL system. It supports many-to-one
associative-commutative(AC) patterns and provides an efficient algorithm[MK98].
Its strategy language gives flexible control over non-deterministic reductions. The
Stratego[VB98] system has more generic strategy specifications. There are also
general-purpose tools that can be used for manipulating formal semantics, such
as Coq[Coq], Isabelle[Isa] and Twelf[Twe]. Compared to those systems, the novelty of the SL system is that it directly supports the specification of the semantic
notions such as dynamic values and evaluation contexts, and it automatically
generates executable interpreters. Associative-commutative patterns can be represented by contexts, but the current SL system does not optimize matching for
efficiency.
Fahndrich and Boyland [FB97] investigate abstract patterns which are even
more general than contexts in the SL system. They build automata for patterns and check the properties of the patterns such as exhaustiveness and nonoverlapping, but they did not provide a computational view of pattern-matching.
The current prototype of the SL system constitutes a first step towards
designing a specification language for syntactic theories and implementing a system generating interpreters from specifications. It also provides an extension
to pattern-matching techniques. A number of interesting examples have been
tested in the prototype system. Follow-up work is underway to allow more expressive specifications, to optimize the compilation of the SL language, and to
automatically prove properties of syntactic theories.

Acknowledgment: The first author thanks the Cristal group at INRIA Rocquencourt for funding his visit from July,1998 to September, 1998. We thank
Xavier Leroy, Didier Remy, Amr Sabry, and Miley Semmelroth for stimulating
discussions about this work.

References
[AB97]

Zena M. Ariola and Stefan Blom. Cyclic lambda calculi. In the International Symposium on Theoretical Aspects of Computer Software (TACS),
1997.
[AFM+ 95] Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and
Philip Wadler. A call-by-need lambda calculus. In the ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 233–
246. ACM Press, New York, 1995.
[Cam]
http://caml.inria.fr/man-caml/index.html, the Caml Light System Homepage.
[CDD+ 85] D. Clément, J. Despeyroux, T. Despeyroux, L. Hascoet, and G. Kahn.
Natural semantics on the computer. Rapports de Recherche 416, INRIA,
Sophia Antipolis, 1985.
[CDD+ 88] D. Clément, J. Despeyroux, T. Despeyroux, L. Hascoet, G. Kahn, and
V. Pascual. Centaur: the system. In SIGSOFT’88, Third Annual Symposium on Software Development Environments (SDE3), Boston, 1988.
[Coq]
http://pauillac.inria.fr/coq, the Coq Project Homepage.
[DPS97] Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In R. Hindley, editor, Proceedings
of the Third International Conference on Typed Lambda Calculus and Applications, pages 147–163, Nancy, France, April 1997. Springer-Verlag, Berlin.
[ELA]
http://www.loria.fr/ELAN, the ELAN System Homepage.
[FB97]
Manuel Fähndrich and John Boyland. Statically checkable pattern abstractions. In the ACM SIGPLAN International Conference on Functional Programming, pages 75–84. ACM Press, New York, 1997.
[FLS99] John Fiskio-Lasseter and Amr Sabry. Putting operational techniques to the
test: A syntactic theory for behavioral Verilog. Electronic Notes in Theoretical Computer Science, 26:32–49, 1999. Third International Workshop on
Higher Order Operational Techniques in Semantics.
[GS84]
Ference Gécseg and Magnus Steinby. Tree Automata. Akadémiai Kiadó,
Budapest, 1984.
[HM92]
John Hannan and Dale Miller. From operational semantics to abstract machines. Journal of Mathematical Structures in Computer Science, 2(4):415–
459, 1992.
[Isa]
http://www.cl.cam.ac.uk/Research/HVG/Isabelle, the Isabelle System
Homepage.
[Ler90]
Xavier Leroy. The ZINC experiment: an economical implementation of the
ML language. Technical report 117, INRIA, 1990.
[LS97]
John Launchbury and Amr Sabry. Monadic state: Axiomatization and type
safety. In the ACM SIGPLAN International Conference on Functional Programming, pages 227–238. ACM Press, New York, 1997.
[Mar94]
Luc Maranget. Two techniques for compiling lazy pattern matching. Research report 2385, INRIA, 1994.
[MK98]
Pierre-Etienne Moreau and Hélène Kirchner. A compiler for rewrite programs in associative-commutative theories. In ”Principles of Declarative
Programming”, number 1490 in Lecture Notes in Computer Science, pages
230–249. Springer-Verlag, September 1998.

[PE88]

[Plo75]
[SS99]

[Twe]
[VB98]

[WF94]

Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In the
ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208, June 1988.
Gordon D. Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoret. Comput. Sci., 1:125–159, 1975.
Miley Semmelroth and Amr Sabry. Monadic encapsulation in ML. In
the ACM SIGPLAN International Conference on Functional Programming,
pages 8–17. ACM Press, New York, 1999.
http://www.cs.cmu.edu/∼twelf, the Twelf System Homepage.
Eelco Visser and Zine-el-Abidine Benaissa. A core language for rewriting. Electronic Notes in Theoretical Computer Science, 15, September 1998.
In C. Kirchner and H. Kirchner, editors, Proceedings of the Second International Workshop on Rewriting Logic and its Applications (WRLA’98),
Pont-à-Mousson, France.
A. K. Wright and M. Felleisen. A syntactic approach to type soundness.
Information and Computation, 115:38–94, 1994.

This article was processed using the LATEX macro package with LLNCS style

