search

ilya-klyuchnikov / sc-mini

SC Mini is a "minimal" positive supercompiler
47 stars 13 forks source link

Nesting let expressions may reveal potential bugs #10

Open gregr opened 7 years ago

gregr commented 7 years ago

Hi, Ilya, thanks for sc-mini! I just finished reading the paper and the source, and noticed some things that didn't make sense to me, which may be unintended. By the way, this issue probably isn't a big deal since let expressions don't seem intended for use in the source language, and so won't appear in nested positions.

I noticed a few places where the handling of let expressions would cause problems if they appeared in nested positions (currently, they are only placed in outer positions during decomposition).

Based on how it's used, vnames should be extracting free variables, so should subtract the let parameter from the names retrieved from the body: https://github.com/ilya-klyuchnikov/sc-mini/blob/71388c1add9e76222564dcc8e4f1367626d1aa0a/DataUtil.hs#L56

I don't think you really want to substitute v' for v in e2' here, since v could legitimately be free in e2'. You really want the behavior you'd get from first substituting the argument for the let-bound parameter in both e2 and e2', then computing the renaming. A more efficient way of getting this would be to prime the renaming with [(v, v')] to ensure that other occurrences of v on the left, indicating that renaming v to anything else should fail; then removing this renaming since v is not actually a free variable in e2: https://github.com/ilya-klyuchnikov/sc-mini/blob/71388c1add9e76222564dcc8e4f1367626d1aa0a/DataUtil.hs#L77

ilya-klyuchnikov commented 7 years ago

Hi Greg, thanks for pointing to this subtlety. Yes, in general case such treatment of let expressions is incorrect (if they were allowed in the source language). But they are introduced only during generalization and hold following properties:

So, bearing in mind the mentioned properties of let expressions, this simple treatment of let expressions is correct.

Feel free to correct me if I am missing something.

On Thu, Sep 14, 2017 at 10:44 PM, Greg Rosenblatt notifications@github.com wrote:

Hi, Ilya, thanks for sc-mini! I just finished reading the paper and the source, and noticed some things that didn't make sense to me, which may be unintended. By the way, this issue probably isn't a big deal since let expressions don't seem intended for use in the source language, and so won't appear in nested positions.

I noticed a few places where the handling of let expressions would cause problems if they appeared in nested positions (currently, they are only placed in outer positions during decomposition).

Based on how it's used, vnames should be extracting free variables, so should subtract the let parameter from the names retrieved from the body: https://github.com/ilya-klyuchnikov/sc-mini/blob/ 71388c1add9e76222564dcc8e4f1367626d1aa0a/DataUtil.hs#L56

I don't think you really want to substitute v' for v in e2' here, since v could legitimately be free in e2'. You really want the behavior you'd get from first substituting the argument for the let-bound parameter in both e2 and e2', then computing the renaming. A more efficient way of getting this would be to prime the renaming with [(v, v')] to ensure that other occurrences of v on the left, indicating that renaming v to anything else should fail; then removing this renaming since v is not actually a free variable in e2: https://github.com/ilya-klyuchnikov/sc-mini/blob/pfp/DataUtil.hs#L77

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ilya-klyuchnikov/sc-mini/issues/10, or mute the thread https://github.com/notifications/unsubscribe-auth/AAQrHJFWc4EqFF4ry4qdFTUlM3s4unMLks5siZ4qgaJpZM4PYOOP .

gregr commented 7 years ago

Nope, that's it. Since it's fresh in my mind, just wanted to point out a few of the more subtle places that, if fixed (along with other less subtle changes), could make it possible to include let expressions in the source language too. It's the kind of code where, if you revisit it after several years, it might be hard to remember where things could go wrong.