Search depth exceeded

[lambdacalculator]

A student wrote a simple recursive addition predicate and used Query to verify 1 + 2 = 3, but failed to find any solution to 1 + 3 = ?. After some initial confusion, I eventually realized that the problem was the search depth, since setting it higher finds these solutions.

Can we avoid this potential confusion by reporting "Search depth exceeded" or something like that when a query fails not because there are no matching rules but because it is limited by search depth? It's the difference between answering "no" (having explored the entire tree) versus answering "I don't know" (because search depth limits further exploration).

[chaudhuri]

Sounds good. Do you want this only for Query and search or for anything that uses implicit search (which includes tactics like apply, backchain, etc.)?

[lambdacalculator]

I can't recall how tactics like apply and backchain report failure to find matches, but my general feeling is that any time an error message is generated when something fails because of a search-depth limitation, then this information should be included in the message. It alerts the user that the tactic might have succeeded with a higher search depth, and so gives a better accounting of the user's options in response to the tactic failure. (Could increasing search depth possibly help, or not?) Thanks.