- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Francisco J. Lopez Fraguas <fraguas_at_sip.ucm.es>

Date: Tue, 06 Nov 2007 12:53:15 +0100

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

Date: Tue, 06 Nov 2007 12:53:15 +0100

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

_______________________________________________

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

*
This archive was generated by hypermail 2.3.0
: Sa Okt 01 2022 - 07:15:06 CEST
*