Re: Intended meaning

From: Sergio Antoy <>
Date: Fri, 02 Nov 2007 15:38:45 -0700 (PDT)

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.

curry mailing list
Received on Fr Nov 02 2007 - 23:48:23 CET

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:09 CEST