Bjorn Lisper wrote:

...

some function argument. For instance, the meaning of the definition

h = let x = f y in g x x

is defined as an abbreviation for the rules

h = aux (f y) aux x = g x x

W.r.t. this semantics, there is no problem even with non-deterministic functions.

How does sharing work here? I assume the "let x = ..." is intended to mean sharing of "...". Does the same hold for function calls in Curry, so "aux x = g x x" implies sharing of x when evaluating g? In that case I

Yes. Since Curry is based on a lazy and (for a particular subclass, namely inductively sequential rules) also optimal evaluation strategy, sharing of function arguments is required and essential.

suspect you might have problems if, for instance, you inline aux naively into g (f y) (f y) and f is nondeterministic. (Inlining should typically work for a referentially transparent language.) The problem can be fixed though: if you have this sharing, then "aux x = g x x" is really shorthand for "aux x = let y = x in g y y". If this definition is inlined and the let is kept (to preserve the sharing), then the transformation should work even if f is nondeterministic.

In the presence of nondeterministic functions (i.e., nonconfluent rules), one has several options for the semantics. For parameter passing, one can use either the call-time choice or run-time choice semantics. Curry is based on the former since there is a well-defined semantical framework for this in the presence of non-strict functions (Gonzalez-Moreno et al., Journal of Logic Programming, Vol. 40, 1999). Semantically, the call-time choice means that rewrite rules can only be applied if the arguments are constructor terms, i.e., totally evaluated. This does not necessarily imply a strict semantics since it can be implemented by lazy reduction provided that function arguments are shared. Thus, this sharing must be somehow represented in an intermediate language for executing the programs and on this level inlining is preserved, as you have remarked. Naive inlining (i.e., without lets but possibly duplicating function calls) does only work for deterministic functions (which is no restriction from a Haskell point of view since Haskell allows only deterministic functions).

I don't know how much of this applies directly to Curry, since the above is for pure term rewriting and I suspect Curry has unification in its evaluation mechanism (right?) which then makes the evaluation more complex. But maybe the above can provide some ideas how to formally define referential transparency for Curry?

The paper mentioned above defines a proof calculus, model theory and operational semantics for this language where the denotation of functions distinguish between deterministic and non-deterministic functions which seems to be conform to your remarks. Although it does not explicitly define referential transparancy, it shows the equivalence of all three notions which I think is enough for reasoning about Curry programs. Nevertheless, many thanks for your hints. Michael