Thanks again for all the replies. It looks like we have different
notions of what can or needs to be evaluated to obtains all the
results of a computation. This can be partly due to the semantics
or models we have in mind. E.g., Wolfgang thinks functions
whereas I think rewrite rules. With a different model, maybe some
steps that I would like to perform are not justified.
I do not want to get into semantic models, thus, I am dropping
again this issue. I am only answering the still-pending questions
that my message generated.
------------------------------------------------------------------
Bernd referring to Paco's example asks:
> Why does the problem have to do with residuation? Why is 1 still
> a result if you decide to reduce (f x) first?
the example being
f 0 = 0
g 1 = 1
f x ? g x where x free
When a variable is shared, a narrowing step must instantiate the
variable with a generator, not only with the cases of the function
that is narrowing the variable. In this particular example, x
should be narrowed to 0 ? 1 exactly as Bernd shows. The type
integer is not algebraically defined, thus here the choice of 0
and 1 needs would require some explanation.
Michael's example is another case in point.
> f True _ = True
> g False = False
>
> and the expression (f x (g x)). If you reduce the narrex (g x),
> you cannot obtain the normal form True.
Since x is shared it should be narrowed to (True ? False).
------------------------------------------------------------------
Both Michael and Wolfgang mention "outermost" to refer to the
steps of the strategy. Note that an outermost strategy cannot be
complete for the class of the constructor-based rewrite systems.
Thus, it is not obvious why a non-outermost step should be
prohibited. Even more so if it is needed.
Cheers,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Nov 02 2007 - 23:48:23 CET