A Semantic Prototyping System

Mitchell Wand

Computer Science Department Indiana University Lindley Hall 101 Bloomington, IN 47405 USA

This Material is based on work supported by the National Science Foundation under grants MCS-7904183 and MCS-8303325.

Abstract

We have written a set of computer programs for testing and exercising programming language specifications given in the style of denotational semantics. The system is built largely in Scheme 84, a dialect of LISP that serves as an efficient lambda-calculus interpreter. The system consists of:

• a syntax-directed transducer, which embodies the principle of compositionality,

• a type checker, which is extremely useful in debugging semantic definitions, and

• an interface to the yacc parser-generator, which allows the system to use concrete syntax rather than the often cumbersome abstract syntax for its programs. In this paper, we discuss the design of the system, its

implementation, and discuss its use.

1. Introduction

The fundamental thesis of denotational semantics is that the meaning of a language may be expressed as a syntaxdirected transduction from the phrases (or parse trees) of the language to certain sets of functions, which are conveniently expressed using the lambda-calculus. If one has a lambdacalculus interpreter, one can run a program by transducing it to a lambda-calculus term and then reducing the term to normal form.

This observation can be pursued in a variety of directions. Mosses [75, 76] and Jones and Schmidt [80] optimized the lambda-terms prior to reducing them. Wand [82ab] considered alternate representations as a way of deriving compilers. In this paper, we will consider how this observation can be engineered into a useful software tool.

We started with Scheme 84, a dialect of Lisp that serves as an efficient lambda-calculus interpreter. Scheme 84 differs from the lambda-calculus in a number of important ways, but it is adequate and efficient for the terms that arise in typical semantic definitions. It is quite easy to write a syntaxdirected transducer in Scheme, but this alone is not enough to consitute a useful tool (as we discovered the hard way!). The transduction is actually into the terms of the typed lambda-calculus, and most errors in semantic definitions show up as type errors. It is therefore extremely useful to have a typechecker which is capable of analyzing the transducer and its auxiliary functions for type consistency. This typechecker turned out to be the most involved portion of the system. Last, it is convenient to have access to a parser generator, so that the programs in the language to be simulated can be written using concrete syntax rather than by writing parse trees by hand. (This, too, we learned from necessity).

A typical language definition, then, consists of definitions of types and auxiliary functions, and a transducer that includes the traditional grammar and semantics. The auxiliary functions and transducer are checked by the type-checker. The transducer is processed to produce a parser and an interpreter for the language. A short complete example is included in the appendix.

A program in the defined language may be run by piping it through the parser; the parser’s output is then interpreted. Execution of programs in this way is quite efficient, as both the yacc-generated parser and the Scheme-based interpreter are more efficient than similar modules in other semanticsbased systems.

In this paper we will discuss the elements of the system, with an emphasis on the design choices we made and how they contrast with similar components in other systems.

2. Environment

Scheme 84 [Friedman et. al. 84] is a local dialect of Scheme [Steele & Sussman 78]. It is a dialect of Lisp that offers lexical binding and functions (and objects) as firstclass values which may be passed without restriction. As such, it becomes an applicative-order (i.e. call-by-value) lambda-calculus interpreter. While applicative order is not complete, it is complete on the terms used in continuation semantics, which is the style we advocate and use almost exclusively. Furthermore, its call-by-value semantics may be implemented far more efficiently than the call-by-name semantics used in some other systems, and normal-order reduction can be simulated when necessary [Steele & Sussman 78]. These properties make Scheme an attractive base for a semantic meta-language.

Scheme 84 is implemented in Franz Lisp, which runs on our VAX 11/780 under UNIX.* Scheme code is compiled to code for an abstract machine (the VSM machine), which is then simulated in Lisp. The use of Franz Lisp as a host also enables us to use the large set of tools available in Franz Lisp and in Unix. In particular, we use the parser-generator yacc [Johnson 75].

3. The Type Checker

3.1 Design Considerations

Our type checker is based on the one in ML [Gordon et. al. 78]. It is rather different in design, however, since our context was quite different. First, since we were interested in denotational semantics, we had to deal with reflexive types, which are disallowed in ML except in absrectypes. Secondly, since we were using type checking as a debugging tool rather than as a guarantor of system-integrity, as ML was, we could adopt a rather different attitude toward holes in the type system.

Both ML’s system and ours rely on Robinson’s algorithm for finding most general unifiers (mgu’s) [Robinson 65]. To allow reflexive types, we had to modify this algorithm. The

* Unix is a trademark of AT&T Bell Laboratories basic modification is the removal of the so-called “occurrence check” in the algorithm, as is done in many Prolog implementations. [J.A. Robinson, personal communication]. We actually used a structure-sharing unification algorithm as in [Boyer & Moore 72]. In this version one needs to do more than remove the occurrence check; we introduce some additional tests and use an algorithm, based on some simple finite-state automata theory, to check whether two (infinite) branches of the type-tree were equal.

In addition, provision had to be made for Scheme’s multipleargument functions. The resulting type-checker resembles that in HOPE [Burstall, MacQueen, & Sannella 80].

In ML, the typechecker serves as a guarantor of system integrity. It assures, for example, that a proof in LCF is valid. The underlying machine [Cardelli 84] does not include any run-time type checks, relying on the typechecker to prevent, for example, integers from being applied as functions.

Our situation was different. The underlying Scheme machine had sufficient run-time checking to prevent integers from being applied as functions, or functions from being applied to the wrong number of arguments. Such errors, we found from bitter experience, were quite difficult to debug at run-time, but were detectable by type-checking at compile time. Our goal, therefore, was a system that would catch most such errors, without unduly restricting our programming style.

In this respect, our situation was similar to that of a systems-implementation language. The most important purpose of holes in the type system of a systems-implementation language is that they permit the use of hand-coded data representations in addition to those provided by the standard data type constructors. [Geshke, Morris, & Satterthwaite 77]. This is useful both for efficiency purposes and to allow the use of pre-existing bodies of native code. Thus “holes” were permissible, so long as they were clearly marked and rarely needed. We shall discuss below the nature of the holes we chose.

3.2 Basics

The purpose of the typechecker is to analyze the code for internal consistency prior to compilation. The standard mode of interaction, therefore, was to have types checked only when definitions are processed, not on every application. Thus one can interact easily with both checked and unchecked code. We found the lack of such interaction to be a serious difficulty in our experiments with ML. One can, of course, typecheck any application if desired.

One writes

 (define-checked foo (-> (seq int bool) int) body)

to define a function foo that takes an integer and a boolean and returns an integer. This will succeed only if the body of the definition matches the type given. Again, this is different from the situation in ML, where one never specifies the type of a function, but waits for the function to be misused. We require the user to specify the type (possibly polymorphic) of every function. This is in accordance with the usual practice in mathematics (again drawing on the intended application in denotational semantics). This arrangement seems to work quite well, since it enables one to tell whether the function has been misdefined or whether it has been misused— an important distinction that must be inferred in the ML design.

The types themselves are similar to those in ML, except that (following the LISP tradition) we write them in Cambridge-prefix form. Types may be defined transparently,

via define-type-abbrev, or opaquely, via define-type-

constructor. In a transparent definition, the new type is defined to be identical to the defining type expression. (This is equivalent to so-called structural equivalence). The scope of such type identifiers is global. Typical transparent definitions might be:

   (define-type-abbrev fun (-> (seq val cont) ccont))
   (define-type-abbrev val (union int fun))
   (define-type-abbrev ccont (-> (seq state) ans))
   (define-type-abbrev env (-> (seq ident) val))
   (define-type-abbrev cont (-> (seq val) ccont))

Here val becomes a reflexive type.

3.3 User-defined type constructors

Opaque types and type-constructors can be defined us-

ing define-type-constructor. The definition of such a

constructor includes a list of formal type parameters, the representation of the new type, and definitions of access, construction, and modification functions for the new type. Access to the representation is provided through the functions dec and enc, which have scope local to the type definition. These map the new type to and from, respectively, its representation. The theory of this approach to opaque types is presented in [Wand 84].

   The effect of define-type-constructor is to define its

associated functions, with global scope. The resulting type constructor is construed by the typechecker to be a basic type constructor, on an equal footing with list, pair, etc. From the point of view of the typechecker, the resulting type has no internal structure, and hence one gets so-called name equivalence when matching such types.

   A typical use of define-type-constructor might be

the definition of association lists in Figure 1, which is taken from the standard package. Here alist is defined to be a type constructor of one argument x, with representation (list (pair literal x)). Three global objects are de-

fined: alist$ext, init-alist, and alist$lookup. The

example of init-alist shows that the objects defined need not be functions, nor is there a system-enforced naming convention (though such naming conventions may be added in a future version).

The example of alist$lookup illustrates the use of additional generic type variables in these definitions. While x is declared as a generic type variable throughout the definetype-constructor expression, here we need an additional degree of type-genericity, so we declare y to be an additional generic type-variable. This example also illustrates the idiom for handling of errors: we cannot use the standard Lisp idiom of returning nil on failure, since that would violate typing. Instead, we pass success and failure functions with

(define-type-constructor alist (x)      ; x is a generic type variable.
(list (pair literal x))              ; the representation.
(alist$ext                           ; define a global function alist$ext.
nil                               ; no additional generic type vbles.
(-> (seq (alist x) literal x)     ; the type of alist$ext.
    (alist x))
(lambda (l id val)                ; the body of the function.
   (enc                           ; be sure to encode the list.
      (cons (pair id val)
            (dec l)))))           ; be sure to decode the alist.
(init-alist                          ; another global definition.
nil
(alist x)                         ; it needn't be a function.
(enc nil))
(alist$lookup (y)                    ; y is an additional generic type
                                 ; variable
(-> (seq literal (alist x)        ; lookup takes a literal, an alist,
       (-> (seq x) y)             ; a success function,
       (-> (seq) y))              ; and a failure function (of 0 args)
    y)                            ; and returns a value of type y.
(lambda (id l succ fail)
   (iterate loop ((l (dec l)))    ; create local loop.
      (cond
         ((null l) (fail))        ; fail by calling the failure
                                 ; function.
         ((eq (lson (car l)) id)
          (succ (rson (car l))))  ; succeed-- call succ with the datum.
         (t (loop (cdr l))))))))  ; otherwise loop.

Figure 1. Code for association-list type constructor.

the same target type (in this case y). We have found this to be a very convenient idiom.

We can use the same device to define opaque types with recursive representations. Figure 2 shows a definition for a stream type. Note that str$cons1 takes a function of no arguments to avoid difficulties with orders of evaluation. The use of the macro str$cons allows the user of the stream

   (define-type-constructor stream (x)
      (pair x (-> (seq) (stream x)))
      (str$cons1 nil
         (-> (seq x (-> (seq) (stream x))) (stream x))
         (lambda (x s)
            (enc (pair x s))))
      (str$car nil
         (-> (seq (stream x)) x)
         (lambda (s)
            (lson (dec s))))
      (str$cdr nil
         (-> (seq (stream x)) (stream x))
         (lambda (s)
            ((rson (dec s))))))
   (defmacro str$cons
       (lambda (l)
           (let ((a1 (cadr l)) (a2 (caddr l)))
               `(str$cons1 ,a1 (lambda nil ,a2)))))
   (define-checked str$and
       (-> (seq (stream bool) (stream bool))
           (stream bool))
       (lambda (s1 s2)
           (str$cons (and (str$car s1) (str$car s2))
               (str$and (str$cdr s1) (str$cdr s2)))))

Figure 2. Code for stream data type, with an example of its use.

type to be oblivious, in most cases, to the order-of-evaluation problem.

3.4 Holes and Interfacing with Unchecked Code

Unchecked code (using the defining-form define) may be intermixed arbitrarily with checked code. In order to use unchecked code inside checked code, one needs to tell the typechecker the putative type of the unchecked code. This can be done by writing (declare-unchecked foo type) which declares the type of foo to be type. This device is, of course, not secure.

In practice, one uses this device to allow an interface to pre-existing code or representations, just as one does in systems-implementation languages. For example, the typeconstructor list uses Scheme’s cons-cells for efficiency; the types of the list manipulation functions are declared with

declare-unchecked. Similarly, alist$lookup is in fact im-

plemented using assq for efficiency and then declared unchecked. An interesting use of declare-unchecked is any:

   (define any '**unbound**)
   (declare-unchecked any (x) x)

This makes any a universally polymorphic object. Such an object is useful to have for initializations. Scheme requires all declarations to be initialized, so any is used to simulate uninitialized declarations, as in the macro rec, which creates a locally-recursive value (usually a procedure):

   (mkmac (rec name value)
          (let ((name any))
               (set! name value)))
   define-type-constructor and any are sufficiently flex-

ible to define (union x y) as a user-defined type constructor. This is shown in Figure 3. An element of union type is represented as a 3-tuple consisting of a tag bit and two data fields. At any given time, only one of the two data fields is in use, and the other contains any. Here inL and inR are the injector functions. casefn (like unioncase in [Reynolds 75]) is the discriminator function. It takes an argument of union type and two functions. The tag field is examined and, depending on which summand the value came from, one of the two functions is applied to the injected value. Thus casefn satisfies the equations

   (casefn (inL x) f g) = (f x)
   (casefn (inR y) f g) = (g y)

   (define-type-constructor union (x y)
      (pair literal (pair x y))
      (inL nil
         (-> (seq x) (union x y))
         (lambda (v)
            (enc (pair 'L (pair v any)))))
      (inR nil
         (-> (seq y) (union x y))
         (lambda (v)
            (enc (pair 'R (pair any v)))))
      (casefn (z)
         (-> (seq (union x y)
                  (-> (seq x) z)
                  (-> (seq y) z))
             z)
         (lambda (l f g)
            ((lambda (q)
                (if (eq? q 'L)
                    (f (lson (rson (dec l))))
                    (if (eq? q 'R)
                        (g (rson (rson (dec l))))
                        (error l))))
             (lson (dec l))))))

Figure 3. Definition of union type.

casefn is another example of the use of additional generic type parameters, and of the “multiple continuation” style of error handling we saw before in alist$lookup. Though the definition of union uses the insecure construct any, the use becomes encapsulated, so that union is type-secure.

3.5 Error Handling

When the type checker processes an application, using Milner’s algorithm, it computes the types of the operands and from them infers a (polymorphic) type for the operator. It then unifies this type with the real type of the operator. If they are not unifiable, then an error message is generated.

Our error messages contain three pieces of information: the application that failed, the given and inferred types for the function, and the actual type expression on which the mgu algorithm failed. The second item, which is not supplied by ML (on either of the two versions we have [Holström & Petersson 82, Cardelli 83]), is quite useful, since it enables the user to determine which argument differed, and hence which variable is being misused in the application. Our mgu algorithm is also coded to return useful information besides the failure token. For example, it gives different error messages for wrong number of arguments to a function or for wrong number of arguments to a type constructor, distinguishing these common errors from a garden-variety type mismatch.

4. The Transducer

The syntax-directed transducer is a relatively straightforward bottom-up transducer. A typical example is shown in Figure 4.

The first item in the list is the parser, which can be written by hand or generated using the parser generator interface (see Section 5). The following items in the list are actions, one per production. Each action consists of a production name, the production itself (to be used by the type checker and the parser generator), dummy variables, and a body.

At each node of the parse tree, the corresponding action is consulted. The values of the subtrees are bound to the dummy variables (like $1, etc. in yacc), and the body is then evaluated. In this example, a typical “dynamic semantics,” the values are Scheme functions, but they could be arbitrary Scheme values.

The transducer itself is a textual object, which is compiled by translating it into a Scheme function that traverses the parse tree. (For the yacc version, the parse tree is not constructed, but rather the Scheme function simulates a postfix machine). The fact that the transducer was written in standard Lisp syntax was, as usual, very convenient: we could design its syntax to concentrate on the semantics of transduction, and furthermore it became relatively easy to write the translation from transducers to traversers.

(define sdt
'((yacc-parser 'example.o)      ; the parser.
(pgm                          ; a production name.
(pgm exp)                  ; the production: pgm -> exp .
(e1)                       ; dummy vble for value of exp.
((e1 init-env init-cont)   ; the value of the node.
 init-state))
(identifier-to-exp
(exp ident)                ; the production: exp -> ident
(id)
(lambda (r k) (k (r id))))
(ident
(ident literal)            ; ident -> literal
(id)
id)
; etc.....
(appl
(exp 'lparen exp exp 'rparen) ; exp -> (exp exp)
(e0 e1)
(lambda (r k)
   (e0 r
      (lambda (v0)
         (casefn v0
            (lambda (n)
               (error (list 'cant-apply-number)))
            (lambda (f)
               (e1 r
                  (lambda (v1)
                     (f v1 k)))))))))))

Figure 4. A typical transducer.

In order to type-check the transducer, it is necessary to associate a type with each non-terminal symbol. This is done using define-type-abbrev. In our mini-example, we might declare:

   (define-type-abbrev pgm ans)
   (define-type-abbrev exp (-> (seq env cont) ccont))
   (define-type-abbrev ident literal)

Given these declarations, the type checker then tries to confirm that the body of each action has the type of the left-hand side of its production, under the assumption that each dummy variable has the type of its corresponding nonterminal. This is done by invoking the function check-sdt (see the Appendix for a complete script).

5. The Parser Generator Interface

The interface to yacc consists of a Scheme program that extracts the grammar (that is, the production part of each action) from the transducer. The grammar information is then piped through awk, which produces suitable lex and yacc files. These are then compiled to produce a Unix filter program that takes the input and produces a stream of production names in postfix order, suitable for processing by a postfix machine. We were amused to notice that pieces of the interface were written in Franz Lisp, Scheme 84, native C, awk, lex, yacc, and csh. This portion of the system, being an interface between two very different subsystems and assembled from pre-existing software parts, claims no medals for elegance, but it does demonstrate once again the flexibility of the Unix toolbox.

6. Experience

With our students, we have used this system to program seven sizable examples studying various programming language features. These are shown in Figure 5.

Each system consists of definitions of types and auxil-

iary functions (using define-type-abbrev, define-type-

constructor, and define-checked), and a transducer, which includes the grammar and the semantic equations. A complete example is included in the appendix.

The first four of these took about 12 man-hours each; the fifth took about 25 man-hours. The most common errors were untyped identifiers (usually misspellings), and failure to

Description  Lines Author
Applicative Lang. with input/output  300 M. Wand
Imperative Lang. with blocks and declarations  222 M. Wand
Mini-Prolog  329 M. Wand
Multiprocessing  549 S. Koelbl
Parameter Passing  800 M. J. Lao
Storage Allocation  379 J. Widom
ASPLE [Marcotty et.al. 76]  700 M. Montenyohl

Figure 5. Applications.

inject a value into a sum domain. The latter class of errors is particularly nasty: there would generally be a dozen or so of them on these examples, and we found on a previous project that it generally took about six hours to find each such error at run time. Detecting these errors at compile time, therefore, is particularly valuable. SIS [Mosses 79, Bodwin et. al. 82] does not include a type checker at all.

Once the type errors were found, the code generally worked with few additional changes. In general, the authors of these examples were pleased with the way the system performed. In addition, we have used the type-checker by itself on several problems (including a second implementation of Prolog), with good results.

The following table shows the approximate size of the various modules in the system:

Section  Lines
Auxiliaries  151
Unifier  93
Checker  416
Transducer  54
Yacc interface  195
Global type defs  104
Total:  1013

Implementation time was approximately 2 man-weeks spread over a period of about 2 months. The small size of the system is the result of the high leverage obtained from using the powerful features of the Scheme programming language, and from the use of the powerful tools (particularly yacc) available in UNIX.

Currently, the system performs type-checking at about 100 lines per cpu minute on our VAX 11/780; this is slow but acceptable. The speed of actual program execution is quite fast: The 11-line program in [Bodwin et. al. 82] took about 6 CPU seconds to parse and compile (most of this time was spent in setting up pipes, etc.), but only about 0.18 seconds to execute. Bodwin reported 7.9 seconds to parse and compile, and 3.1 seconds to execute the same program in SIS on their much faster (by a factor of 10) Amdahl 470/V8 machine. Thus our compiled programs seem to run at least 200 times faster in Scheme than those executed in SIS. We hypothesize that the major reason for the difference in execution speed is that the resulting Scheme code is executed on an abstract machine (the VSM machine), while SIS does direct reduction of λ-calculus expressions. (Pleban [personal communication] has reported a similar speedup for Paulson’s SECD-machine system [Paulson 82] compared to SIS). It is harder to compare the compilation times, since the analyses performed are not the same.

7. Comparison with Related Work

We know of four other systems with goals related to ours. We can summarize the comparisons in Figure 6.

8. Conclusions

We have constructed a useful tool for testing and exercising programming language specifications. The system can be used for “rapid prototyping” of semantics. In addition, its components can be and have been used separately when the full power of the system is not needed. The semantic meta-language is based on the language Scheme, allowing efficient execution of the resulting programs.

System  Parser Generator  MetaLanguage  Typechecker
SIS [Mosses 79]  SLR(1)  DSL(λ-calc)  No
[Paulson 82]  LALR(1)  attribute grammar/λ-calc  ??
Plumb [Sethi 82]  yacc  λ-calc  No
ISI [Kini et. al. 83]  LR(1)  Ada subset  Ada-based
Wand  yacc  λ-calc  ML-based
System Object Language  Execution  Implementation Lang
SIS  λ-calculus  Reduction  BCPL
Paulson  SECD-code  SECD-Machine  PASCAL
Plumb  Directed Graph  None  lex/yacc, C
ISI  AFDL-IL  AFDL-IL Interpreter  Interlisp
Wand  Scheme functions  VSM Machine  Scheme/Franz Lisp

Figure 6. Comparison of Semantics-Based Tool Systems.

References

[Bodwin 82] Bodwin, J., Bradley, L., Kanda, J., Little, D., and Pleban, U. “Experience with an Experimental Compiler Compiler Based on Denotational Semantics,” Proceedings of the SIGPLAN ’82 Symposium on Compiler Construction, SIGPLAN Notices 17, 6 (June, 1982), 216– 229.

[Boyer & Moore 72] Boyer, R.S., and Moore, J S. “The Sharing of Structure in Theorem-Proving Programs,” in Machine Intelligence 7 (B. Meltzer & D. Michie, eds), Edinburgh University Press (1972), 101–116.

[Burstall, MacQueen, & Sannella 80] Burstall, R.M., MacQueen, D.B., and Sannella, D.T. “HOPE: An Experimental Applicative Language,” Conf. Rec. 1980 LISP Conference, 136–143.

[Cardelli 83] PASCAL VAX-UNIX version of Edinburgh ML, converted from VMS by Nobuo Saito, CMU, developed by Luca Cardelli, Bell Laboratories, Murray Hill, March, 1983.

[Cardelli 84] Cardelli, L. “Compiling a Functional Language,” Proc. 1984 ACM Symp. on Lisp and Functional Programming (Austin, TX, 1984), to appear.

[Friedman et. al. 84] Friedman, D.P., Haynes, C.T., Kohlbecker, E., and Wand, M. “The Scheme 84 Reference Manual” Indiana University Computer Science Department Technical Report (March, 1984).

[Geschke, Morris, & Satterthwaite 77] Geschke, C.M., Morris, J.H., & Satterthwaite, E.H., “Early Experience with Mesa” Comm. ACM 20 (1977), 540–553.

[Gordon, et. al. 78] Gordon, M., Milner, R., Morris, L., Newey, M., & Wadsworth, C. “A Metalanguage for Interactive Proof in LCF,” Proc. 5th Annual ACM Symp. on Principles of Programming Languages (1978) 119–130.

[Holmström & Petersson 82] S. Holmström S., and Petersson, K. Franz Lisp VAX-Unix ML/LCF, Chalmers University of Technology, S-41269 Göteborg, Sweden.

[Johnson 75] Johnson, S.C. “Yacc: Yet Another Compiler-Compiler” Technical Report CSTR32, Bell Laboratories, Murray Hill, NJ, 1975.

[Jones & Schmidt 80] Jones, N.D. and Schmidt, S. “Compiler Generation from Denotational Semantics,” in Semantics-Directed Compiler Generation (N.D. Jones, ed.), pp. 70–93, Springer Lecture Notes in Computer Science, Vol. 94 (Berlin, 1980).

[Kini, Martin, & Stoughton 82] Kini, V., Martin, D.F., and Stoughton, A. “Testing the INRIA Ada Formal Definition: The USC-ISI Formal Semantics Project” Proc. ADATec Meeting (1982).

[Marcotty, Ledgard, & Bochman 76] “A Sampler of Formal Definitions,” Computing Surveys 8 (1976), 191–276.

[Mosses 75] Mosses, P.D. “Mathematical Semantics and Compiler Generation,” D. Phil. thesis, Oxford University, 1975.

[Mosses 76] Mosses, P.D. “Compiler Generation Using Denotational Semantics,” Proc. Symp. on Math. Found. of Comp. Sci., Gdansk, 1976, Lecture Notes in Computer Science, Vol. 45, Springer, 1976, 436–441.

[Mosses 79] Mosses, P. “SIS — Semantics Implementation System: Reference Manual and User Guide” DAIMI MD-30, Department of Computer Science University of Aarhus, Denmark (August 1979)

[Paulson 82] Paulson, L. “A Semantics-Directed Compiler Generator,” Conf. Rec. 9th ACM Symp. on Principles of Programming Languages (1982), 224–233.

[Reynolds 75] Reynolds, J.C. “User-Defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction” Conf. on New Directions on Algorithmic Languages, IFIP WG 2.1, Munich, August, 1975.

[Robinson 65] Robinson, J.A. “A Machine-Oriented Logic Based on the Resolution Principle,” J. Assoc. Comput. Mach. 12 (1965), 23–41.

[Sethi 83] Sethi, R. “Control Flow Aspects of Semantics-Directed Compiling” ACM Trans. on Prog. Lang. and Sys. 5 (1983) 554–596.

[Steele & Sussman 78] Steele, G.L. & Sussman, G.J. “The Revised Report on SCHEME,” Mass. Inst. of Tech. Artif. Intell. Memo No. 452, Cambridge, MA (January, 1978).

[Wand 82a] Wand, M. “Semantics-Directed Machine Architecture”

Conf. Rec. 9th ACM Symp. on Principles of Prog. Lang. (1982), 234–241.

[Wand 82b] Wand, M. “Deriving Target Code as a Representation of Continuation Semantics” ACM Trans. on Prog. Lang. and Systems 4, 3 (July, 1982) 496–517.

[Wand 84] Wand, M. “A Types-as-Sets Semantics for Milner-style Polymorphism,” Conf. Rec. 11th ACM Symp. on Principles of Programming Languages (1984), 158–164.

Appendix: A Short Complete Example

; simple applicative language
; define types
(define-type-abbrev fun (-> (seq val cont) ccont))
(define-type-abbrev val (union int fun))
(define-type-abbrev ccont (-> (seq (state)) (ans)))
(define-type-abbrev env (-> (seq ident) val))
(define-type-abbrev cont (-> (seq val) ccont))
; define types for nonterminals
(define-type-abbrev pgm ans)
(define-type-abbrev exp (-> (seq env cont) ccont))
(define-type-abbrev literal ident)
; define opaque types
(define-type-constructor state nil
   literal
   (init-state nil
      (state)
      'the-state-token))
(define-type-constructor ans nil
   literal

(the-ans nil
   (ans)
   'terminate-normally))
(define-type-abbrev ans (ans))
; define auxiliaries
(define-checked init-cont
cont
(lambda (v)
   (lambda (s)
      (block
         (schprint v)
         (terpri)
         the-ans))))
(define-checked init-env
env
(lambda (x) (inL 0)))        ; initially everything is bound to 0
(define-checked ext
(-> (seq env val ident) env)
(lambda (r v id)
   (lambda (id1)
      (if (eq id id1) v (r id1)))))
; now define the transducer
(define sdt
'((yacc-parser 'example.o)
  (pgm
     (pgm exp)
     (e1)
     ((e1 init-env init-cont) init-state))
  (identifier-to-exp
     (exp ident)
     (id)
     (lambda (r k) (k (r id))))
  (ident
     (ident literal)

(id)
id)
(number-to-exp
(exp int)
(n)
(lambda (r k) (k (inL n))))        ; inject into union
(func
(exp 'lparen 'lambda ident exp 'rparen)
(id exp)
(lambda (r k)
   (k (inR
         (lambda (v k1)
            (exp (ext r v id) k1))))))
(appl
(exp 'lparen exp exp 'rparen)
(e0 e1)
(lambda (r k)
   (e0 r
      (lambda (v0)
         (casefn v0        ; branch on case in union type
            (lambda (n)
               (error (list 'cant-apply-number)))
            (lambda (f) ; it was a fcn-- evaluate operand
               (e1 r (lambda (v1) (f v1 k)))))))))))
(define boot
(lambda ()
(define ex (enclose-pf sdt))))
; To load: (load 'example.s)
; To check the sdt: (check-sdt sdt)
; To build the parser: (enclose-yacc sdt 'pgm 'example.o)
; To compile the sdt: (boot)
(define pgm1 '((lambda x x) 0))
(define pgm2 '(((lambda f (lambda x (f x))) (lambda x x)) 3))
; To run an example: (ex pgm2)
; On our VAX, this consumes about .6 sec of CPU time in Lisp, plus a small
; amount of time in pipe-building, running the parser, etc.

; It took about an hour of connect time to get this running-- about
; half an hour for typing in the code and about half an hour for debugging.