Re: Pull tabbing with variables

From: Michael Hanus <mh_at_informatik.uni-kiel.de>
Date: Wed, 30 Dec 2015 12:21:41 +0100

Hi Andy,

yes, in principle, you are right. To be more precise:
Since gen_Peano should be matched (against Z by definition of f),
it is replaced by "?_Peano Z (S _x)" so that a further pull-tab
step yields the step you described. By evaluating gen_Peano
and processing both results with f, the sharing is broken.

Best regards,

Michael

On 12/24/2015 07:32 PM, Andy Jost wrote:
> 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
>>
>
>
>

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Wed Dec 30 2015 - 12:23:28 CET

This archive was generated by hypermail 2.3.0 : Thu Sep 19 2019 - 07:15:09 CEST