Thank you, Michael, it does help. At an operational level, I believe the sharing is broken by a step like this one:
f (S gen_Peano) -> ?_Peano (f (S Z)) (f (S (S _x))).
The left-hand side S is shared, but since the replacement occurs at the operation, f, copies are made. Is it correct?
-Andy
-----Original Message-----
From: curry-bounces_at_lists.RWTH-Aachen.DE [mailto:curry-bounces_at_lists.RWTH-Aachen.DE] On Behalf Of Michael Hanus
Sent: Monday, December 21, 2015 8:47 AM
To: curry_at_lists.RWTH-Aachen.DE
Subject: Re: Pull tabbing with variables
Hi Andy,
the behavior you see is due to the distinction between free variables and generators. Although this distinction is somehow irrelevant from a semantical point of view, it is essential to implement unification of free variables.
For instance, the result of solving the equational constraint
> x =:= (y :: [Bool]) where x,y free
should be just one answer (binding x and y to the same variable) instead of infinitely many results if x and y are handled as generators. Therefore, KiCS2 has a tag for generators which shows whether this generator is a variable or a choice.
Initially, each free variable in the program is tagged as a "variable", but when it is narrowed, the variable tag is replaced by a "choice" tag.
Now, consider your example: Operation g does nothing with its argument, so the tag is not changed. However, operation f narrows its argument, therefore the tag is changed before the actual narrowing takes place. Note that the tag change is not done in place since we compile to Haskell, i.e., other occurrences of y have still the "variable" tag.
Altogether, we obtain two results:
- from g: S y (where the tag on y is not changed)
- from f: Z
Since the REPL checks the tags before printing a choice value, it prints in the first case (S _x2), although the value behind _x2 is a choice.
The actual implementation is a bit more advanced (due to the implementation of encapsulated search), but the basic ideas of this scheme are described in our PADL'13 paper, see
http://www.informatik.uni-kiel.de/~mh/papers/PADL13.html
I hope this explanation was helpful.
Best regards,
Michael
On 12/17/2015 04:00 PM, Andy Jost wrote:
> Consider the following program:
>
>
>
> data Peano = S Peano | Z
>
> f (S Z) = Z
>
> g a = a
>
> main = f x ? g x where x=S y; y free
>
>
>
> KiCS2 produces the correct answers, (S _x2) and Z; my question is
> about how it does so.
>
>
>
> We know KiCS2 will replace y with the generator (S _x) ? Z, and we
> might naively expect f to execute a pull tab step so that f x and g x
> share the expression x = (S (S _x)) ? (S Z). Note that the choice
> arising from the generator is now above S in (the original) x. (I
> ignore the unlikely possibility that we simply got lucky by evaluating
> g x before f x.)
>
>
>
> If the above is accurate, then the program would output (S (S _x)), (S
> Z), and Z. So something else must be going on. I don't recall seeing
> any mention of this issue in the published work about KiCS2.
>
>
>
> Can anyone explain what accounts for this behavior? One theory I have
> is that the shared subexpression is not shared after the pull-tab step.
> That would seem to imply some inefficiency, but Brassel's dissertation
> contains a section on the benefits of sharing subexpressions in KiCS2,
> so I'm not sure.
>
>
>
> Any help is appreciated!
>
>
>
> -Andy
>
>
>
> _______________________________________________
> curry mailing list
> curry_at_lists.RWTH-Aachen.DE
> http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
>
Received on Mi Dez 30 2015 - 12:21:55 CET