"Francisco Javier López Fraguas" <fraguas_at_sip.ucm.es> writes:
> Michael Hanus wrote:
>
>>However, an implementation is free to do some optimizations,
>>e.g., inlining, constant propagation, partial evaluation,
>>or omitting eta-expansion so that reductions can be done earlier.
>
> Removing eta expansion is not merely an optimization,
> but has subtle semantic consequences in presence of non-determinism.
Depends on what semantics you choose for that non-determinism.
> The following is a well-known example for the CRWL (Toy) community:
[example deleted]
> So, I strongly recommend to eliminate in the Curry report the paragraph
> mentioned by Wolfgang. Otherwise the report will not correspond to the behavior
> of the system.
We think it doesn't matter, as Curry semantics should be preserved
under extensionality.
Umm, this may be a good moment (using your example) to write down some
concerns we have about the semantics of non-determinism.
As your example showed, current non-determinism in FLP doesn't
preserve program semantics in simple cases like:
coin = 0
coin = 1
let x = coin in (x,x)
!=
(coin,coin)
[Note that Sloth indeed can spot such simple cases and fix them, but
it doesn't work in general, with eta-expansion and so on.]
We dislike semantics where this is not preserved, so perpetuating this
kind of behavior is not a path we'd like to follow,
Of course, getting our desired semantics is not easy goal to achieve,
but we are actively working on it.
> Wrt HO patterns, I will be glad if the FLP community adopt more
> widely the CRWL approach for HO.
I'm not really sure about this either, nor the status of function
patters in Curry.
Handling predicates by name may be OK as noted in [1], (and IMO it was
quite hard to get it right and doesn't cover all the cases) but
definitively doing the same for functions as data is not OK. Just see
the simple example:
id1 = \x -> x
id2 = \x -> x
gu id1 = 1
gu id2 = 2
This destroys any semantics based on mapping Curry functions to their
mathematical counterpart. It is my understanding (from reading the
docs, sorry I didn't have yet time to actually try it) that this is
the current behavior, both in packs and Toy.
The approach of just profiting from the Prolog translation of partial
applications to do some kind of HO matching is IMVHO not the path to
follow. Just see how big the list of problems for it is in the Toy
report, and we are not trying yet to proof some fancy semantics
properties.
Getting HO right is hard. Lambda-Prolog is the closest I know of, and
they do need HO unification for a start.
Regards,
Emilio
[1]
_at_inproceedings{DBLP:conf/asian/CabezaHL04,
author = {Daniel Cabeza and
Manuel V. Hermenegildo and
James Lipton},
title = {Hiord: A Type-Free Higher-Order Logic Programming Language
with Predicate Abstraction.},
booktitle = {ASIAN},
year = {2004},
pages = {93-108},
ee = {
http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3321{\&}spage=93},
crossref = {DBLP:conf/asian/2004},
bibsource = {DBLP,
http://dblp.uni-trier.de}
}
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Mär 30 2007 - 10:48:22 CEST