Wolfgang and Bernd,
Thanks for your comments. I am leaving for New York, so only a
quick reply.
The program was:
> t = let x free in (f x ? g x)
> f True = success
> g False = success
Wolfganag writes:
> > 1. t -> let x free in f x
> > 2. t -> let x free in g x
> > 3. t -> success ? g (True ? False)
> > 4. t -> f (True ? False) ? success
> >
> > In the narrowing step, I bound the free variable x to (True ?
> > False) rather than only True or only False, because variables
> > may
> > be shared (indeed x is shared in this case).
>
> And this is the point I do not understand. In 3. you have chosen
> to narrow the narrex (f x), which means that x is instantiated to
> True. So if x is shared (as you admit), then the only possible
> reduction is
> 3. t -> success ? g True
> and likewise for 4. By using an independent and unconstrained
> generator (True ? False) for the variable x in (g x) you break
> the sharing.
OK, but now consider adding
f False = failed
The meaning of the program should remain the same, but the step
in question becomes much more plausible.
Bernd writes:
> Just out of curiosity: Why do you call such a step a "narrowing
> step"? What is becoming more narrow by it? My guess is that
> this might be the root of all the misunderstandings in the
> mailing list that people would normally assume that it is at
> least possible that the search space becomes smaller because of
> a narrowing step.
I call it narrowing for lack of better term.
> One point to remark is that it is not feasible to execute steps
> 3 and 4 if your integers are solely given in a primitive
> way. You would have to "narrow" to (0?1?-1?2?-2?...) Do you want
> to do this for functions "f 1 = success" and "g 0 = success"?
This is a good point. I do not know. 0 and 1 should be generated
because they make a difference. Any other value should not
matter.
> I am asking this because it directly relates to your problem as
> one of the very main reasons to have residuation as a language
> construct is the existence of types like integers.
>
> Therefore I see two solutions to this:
>
> a) allow residuation only on such built-in types, e.g., have
> functions
> "ensureInt :: Int -> Int " and
> "ensureFloat :: Float -> Float"
> "ensureIOHandle :: IOHandle -> IOHandle"
> and then live with the incompleteness for such types.
>
> b) suspend also on non-deterministic choices, e.g.
>
> > 3. ... g (True ? False)
>
> does not evaluate any further as g is rigid.
I had not thought about this. On the one hand it looks
consistent, on the other it gievs a reason to have both
variables and non-determinism in a language (as opposed
to either one).
Best,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Nov 09 2007 - 14:37:37 CET