Equational Programming Topics

Equational programming

Equational programming is the implementation of term rewriting systems with don't care non-determinism against a formal background of algebraic specification with term rewriting as a concrete model.

It is a phrase which was used in the mid eighties (cf. ODO85,DP88) to refer to programming based on equations and equational logic. The name has never caught on, probably because the implementations of the time were suitable only to study equational specifications; not to support programming at large.

Since then, the quality of implementations has increased such, that in many circumstances there is now a real choice between a general purpose language and an implementable specification language: the speed that can be attained using the general purpose language must be weighed against the speed with which an executable specification can be developed.

A compiler for TRS is described in Wal94f References:

The language EPIC

EPIC is an equational programming language that can be used as a `formal systems programming language'.

ARM (and its precursor µArm)

References:

Examples, bits and pieces

Theoretical foundations

Various

Minimal TRSs

I/O in side-effect-free languages

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 have defined 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. References:

Lazy reduction strategy

References:

Hybrid specifications

The problem of insufficient execution speed of equational programming is addressed Wal90 by presenting a formal framework in which implementations based on ground term rewriting 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 incremental 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 Wal89 or Chapter 4 of Wal91). An extended example is shown in Wal90,Wal89,Wal91. In Chapter 5 of Wal91 extensive examples and measurements are presented. References:

© 1998 Babelfish BV