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.
I need to think about this some more..
Cheers,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Jun 21 2007 - 12:27:31 CEST