Paco writes:
> Is it related to the property that C[e ? e'] should be
> equivalent to C[e] ? C[e'], for any context C and expressions e,
> e' ?
At the level of this discussion "equivalent" should be clarified.
Informally (to avoid any specialized semantics) I would guess that
any value derived from the first can be derived from the second
and vice versa. The difficulty is to clarify what "to derive"
means, see below.
> I remark that the property is certainly true for CRWL
> programs.
I believe that CRWL ignores residuation, which was the ONLY
problem in my original posting.
> An interesting point is that the proof of it is easy
> if one uses semantic-based reasonings.
The proof is easy in other settings, too, depending on the
notion of "equivalence".
> Thus, an operational procedure can use the above equivalence
> while preserving the semantics.
I agree completely. My concern is reversing this principle, i.e.,
we have an operational procedure, e.g., backtracking, and we
define a semantics to comply with the operational procedure. My
understanding is that we do not yet have a semantics for the
following problem: a variable is shared by the arguments of a
choice and the variable residuate in one argument whereas narrows
in the other.
Backtracking over the choice does not even see the sharing. Is
this the semantics we desire? Other operational procedures, which
might be more efficient and/or more complete, see the sharing.
We semantics should they comply with?
Cheers,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Nov 08 2007 - 09:17:26 CET