Linearity Requirement for Patterns

[Michael Hanus]

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