Linearity Requirement for Patterns

[Bjorn Lisper]

Michael Hanus:
>In Curry, each defining equation contributes to the semantics
>of a function independently of the other equations for the same
>function, and the overall goal is to compute all values of
>an expression (plus possible substitutions for free variables)
>which can be derived from this equational reading of all rules.
>In this sense, Curry is refentially transparent (although I have
>no formal definition of this notion but only soundness, completeness
>and optimality results). Your "counter example" comes from a
>misunderstanding of the "let" in Curry. Since the kernel language
>is based lazy evaluation w.r.t. a set of constructor-based rewrite
>rules, the "let" is considered as syntactic sugar for abbreviating
>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
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.

If, on the other hand, Curry has a call-by-name semantics, then the direct
inlining should work.

>If you have a precise definition of "referentially transparent"
>at hand so that you can make your statement more precise, I would
>be very interested to read it. As you have seen, the slogan
>"replacing equals by equals" is still to fuzzy since just looking
>for equality symbols in a language is not sufficient.

Referential transparency is defined w.r.t. some notion of equality on terms,
and cannot be precise unless this notion is made precise. If the language at
hand has a denotational semantics, then equality on terms can be derived
from their denotations. But referential transparency can also be defined
w.r.t. other semantics. An interesting case is term rewrite semantics: a
confluent term rewrite system defines a notion of equality through its
convertibility relation (the transitive-reflexive-symmetric closure of the
reduction relation). A notion of referential transparency can be based on this
equivalence relation (which is an equality relation, due to closedness of
the reduction relation under substitutions and taking of contexts).

A restricted notion of referential transparency carries over to nonconfluent
(and thus nondeterministic) rewrite systems. If the rewrite system can be
partitioned into a confluent and a nonconfluent part, then the
convertibility relation for the confluent part can be taken as an equality
relation upon which the referential transparency can be defined.  Under
certain (not so strong) technical conditions, the set of possible normal
forms will be the same for terms that are equal w.r.t. this convertibility
relation. This holds also if the concept of normal form is extended to cover
infinite and possibly diverging computations.

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?

Björn Lisper

PS. I have a paper on this. There is also a paper by Søndergaard and Sestoft
that has an interesting discussion about referential transparency and
nondeterminism. Bibtex entries are given below.


@STRING{tcs = "Theoret.\ Comput.\ Sci."}

@ARTICLE{Lisper-TCS,
	AUTHOR = {Bj{\"o}rn Lisper},
	TITLE = {Computing in Unpredictable Environments: Semantics, Reduction Strategies, and Program Transformations},
	JOURNAL = tcs,
	YEAR = {1998},
	VOLUME = {190},
	NUMBER = {1},
	PAGES = {61--85},
	MONTH = jan
}
@ARTICLE{SonSes-reftrans-unfold,
	AUTHOR = {Harald S{\o}ndergaard and Peter Sestoft},
	TITLE = {Referential Transparency, Definiteness and Unfoldability},
	JOURNAL = {Acta Informatica},
	YEAR = {1990},
	VOLUME = {27},
	PAGES = {505--517}
}