Sebastian,
Thanks for this attempt. Let me try to formalize it a little more.
> I'll try to sum up the situation:
>
> The semantics of Curry differs from standard term rewriting in the
> presence of non-determinism. In term rewriting, we can safely replace
> variables by their bindings, even if the variables are shared and the
> bindings induce a non-deterministic branching.
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. So, what are we trying to capture here? I think
that we use variables for capturing sharing. In other words, we
are talking of graph rewriting. In graph rewriting a variable is
the label of a node. We use variables in two different ways. In
rewrite rules, variables are "place holders" for any term. In the
graphs to be rewritten, variables are a "notational device" to
express sharing. If we are allowed to represent a graph in other
ways than textually, we might not use variables at all as
notational devices. E.g.;
(not x, not x) where x = True ? false
vs
(,)
/ \
not not
\ /
?
/ \
True False
If we agree that a variable is (the label of) a node, the "binding
of a variable" is the subgraph rooted at that node. There is no
natural or implied replacement. There is the subgraph at the
node. And one could replace the (sub)graph at a node with another
graph, but this is a separate issue.
> In Curry we are not
> allowed to do so because of the call-time choice semantics. On the
> other hand, the distributive properties
>
> f (x?y) = f x ? f y
> (f?g) x = f x ? g x
>
> hold for Curry programs (without encapsulation) but not for term
> rewriting! Consider
Let me try to formalize a bit more this distributive property.
As usual, -*-> denotes zero or more rewriting steps.
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.
> In Curry it is true that the expression
>
> pair (True?False)
>
> has the same results as
>
> pair True ? pair False
>
> namely (True,True) and (False,False). However, in term rewriting, the
> first expression could evaluate to (True,False) and (False,True)
> also. Distributivity does not hold here!
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.
Cheers,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 20 2007 - 18:28:15 CEST