Search hangs

[lambdacalculator]

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]

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]

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

Can you elaborate on this?

[chaudhuri]

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]

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]

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]

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.