Rewriting and Call-Time Choice: The HO Case

It is known that the behavior of non-deterministic functions with call-time choice semantics, present in current functional logic languages, is not well described by usual approaches to reduction like ordinary term rewriting systems or -calculus. The presence of HO features makes things more difficult, since reasoning principles that are essential in a standard (i.e., deterministic) functional setting, like extensionality, become wrong. In this paper we propose HOlet-rewriting, a notion of rewriting with local bindings that turns out to be adequate for programs with HO non-deterministic functions, as it is shown by strong equivalence results with respect to HOCRWL, a previously existing semantic framework for such programs. In addition, we give a sound and complete notion of HOlet-narrowing, we show by a case study the usefulness of the achieved combination of semantic and reduction notions, and finally we prove within our framework that a standard approach to the implementation of HO ...

• Type: Conference
• Year: 2008
• Where: FLOPS
• Authors: Francisco Javier López-Fraguas, Juan Rodríguez-Hortalá, Jaime Sánchez-Hernández
• Keywords: Automated Reasoning, FLOPS 2008, HO Features, HO Non-deterministic Functions, Non-deterministic Functions