Computational semantics of terms rewriting systems.

*(English)*Zbl 0611.68007
Algebraic methods in semantics, Semin. Fontainebleau/France 1982, 169-232 (1985).

[For the entire collection see Zbl 0568.00021.]

The paper presents a computational approach to building a framework for understanding non-deterministic recursive definitions given by term rewriting systems (TRS). Computations are considered as sequences of consistent sets of redexes, equivalence of computations up to permutations is defined, and the space of computations ordered by extensions up to permutations is shown to be a complete partial order, in which maximal computations generalize the concept of terminating computation. Based on the methods of algebraic semantics, interpretations of TRS are algebras with terms to be computed denoting the least elements, and the semantics of terms under interpretation is defined as the set of results of terminating computations. The paper ends by considering a more restrictive setting so as to present an approach to effective and efficient computational rules. The notion of needed redex is introduced, yielding the subspace of call-by-need computations still being complete, with the structure of coherent algebraic partial orders. It is shown that there is a continuous projection giving from any computation its maximal call-by-need subcomputation, and preserving termination. For a class of sequential systems it is proved that the continuous projection preserves results and hence provides a correct computational rule.

The paper presents a computational approach to building a framework for understanding non-deterministic recursive definitions given by term rewriting systems (TRS). Computations are considered as sequences of consistent sets of redexes, equivalence of computations up to permutations is defined, and the space of computations ordered by extensions up to permutations is shown to be a complete partial order, in which maximal computations generalize the concept of terminating computation. Based on the methods of algebraic semantics, interpretations of TRS are algebras with terms to be computed denoting the least elements, and the semantics of terms under interpretation is defined as the set of results of terminating computations. The paper ends by considering a more restrictive setting so as to present an approach to effective and efficient computational rules. The notion of needed redex is introduced, yielding the subspace of call-by-need computations still being complete, with the structure of coherent algebraic partial orders. It is shown that there is a continuous projection giving from any computation its maximal call-by-need subcomputation, and preserving termination. For a class of sequential systems it is proved that the continuous projection preserves results and hence provides a correct computational rule.

Reviewer: J.Zlatuska

##### MSC:

68Q65 | Abstract data types; algebraic specification |