- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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=

e.

Any help is appreciated!

-Andy

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

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

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=

e.

Any help is appreciated!

-Andy

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

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

*
This archive was generated by hypermail 2.3.0
: Mo Feb 06 2023 - 07:15:14 CET
*