A problem I had with this discussion is that it was not clear
(to me) which is Sergio's answer (or preferred answer, if there are more
than one) to his starting question:
Given the following program:
test = 1+x ? zero x where x free
zero 0 = 0
what should the evaluation of test produce?
Disregarding secondary (imho) aspects related to residuation,
the example was accurately examined from the point of view of
'classical' Curry (coinciding also with Toy/CRWL view) by Michael and Wolfgang.
I do not see anything problematic with the example, as far as
one is concerned with individual results corresponding to different
alternative computations.
After the first messages it seemed to me that Sergio suggested
the following computation
test
-> 1+x ? zero x where x free
-> {x->0} 1+0 | {x->0} 0
-> {x->0} 1 | {x->0} 0
as a right and complete computation
(complete in the sense that there was no need
of considering other computations).
Since in my view that computation is semantically right
(narrowing at any position is sound, but may lose answers;
the computation strategy is responsible of not losing answers)
but uncomplete, I sent my example
f 0 = 0
g 1 = 1
goal: f x ? g x where x free
which, according to my thoughts about Sergio's thoughts,
would lead to different results depending on which expression
(f x or g x) was reduced first. Apparently by his reply,
also Bernd was thinking in this direction.
Bernd's answer, agreed by Sergio, introduced generators to replace
free variables, thus replacing narrowing over the free variables by evaluation
of the generators. If I'm not wrong, the use of generators (in the sense of
papers by Sergio&Michael, Bernd and myself) do not change the set of ground
values that can be obtained from an expression (more precise statements
can be found in the three papers, with proofs
corresponding to different formal settings).
Therefore, nothing essentially different
(from the point of view of individual computed values) is
obtained from generators, except some possible loss in the generality of
answers.
which can be seen only as a minor problem, in particular if generators ease
some approaches to implementation.
Personally, I prefer to maintain the possibility of genuine free variables
to be narrowed in the classical sense (although respecting call time choice,
as in our wlp2007 paper).
In any case, the use of generators/rewriting to replace free variables/narrowing
does not need any new theory nor formal setting (this doesn't mean that
nothing interesting can be investigated).
Existing formalisms (CRWL and its
rewriting-with-let-bindings counterpart --see our ppdp07--, or the operational
semantics of JSC mentioned by Michael) cope perfectly with generators,
which conceptually are not different from any other function, as happens
also with the function ?.
I don't think that giving to generators or to ? a special
status from the point of view of the semantics (intended or formal) is a real
need,
not even an advantage.
A different question is the interest of developing an operational procedure
where computations produce set of values, instead of individual ones.
This is interesting in many aspects, has been addressed several times,
and might profit of a sage usage of generators combined with ?, as it seems
you are working out in your recent papers.
But I don't think that this needs changing the foundations of FLP.
Instead, in my opinion such collecting procedures should guarantee
equivalence with the semantics given to individual computations in previous
proposals (CRWL, JSC, ppdp07).
This was done for instance, for CRWL and the set-valued semantics in our
lpar01/flops02 papers.
As a final remark, I support Michael's idea of giving to Curry a CRWL-based
declarative
semantics and replace the present operational
description of Curry based on disjunctive expressions by a new one
specifying individual computations and at the same time respecting call-time
choice
(an issue not well covered in the report).
JSC semantics and/or let-rewriting/narrowing of our ppdp07/wlp07 papers
are good candidates.
Sorry for the very long message and best regards,
Paco
----- Original Message -----
From: "Sergio Antoy" <antoy_at_redstar.cs.pdx.edu>
To: <bbr_at_informatik.uni-kiel.de>
Cc: <curry_at_lists.RWTH-Aachen.DE>
Sent: Monday, November 05, 2007 7:06 PM
Subject: Re: Intended meaning
> Bernd Brassel schrieb:
>
>> Sergio Antoy schrieb:
>> > 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.
>>
>> Could it be that the semantic model you have in mind is that of
>> _confluent_ rewriting? That you want to embed the non-confluence of
>> non-deterministic functions into a confluent system with special
>> treatment of the non-deterministic choice?
>
> Not exactly. The semantics of non-determinism we intend in Curry
> is such that computations are confluent (except for the order and
> timing in which non-deterministic alternatives are produced), but
> here I see the problem as an interaction between order of
> evaluation, sharing and non-deterministic choices. The meaning of
>
> (f x ? g x where x free)
> as
> (f x where x free) ? (g x where x free)
>
> makes sense. Unfortunately, the language syntactically allows the
> first form and I am afraid one cannot catch all the variations of
> this problem at compile time. Giving the intended semantics
> statically might be quite difficult.
>
>> This would enlighten your comment:
>>
>> > 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.
>>
>> and also your reply, to Michael's example:
>>
>> > 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).
>
> In my opinion, this is mostly or only related to the order of
> evaluation. I am thinking about the opportunities that massively
> parallel computations would offer. Hence I do not want to count
> too much on any specific order.
>
>> Making such non-standard narrowing steps is implemented in kics, since
>> mapping to functional programs means that you have to map to a confluent
>> system. And, unfortunately, we couldn't add the additional constraint
>> "since x is shared" which would make many computations in kics much more
>> efficient.
>
> Well... 10 years ago (in my ALP 1997 paper), I defined a narrowing
> step as a two-part process in which part 1 is just an
> instantiation and part 2 is plain rewriting. The most general
> instantiation is a generator. I think this is a simple and
> general way to look at narrowing that is useful for both theory
> and implementations.
>
> Why you could not add the constraint that x is shared? I
> discussed this a bit with Sebastian, when he was here, but it was
> not detailed enough. I understand that you map kics to
> haskell. If the mapping of kics expressions into haskell
> expressions is the identity (or close to it), then controlling
> sharing might be difficult or impossible. But I would guess that
> there are other mappings that satisfactorily abstract sharing.
>
> Cheers,
> Sergio
> _______________________________________________
> curry mailing list
> curry_at_lists.RWTH-Aachen.DE
> http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
>
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Di Nov 06 2007 - 14:23:58 CET