search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Search hangs #118

Open lambdacalculator opened 5 years ago

lambdacalculator commented 5 years ago

In an earlier version of Abella, the searches in this (small) theorem completed almost instantly with the witnesses indicated in the comments. Now they hang, or at least take more time than I was willing to wait. comb.zip

chaudhuri commented 5 years ago

Related to #117.

The reasons for this is that search has moved the exponential search space around since it changed the order of depth-bounded search. We may have to add the old style back and give the current one a different name such as eager_search. I don't know a good answer yet.

yvting commented 5 years ago

... search has moved the exponential search space around since it changed the order of depth-bounded search.

Can you elaborate on this?

chaudhuri commented 5 years ago

Abella used to do iterative deepening by exploring search depth 1 fully before trying depth 2, then 3, then 4, etc.

During @robblanco's PhD, he was experimenting with running bits of the ProofCert kernel inside Abella. He found it more useful if Abella would skip full exploration of depths 1..k-1 if the initial depth bound was k (which is 5 by default). This means that search would be much faster in cases where there isn't a lot of branching or proofs of different lengths. This is also how Teyjus and essentially every other logic programming interpreter works.

However, this also means that Abella doesn't find the shortest proof first -- for example, there may have been a depth 3 proof on a different path Abella will spend a long time exploring the depth 5 space on the branch it's currently on.

yvting commented 5 years ago

Can you point to me the commit that introduces this change? Is it before v2.0.5 or after?

What I noticed is that there is huge performance decrease from v2.0.5 to v2.0.6 on the example provided by Todd. If the change you mentioned is not introduced between v2.0.5 and v2.0.6, then it is likely not relevant to the performance decrease. I suspect the performance decrease is caused by the new heuristics I implemented for searching for type-generic proofs.

chaudhuri commented 5 years ago

Ah, no, I was talking about a change from before 2.0.5. If this is a regression in 2.0.6 then it's not what I'm thinking of.

yvting commented 5 years ago

Here is what I find out after some investigation using the provided example.

The performance decrease seems to be caused by the combination of

  1. Performance decrease in unification because of the introduction of type unification and backtracking

  2. An unusually large amount of calls to unification in a single search which significantly magnifies the previous performance decrease

I added code to track the average runtime and the number of calls to relevant functions in the implementation of "search". I then run the modified code on "comb.thm" up to the first search.

For v2.0.5, there are

Num of calls to try_right_unify_cpairs: 2901528 Num of calls to claus_aux: 515434 Average time to run clause_aux: 0.001095 Average time to run try_right_unify_cpairs: 0.000198

For the master branch, there are

Num of calls to try_right_unify_cpairs_fully_inferred: 2901528 Num of calls to claus_aux: 515434 Average time to run clause_aux: 0.005483 Average time to run try_right_unify_cpairs_fully_inferred: 0.000990

So there are about 5 times of performance decrease for a single call to try_right_unify_cpairs. However, because there is a huge amount of calls to this function, the performance decrease is magnified significantly.

The thing I don't understand is why there are so many calls to clause_aux for a single search. Is this related to the change Kaustuv mentioned?

Edit: The clause_aux function is defined in the search function in "tactics.ml". It performs backchaining on program clauses, in this process it calls try_right_unify_cpairs (or try_right_unify_cpairs_fully_inferred after the introduction of schematic polymorphism) for unification.