search

proofcert / checkers

This is not a game.
3 stars 2 forks source link

Special case for store is breaking the abstraction #4

Closed shaolintl closed 8 years ago

shaolintl commented 8 years ago

Hi Marco,

I have finished the lmf-single and multi focused versions.

The singlefoc version seems to work fine but not so the multifoc.

The reason is as we discussed - the special case of store on line 21 in lmf-singlefoc.mod.

As long as the lower level - singlefoc - generates new nodes, we cannot abstract over it.

Can you think how to write this special case without adding new nodes? This is the only problem as far as I can see with our design.

To use the current branch I am working on:

git checkout delay-fix
./prover.sh ftab1 (works)
./prover.sh ftab1-mf (exactly the same but trying to use the multifoc fpc - does not work)

I believe that if you fix this problem in singlefoc.mod, then both will run properly.

The store I am expecting does not add or remove nodes to the tree...

shaolintl commented 8 years ago

Hi Marco, wait before you start. I need to check something.

shaolintl commented 8 years ago

Hi Marco,

The problem was fixed, you can try now to fix the special rule.

emmevolpe commented 8 years ago

Hi Tomer,

I tried to reconstruct why we needed this special case. I think it was just because for some reason (bug?) we were forced to do strange things during the translation of formulas (you probably remember we discussed that and for a while you also tried to replace teyjus with something else). For example, we were forced to delay negative atoms, which in principle shouldn't be necessary. This special case is thus used to remove such a delay. I.e., when we store a (positively delayed) negative atom, we force the kernel to focus on it immediately after (that's why we modify the tree) so that the delay is removed in the next phase and the (now undelayed) negative atom is properly stored.

The cheapest way of fixing this would be taking this fact into account when we produce (by hand) the evidence, so that this duplication of the node is already in the original tree and we do not need to add anything during the derivation. It's not a neat thing, but in the end it's just a solution to a stupid teyjus problem, I guess, and we can keep it hidden. In a sense, better to keep the fpc clean and rather adjust the evidences... What do you think?

shaolintl commented 8 years ago

I agree. Can you try to modify the example we use right now to fix that? I think that if we just remove the inference rule, the example fails. Can you make the example work without this rule?

emmevolpe commented 8 years ago

Sure. I am trying to make checkers work on my laptop, which I never used before for this. I hope I will manage soon.

emmevolpe commented 8 years ago

The example seems to work now on singlefoc. I will give a further check tomorrow and also produce an example for LMF*.

shaolintl commented 8 years ago

you mean ./runner.sh ftab1-mf is working for you? On my computer it seems not to working, probably because of another problem. I will check it during this weekend.

shaolintl commented 8 years ago

Here you can see the output of the two. At some point they diverge. The storing seems not to happen at the right moment and then instead of a decide, it does or...

output2.txt output.txt

emmevolpe commented 8 years ago

I modified the file ftab1-mf.mod. Still not working.

Looking at the example, I found (at least) a couple of problems:

1) I think that in the -mf example, in the very beginning, the second clause for orNeg_kc (of lmf-singlefoc.mod) was being used instead of the first one. This shouldn't be the case. I modified it so that this clause is now applied only if the list of indexes in the state is non-empty, which is what we want. I.e., I replaced the simple orNegkc C C. with a more complex one. Is it true that if I write [A|B] in lambda-prolog, then I require there is at least one element in the list? If this is the case, we need to do the same for the andNeg. Anyway, now that step seems to work fine.

2) This is probably related to the recursive/non_recursive behavior (as you call it) of the clerxperts. I was not sure and did not want to touch your code too much. But I notice that after the second store in the -mf example, we are left with a root of the tree that is already a multifoc-node (and not a single-foc one), so that the lmf-singlefoc_to_lmf-multifoc shouldn't be needed (at least not in that form).

shaolintl commented 8 years ago

Hi Marco,

you were right, there was a problem there where I did not take into account that even when we recurse on the tree, I need to change back the certificate type to multifoc, then there were a couple of other problems but it is working now.

I created a new branch for lmf-star, please create the example on it..

shaolintl commented 8 years ago

Hi Marco,

I forgot to refer to your point 1. Thank you very much for making the fix. Yes, [A|B] means it is a list with a head and tail and therefore has at least one element. What is the more complex structure we need here?

emmevolpe commented 8 years ago

What I mean by more complex is simply what you find now in the fixed version. " orNegkc C C" did not work because we want this case to be enabled only when lists have at least one element.

emmevolpe commented 8 years ago

I mean: ./prover.sh ftab1

There is no multifocusing. I have only modified the example in order to take care of the delays on the atoms.

On 10/20/2016 11:36 PM, shaolintl wrote:

you mean ./runner.sh ftab1-mf is working for you? On my computer it seems not to working, probably because of another problem. I will check it during this weekend.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/4#issuecomment-255235401, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBDyJewyFurEblHvRNL9G_Cuje7RzJks5q197ogaJpZM4KWXti.

shaolintl commented 8 years ago

I fixed it by then, you can run ./prover.sh ftab1-mf

Do you think you will manage to create the example until Thursday? I will try then to work on the lmf-star.mod file then. I will also add your fix from above to andNeg and then close this issue.

See you on Thursday!

emmevolpe commented 8 years ago

OK. I will check tomorrow. But I have not touched the mf version yet.

On 10/20/2016 11:47 PM, shaolintl wrote:

Here you can see the output of the two. At some point they diverge. The storing seems not to happen at the right moment and then instead of a decide, it does or...

output2.txt https://github.com/proofcert/checkers/files/542969/output2.txt output.txt https://github.com/proofcert/checkers/files/542970/output.txt

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/proofcert/checkers/issues/4#issuecomment-255237697, or mute the thread https://github.com/notifications/unsubscribe-auth/AQoBD4wfCzySoo1XdZAWAwAS6tz-iK_Aks5q1-FsgaJpZM4KWXti.