Separability and translatability of sequential term rewrite systems into the lambda calculus


Orthogonal term rewrite systems do not currently have any semantics other than syntactically-based ones such as term models and event structures. For a functional language which combines lambda calculus with term rewriting, a semantics is most easily given by translating the rewrite rules into lambda calculus and then using well-understood semantics for the lambda calculus. We therefore study in this paper the question of which classes of TRS do or do not have such translations. We demonstrate by construction that forward branching orthogonal term rewrite systems are translatable into the lambda calculus. The translation satisfies some strong properties concerning preservation of equality and of some inequalities. We prove that the forward branching systems are exactly the systems permitting such a translation which is, in a precise sense, uniform in the right-hand sides. Connections are drawn between translatability, sequentiality and separability properties. Simple syntactic proofs are given of the non-translatability of a class of TRSs, including Berry's F and several variants of it.