10.4230/LIPICS.FSTTCS.2008.1764
Rodriguez-Hortala, Juan
Juan
Rodriguez-Hortala
A Hierarchy of Semantics for Non-deterministic Term Rewriting Systems
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2008
Functional-logic programming
term rewriting systems
constructor-based rewriting logic
non-determinism
call-time choice semantics
run-time choice
Hariharan, Ramesh
Ramesh
Hariharan
Mukund, Madhavan
Madhavan
Mukund
Vinay, V
V
Vinay
2008
2008-12-05
2008-12-05
2008-12-05
en
urn:nbn:de:0030-drops-17643
10.4230/LIPIcs.FSTTCS.2008
978-3-939897-08-8
1868-8969
10.4230/LIPIcs.FSTTCS.2008
LIPIcs, Volume 2, FSTTCS 2008
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
2013
2
4
328
339
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Hariharan, Ramesh
Ramesh
Hariharan
Mukund, Madhavan
Madhavan
Mukund
Vinay, V
V
Vinay
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2008
2
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
443661 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
Formalisms involving some degree of nondeterminism are frequent in computer science. In particular, various programming or specification languages are based on term rewriting systems where confluence is not required. In this paper we examine three concrete possible semantics for non-determinism that can be assigned to those programs. Two of them --call-time choice and run-time choice-- are quite well-known, while the third one --plural semantics-- is investigated for the first time in the context of term rewriting based programming languages. We investigate some basic intrinsic properties of the semantics and establish some relationships between them: we show that the three semantics form a hierarchy in the sense of set inclusion, and we prove that call-time choice and plural semantics enjoy a remarkable compositionality property that fails for run-time choice; finally, we show how to express plural semantics within run-time choice by means of a program transformation, for which we prove its adequacy.
LIPIcs, Vol. 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, pages 328-339