search hangs (infinite loop)

[kyagrd]

Here is an example. Used Abella version 2.0.5-dev.

Specification "finite-pic". % two level pic exmaple in abella distro

%% Tiu and Miller 2010 encoding of MPW logic (for late and open)

Kind o'                  type.
Type tt, ff              o'.
Type conj, disj          o' -> o' -> o'.
Type boxMatch, diaMatch  n -> n -> o' -> o'.
Type boxAct, diaAct      a -> o' -> o'.
Type boxOut, diaOut,
     boxInL, diaInL      n -> (n -> o') -> o'.

Define sat : p -> o' -> prop
by sat P ff := false
 ; sat P tt := true
 ; sat P (conj A B) := sat P A /\ sat P B
 ; sat P (disj A B) := sat P A \/ sat P B
 ; sat P (boxMatch X Y A) := X = Y -> sat P A
 ; sat P (diaMatch X Y A) := X = Y /\ sat P A
 ; sat P (boxAct X A) := forall P1, {one P X P1} -> sat P1 A
 ; sat P (diaAct X A) := exists P1, {one P X P1} /\ sat P1 A
 ; sat P (boxOut X A) := forall Q, {oneb P (up X) Q} -> nabla w, sat (Q w) (A w)
 ; sat P (diaOut X A) := exists Q, {oneb P (up X) Q} /\ nabla w, sat (Q w) (A w)
 ; sat P (boxInL X A) := forall Q, {oneb P (dn X) Q} -> exists w, sat (Q w) (A w)
 ; sat P (diaInL X A) := exists Q, {oneb P (dn X) Q} /\ forall w, sat (Q w) (A w)
 .

Theorem aaaaa : forall P X Q,
  {oneb (nu P) (dn X) (y\ nu w\Q w y)} -> exists F, sat (nu P) (diaInL X F).
  intros.
  search. % does not infinit loop

Theorem aaaaa : forall P X Q, nabla (w : n),
  {oneb (nu P) (dn X) (y\ nu w\Q w y)} -> exists F, sat (nu P) (diaInL X F).
  intros.
  case H1.
  search. %%% infinite loop :(

Theorem bbbbb : forall P X Q, nabla w,
  {oneb (P w) (dn X) (y\Q w y)} -> exists F, sat (nu P) (diaInL X F).
  intros.
  search. %%% infinite loop :(

[chaudhuri]

Thanks for the report. I'll take a look at it this evening when I'm back in civilization. There is another report from a while back about looping search that we seem to have forgotten about. I should put it on github so we can track both properly.

[chaudhuri]

As far as I can tell, there is no looping search in this example. The search space is just very branchy, with a branching factor of roughtly 30 per level. This means that at search depth 5 it has to exhaustively check 30^5 or 24.3 million cases. Needless to say that can take some time. You can see the exponential cliff by comparing search 4 against search 5.

What this means is that we need better search bounds. Counting the number of definition unfolding and backchaining steps is too coarse a measure. Perhaps we should also bound the number of branches explored before giving up.

[chaudhuri]

Pinging @thatdalemiller and @robblanco as this may be relevant to some stuff they are doing...

[chaudhuri]

Closing this as not a bug.