Juan Rodriguez Hortalá, Teaching Assistant, Universidad Complutense de Madrid, Spain
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 talk we will 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 will show some basic intrinsic properties of the semantics and establish some relationships between them: the three semantics form a hierarchy in the sense of set inclusion, and besides call-time choice and plural semantics enjoy a remarkable compositionality property that fails for run-time choice; finally, we will show how to express plural semantics within run-time choice by means of a program transformation, whose adequacy has been formally proved. To conclude, a prototype developed in the Maude system based on the aforementioned transformation and the natural rewriting on-demand evaluation strategy will be also presented.