A simple rewrite notion for call-time choice semantics

Non-confluent and non-terminating rewrite systems are interesting from the point of view of programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is not a trivial issue that has been addressed from a semantic point of view in the Constructor-based Rewriting Logic (CRWL) framework. We investigate here how to express call-time choice and non-strict semantics from a point of view closer to classical rewriting. The proposed notion of rewriting uses an explicit representation for sharing with let-constructions and is proved to be equivalent to the CRWL approach. Moreover, we relate this let-rewriting relation (and hence CRWL) with ordinary rewriting, providing in particular soundness and completeness of let-rewriting with respect to rewriting for a class of programs which are confluent i...

• Type: Conference
• Year: 2007
• Where: PPDP
• Authors: Francisco Javier López-Fraguas, Juan Rodríguez-Hortalá, Jaime Sánchez-Hernández
• Keywords: Constructor-based Rewriting Logic, PPDP 2007, Rewrite Systems, Semantics