[LightMachine]

The search space I'm using is that of all functions of a given dependent type. That allows you to make the search space by using a strong enough type.

For example, if you search for `Integer -> Integer -> Integer` function, it will consider Integers of different bit-sizes. But if you instead search for `∀(n: Nat). Int(n) -> Int(n) -> Int(n)`, you will only consider integers of the same bit-size, which is a much smaller space. You can make arbitrary restrictions to shorten your search.

[YeGoblynQueenne]

So you're enumerating a search space of functions, with some constraints to keep the search tractable?

When you do this kind of thing, there are two worst cases:

a) Your constraints are too strong and the search space does not include the target.

b) The search space includes the target but it is too large to search in polynomial time.

How are you dealing with those?

To clarify, the happy case is when your search target is easy to find, i.e. when the search space is small and includes the target. But that happens... rarely (because program search spaces are large).