# Re: Confused Students

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Thu, 21 Jun 2007 12:15:24 +0200

Dear Sergio,

thanks for your reply. It reminds me to use articulate statements in
order to not being misunderstood.

> In term rewriting, there are no variables in a term being
> rewritten. A variable would be treated as an irreducible constant
> or a nullary constructor. In term rewriting there are variables
> in rewrite rules. Replacing these variables would change the
> rewrite system.

I referred to variables in rewrite rules. But with 'replacing
variables' I didn't mean to change the rewrite system. When a rule of
a term rewrite system is applied, the variables in the right-hand
side of this rule are replaced by other terms. I think the source of
confusion is that my examples uses variables that are arguments of
functions while yours uses variables that are defined in a local
declaration. Before I comment on your formalization and graph
rewriting, let me point out differences between local and top-level
declarations in Curry:

Wolfgang wrote:

> Would you accept the following reformulation?
>
> | If "u = x?y" is a (desugared) program rule
> | (as opposed to a (derived) semantic equation),
> | then t[v \ u] = t[v \ (x?y)] holds as a semantic equation,
> | otherwise the substitution rule holds only for values,
> | or for expressions having the same SINGLE values.
>
> It tries to make explicit how program rules,
> which are used as rewriting rules,
> connect the two worlds....

Here, "program rules" should mean "rules on top-level" because as you
can see from the examples introduced by Sergio, local declarations
behave differently. For example the following two Curry programs have
different semantics:

program 1:

pair = (x,x)
x = True ? False

program 2:

pair = (x,x)
where
x = True ? False

I consider this counter intuitive.

Now back to the formalization of distributivity:

> Let R be a term (or graph) rewriting system or a Curry program.
> We say that the distributive property holds for R iff
> for every unary symbol f, terms x and y, value v, and context C[],
>
> C[f (x?y)] -*-> v iff C[f x ? f y] -*-> v.

At first, I considered this a good formalization, but now I noticed
that it holds neither in term rewriting nor in graph rewriting (but
in some sense in Curry).

> With my proposed definition, the distributive property does not
> hold for Curry programs and graph rewriting. I would conjecture
> that it holds for every term rewriting system.

Here is a counter example:

pair x = (x,x)

Now, we have

pair (True?False) -> (True?False,True?False) -> (True,True?False) ->
(True,False)

in other words: pair (True?False) -*-> (True,False), i.e., the left
part of the equivalence holds for

f = pair, x = True, y = False, v = (True,False) and an empty context C

The corresponding right part of the equivalence is

pair True ? pair False -*-> (True,False)

which is wrong. As a conclusion, distributivity as you defined it
does not hold for term rewriting.

For completeness, lets observe that your example is indeed a counter
example for the distributive law in graph rewriting. Here, we choose
f as the first 'not', x as True and y as False and the context C as
the surrounding expression:

(not z, not z) where z = True ? False

The only values of this expression are (True,True) and (False,False).
The right part of the equivalence is now:

(not True, not z) ? (not False, not z) where z = True ? False

which has more results. If we link both non-deterministic choices and
restrict them to choose the same alternative in every computation,
then the law holds. This observation is familiar to those who are
aware of a new natural semantics for Curry which is unfortunately not
yet published.

In the context of Curry, your equivalence is not applicable to

(not z, not z) where z = True ? False

as there is no function application of the form f (x?y) in this
expression. This textual understanding of the rule ensures that the
argument of f cannot be shared somewhere else in the context C.
However, there is no Curry semantics (besides graph rewriting) that
allows such expressions -- usually only normalized expressions are
allowed.

If we agree that

f z where z = (x?y)

is not a Curry expression of the form 'f (x?y)', then the
distributive property as you defined it holds for Curry programs.

I tried to reformulate the property such that it holds for graph
rewriting too but did not get to an elegant definition yet.

I'd like to see a definition that is satisfied or Curry and graph
rewriting but not for term rewriting because I think the distributive
law characterizes call-time choice semantics. Curry and graph
rewriting have call-time choice semantics while term rewriting has not.