Incomplete introduction of parameters after elimination (when containing Props)

mwleeds / epigram

Automatically exported from code.google.com/p/epigram

0 stars 0 forks source link

Incomplete introduction of parameters after elimination (when containing Props) #74

Closed GoogleCodeExporter closed 8 years ago

GoogleCodeExporter commented 8 years ago

Cf. test/BugLetLambda.pig.

I would expect that, in a programming problem, all parameters are introduced. 
Right now, the engine would stop introducing them when we hit a parameter of 
type (x : :- blah) with a "sufficiently complicated" blah.

Original issue reported on code.google.com by pedag...@gmail.com on 2 Sep 2010 at 1:22

GoogleCodeExporter commented 8 years ago

That test case doesn't seem to be in the main tree. Please can you darcs push 
it?

I couldn't reproduce this, but discovered that amusing things can happen if one 
of the parameters to a programming problem is a proof that the propositional 
simplifier can discover...

Original comment by adamgundry on 3 Sep 2010 at 7:38

GoogleCodeExporter commented 8 years ago

Thanks for pushing BugLetLambda.pig.

The simplification rule for |ALL s ABSURD| was just wrong. Moreover, using de 
Bruijn indices in the propositional simplifer is dangerous: we must remember to 
increment them when bringing a term under a binder. There may be other similar 
issues remaining.

We also now retain more name advice, at the cost of losing knowledge that 
certain functions are constant after simplification. Name advice in problem 
simplification needs more work: BugLetLambda.pig now shows three hypotheses 
losing their names.

Original comment by adamgundry on 6 Sep 2010 at 9:50

Changed state: Fixed

GoogleCodeExporter commented 8 years ago

The main patch fixing this issue is

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100906094243-e29d1-a
c86262baaf8280118e38a41536766e3fc134a85.gz

I have now also changed problem simplification to retain name advice for 
propositional hypotheses that simplify to a single proposition, in patch

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100906100925-e29d1-a
731bbed967b5eea361e3d2334e207efe0b3093d.gz

Original comment by adamgundry on 6 Sep 2010 at 10:14

GoogleCodeExporter commented 8 years ago

Another related fix:

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100909092151-e29d1-c
2056110662801cc172958bf0468bcb6960505ae.gz

Original comment by adamgundry on 9 Sep 2010 at 9:36