A flexible framework for programming with non-deterministicfunctions

摘要

The possibility of non-deterministic reductions is a distinctive feature of some declarative languages. Two semantics commonly adopted for non-determinism are call-time choice-- a notion that at the operational level is related to the sharing mechanism of lazy evaluation in functional languages-- and run-time choice, which corresponds closely to ordinary term rewriting. But there are practical situations where neither semantics is appropriate, if used in isolation. In this paper we propose to annotate functions in a program with the semantics most adequate to its intended use. Annotated programs are then mapped into a unified core language (but still high level), designed to achieve a careful but neat combination of ordinary rewriting --to cope with run-time choice-- with local bindings via a let-construct devised to express call-time choice. The result is a flexible framework into which existing languages using pure run-time or call-time choice can be embedded, either directly --in the case of run-time choice-- or by means of a simple program transformation introducing lets in function definitions --for the case of call-time choice--. We prove the adequacy of the embedding, as well as other relevant properties of the framework.