Pull tabbing with variables

From: Andy Jost <Andrew.Jost_at_synopsys.com>
Date: Thu, 17 Dec 2015 15:00:56 +0000

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 na=
ively expect f to execute a pull tab step so that f x and g x share the exp=
ression x = (S (S _x)) ? (S Z). Note that the choice arising from the ge=
nerator is now above S in (the original) x. (I ignore the unlikely possibi=
lity 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 ment=
ion of this issue in the published work about KiCS2.

Can anyone explain what accounts for this behavior? One theory I have is t=
hat the shared subexpression is not shared after the pull-tab step. That w=
ould seem to imply some inefficiency, but Brassel's dissertation contains a=
 section on the benefits of sharing subexpressions in KiCS2, so I'm not sur=

Any help is appreciated!


curry mailing list
Received on Mo Dez 21 2015 - 17:47:13 CET

This archive was generated by hypermail 2.3.0 : Mi Okt 21 2020 - 07:15:04 CEST