H.R.Walters and J.F.Th.Kamperman
We present {\sc EPIC}, an equational programming language: its abstract syntax, static and operational semantics, and one of many possible concrete grammars of unconditional {\sc EPIC}.
J.F.Th.Kamperman and H.R.Walters
A simple, efficient and correct compilation technique for left-linear Term Rewriting Systems (TRSs) is presented. TRSs are compiled into {\em Minimal Term Rewriting Systems} (MTRSs), a subclass of TRSs, presented in \cite{KW95d}. In MTRSs, the rules have such a simple form that they can be seen as instructions for an easily implementable abstract machine, the {\em Abstract Rewriting Machine} (ARM). In the correctness proof, it is shown that the MTRS resulting from compilation of a TRS simulates neither too much ({\em soundness}) nor too little ({\em completeness}), nor does it introduce unwarranted infinite sequences ({\em termination conservation}). The compiler and its correctness proof are largely independent of the reduction strategy.
Bibliography: KW96 Available as: CS-R9605.ps.Z
J.F.Th.Kamperman and H.R.Walters
Formally well-founded compilation techniques for Term Rewriting Systems (TRSs) are presented. TRSs are compiled into {\em Minimal Term Rewriting Systems} (MTRSs), a subclass of TRSs in which all rules have an extremely simple form. A notion of simulation of (rewrite) relations is presented, under which an MTRSs can be said to simulate a TRS. The MTRS rules can be directly interpreted as instructions for an extremely simple Abstract Rewriting Machine (ARM). Favourable practical results have already been obtained with an earlier version of ARM.
Bibliography: KW95d Availble from: CS-R9573.ps.Z
J.F.Th.Kamperman and H.R.Walters
Existing models for I/O in side-effect free languages focus on functional languages, which are usually based on a largely deterministic reduction strategy, allowing for a strict sequentialization of I/O operations. In concurrent logic programming languages a model is used which allows for don't care non-determinism; the sequentialization of I/O is extensional rather than intensional. We apply this model to equational languages, which are closely related to functional languages, but exhibit don't care non-determinism. The semantics are formulated as constrained narrowing, a relation that contains the rewrite relation, and is contained in the narrowing relation.We present constrained narrowing and some of its properties; a constructive method to transform conventional term rewriting systems to constrained narrowing systems; and a discussion on requirements for an implementation.
Bibliography: KW95c Availble from: CS-R9572.ps.Z
H.R.Walters and H.Zantema
We present three term rewrite systems for integer arithmetic with addition, multiplication, and, in two cases, subtraction. All systems are ground confluent and terminating; termination is proved by semantic labelling and recursive path order.The first system represents numbers by successor and predecessor. In the second, which defines non-negative integers only, digits are represented as unary operators. In the third, digits are represented as constants. The first and the second system are complete; the second and the third system have logarithmic space and time complexity, and are parameterized for an arbitrary radix (binary, decimal, or other radices). Choosing the largest machine representable single precision integer as radix, results in unbounded arithmetic with machine efficiency.
Bibliography: WZ95
J.F.Th.Kamperman and H.R.Walters
We call a compiler {\em bootstrapped} when it is able to compile its own source. To achieve this situation, the compiler must be expressed in its own language, and an initial interpreter or compiler for this language must be available.We describe the tools and techniques used for the bootstrapping of the new ASF compiler, which is itself expressed in ASF+SDF. As initial compiler, the previous version of the ASF compiler, ASF2C, and the meta-environment are used.
Both as a case-study in the manipulation of algebraic specifications, and as case-study in software-engineering of a portable compiler, the project is interesting to the ASF+SDF community.
Bibliography: KW95
J.F.Th.Kamperman and H.R.Walters
This version was published in RTA.
(See also)
Bibliography: KW95b
C.-T. Buehl, T.B. Dinesh, J.F.Th. Kamperman and H.R. Walters
(See also)
Bibliography: fSDL
J.F.Th.Kamperman, T.B.Dinesh and H.R.Walters
The design and implementation of the language fSDL (full Structure Definition Language) is discussed. In fSDL, complex user-defined data types such as lists, tables, trees, and graphs can be constructed from a tiny set of primitives. Beyond mere structure definitions (also offered by previously existing tools) high-level functionality on these data types can be specified. In the COMPARE (ESPRIT) project, the C code generated from an fSDL specification is used by compiler-components running in parallel on a common data pool. fSDL is first translated into a sublanguage, {\em flat} fSDL, from which the actual C code is produced. {\em Flat} fSDL is a convenient interface for cooperation with other compiler generation tools. There is a formal relation between the input fSDL and the resulting flat form.
Bibliography: KWD94
H.R.Walters and J.F.Th.Kamperman
A hybrid interpreter for code for the abstract rewriting machine is presented. The interpreter reads a \uarm\ program and one or more subject terms, and normalizes the terms using that program. The program is internally stored in a way optimized for efficiency.The interpreter accepts a set of external functions, which may implement basic data types (such as integers or floating point numbers), but which may also be compiled versions of \uarm\ function definitions. In this way the interpreter can process mixed compiled and interpreted code; a technique sometimes referred to as `melting ice technology' (for static crystalline compiled code and fluid interpreted code). We refer to this capability as {\em hybrid}.
Bibliography: WK94
H.R.Walters
(See also)
Bibliography: Wal94e
H.R.Walters
Aslib is a software tool which provides library facilities for the algebraic specification language ASF+SDF. ASF+SDF is a modular language which does not support parameterization. This is overcome by providing {\em renamings}, where an imported virtual module acting as formal parameter is renamed (rather than bound) to some actual module.Aslib enhances software reuse in two manners: firstly plain modules become more easily reusable due to the possibility of renaming sorts and functions, and secondly parameterized modules (and hence datatypes) become available by renaming imported modules and their local sorts and functions.
Bibliography: Wal94b
H.R.Walters
A compiler for ASF+SDF, and a hybrid interpreter for the generated code are presented.In \cite{KW93} an abstract rewriting machine (called ARM) was described which aimed at efficient term rewriting. The major shortcoming recognized in ARM, was the fact that it was implemented by a mapping to C. That is, a TRS was translated to ARM code, and then to C code, and then (using a C compiler) to executable object code. In addition, the C code consisted of a single (huge) function. This situation required a time consuming C compilation phase for every change to the TRS.
For \uarm\ a different approach is taken: its code is made suitable for interpretation, and it is modular. Hence, the C compilation (which used to take 90\% of the compilation time) is avoided, and in addition local changes to the TRS only require re-compilation of one, or a few modules.
The \uarm\ interpreter is constructed in such a manner that functions which are expected to remain stable can be compiled to machine executable functions (via C or otherwise), and can be linked to the interpreter to be executed instead of an interpreted function definition. This technique of a combination of compiled and interpreted code is sometimes referred as `melting ice technology'. The same mechanism used for linking in compiled functions can also be used to access functions which perform actions that are inexpressible in a TRS, such as IO.
Since a running system may in general have both interpreted and compiled functions, the interpreter is called {\em hybrid}.
Bibliography: Wal94f
H.R.Walters
We present a calculus which defines an operational semantics of applicative conditional term rewriting. Since the application of a rule (i.e., the one step reduction relation) is expressed in a single (conditional) rewrite rule, this definition is reflexive. We extend the calculus to allow for higher-order functional objects (not higher-order matching), and to allow for explicit, user-definable reduction strategies.We sketch how this calculus can be implemented using a conditional first-order applicative term rewriting implementation.
Bibliography: Wal94d
This article is available as rat.ps. An older article with related but different ideas is hot.ps.
H.R.Walters
We present a calculus which defines an operational semantics of applicative conditional term rewriting. Since the application of a rule (i.e., the one step reduction relation) is expressed in a single (conditional) rewrite rule, this definition is reflexive. We extend the calculus to allow for higher-order functional objects (not higher-order matching), and to allow for explicit, user-definable reduction strategies.We sketch how this calculus can be implemented using a conditional first-order applicative term rewriting implementation.
Bibliography: Wal94a
H.R.Walters
Bibliography: Wal94c
J.F.Th.Kamperman and H.R.Walters
We define {\em Lazy Term Rewriting Systems} and show that they can be realized by local adaptations of an {\em eager} implementation of conventional term rewriting systems. The overhead of lazy evaluation is only incurred when lazy evaluation is actually performed.Our method is modelled by a transformation of term rewriting systems, which concisely expresses the intricate interaction between pattern matching and lazy evaluation. The method easily extends to term {\em graph} rewriting. We consider only left-linear, confluent term rewriting systems, but we do not require orthogonality.
H.R.Walters
We present a term rewriting system for decimal integers with addition and subtraction. We prove that the system is confluent and terminating.
Bibliography: Wal94 Availble from: Wal94.ps.Z
J.F.Th.Kamperman
GEL (Graph Exchange Language) is a formalism for the compressed exchange of (term) graphs between processes. Key features of GEL are speed, compactness, independence of readers and writers, and compositionality. Typically, GEL representations of large, tree-like graph structures require an average of a little more than one byte storage for representing one node in the graph. Orthogonally to GEL, other protocols can be used to exchange data residing in the nodes of a graph. An algebraic specification of the semantics of GEL texts is given, as well as performance measurents of an experimental C library for GEL. The C library (including an example) can found at ftp://ftp/cwi.nl/pub/gipe/sources/GEL.tar.Z
H.R.Walters and J.F.Th.Kamperman
A formal specification is presented of a cross section of a Cosy system. The formalism used is ASF+SDF. The specification illustrates parts of the Data Model, parts of an Intermediate Language and a small Cosy Engine.In this document a formal specification of the functional behavior of several parts of a Cosy system is presented. This specification is created in order to investigate the merits of the ASF+SDF meta-environment for such a purpose, and in order to guide the ongoing discussion on the IR, the DMCP and Cosy. This specification is not specifically intended to serve as (the start of) a design of the ultimate Cosy environment.
Roughly, the specification contains four parts: basic modules, the data model, the intermediate representation and an engine. We will present these parts in some detail, and then we will formulate some considerations and conclusions.
Bibliography: WK93
J.F.Th.Kamperman and H.R.Walters
Term rewriting is frequently used as implementation technique for algebraic specifications. In this paper we present the abstract term rewriting machine (ARM), which has an extremely compact instruction set and imposes no restrictions on the implemented TRSs. Apart from standard conditional term rewriting, associative lists are supported. ARM code is translated to (ANSI) C; the resulting execution speeds are good (on a sun4, an average of 80000 rewriting steps per second and a maximum of 416000 r/s were measured). Several benchmarks are given, and related work is discussed in depth.
J.F.Th.Kamperman and H.R.Walters
(See also)
Bibliography: KW93a
H.R.Walters
Bibliography: Wal91 Availble from: Wal91.ps.Z
H.R.Walters
The problem of insufficient execution speed of implementations of algebraic specifications is approached by presenting a formal framework in which implementations based on term rewriting [3] can be combined transparently with implementations based on conventional programming languages. This hybrid method can be used for the implementation of parameterized datatypes, where the formal parameter may have a formal signature and where the actual parameter may be implemented in either fashion. The hybrid method permits later addition of equations over datatypes implemented in this fashion, and allows for non-canonical terms to have an `internal representation'. The correctness of the hybrid method can be established (it is completely covered in [6]). An extended example is shown. Measurements done on a prototype suggest a gain of a factor five in execution speed.
Bibliography: Wal90
H.R.Walters
(See also)
Bibliography: Wal89
H.R.Walters
In this chapter we give a specification of the abstract syntax and static semantics of the parallel object oriented programming language POOL. .AE .NH 1 "Introduction" POOL is an acronym of Parallel Object Oriented Language and it refers to a family of languages developed at Philips Research Laboratories in Eind\%hoven. The language used in this chapter is the language POOL-T as defined in [Ame85] (with some minor alterations). We will refer to this language simply as POOL.
Bibliography: Wal89a
L.G.Bouma and H.R.Walters
In this chapter we introduce the concept of execution of algebraic specifications based on term rewriting systems and give an overview of some existing (semi-)automatic implementation methods.
Bibliography: BW89
L.G.Bouma and H.R.Walters
(See also)
Bibliography: BW87
H.R.Walters
(See also)
Bibliography: Wal86a