Unrolling closures into SAT boolean formula

Question

I need to verify some assertions about the minimalist Turing-complete language Jot.

Many of the assertions I want to investigate are semi-deciable (co-recursively enumerable). So far it's been fairly straightforward to literally enumerate every Jot program via its Goedel number and testing the assertion's complement by running a Jot program with a given space/time bound.

This works great for small programs (< ~40 bits) and has allowed me to find the shortest known representations of several standard simple functions from lambda calculus.

SUCC = J(18400)
CHURCH_0 = J(154)
CHURCH_1 = J(0)
CHURCH_2 = J(588826)
IS_ZERO = J(5)
MUL = J(280)
EXP = J(18108)
S = J(8)
K = J(4)
AND_2 = J(16)
AND_3 = J(139248)
OR_2 = J(9050)

However, this is particularly inefficient for larger functions and I'd like to speed up searches using a SAT solver. To do this requires unrolling the recursion of a Jot program J(n) to a predefined hard cut-off depth as a boolean formula.

Technically the formula isn't of polynomial length, but is still practically useful due to the small constants in program length and an already known existing polynomial number of beta reductions in an equivalent (but verbose) implementation of the target J(n).

I'm used to encoding problems in SAT formulae, however the new issue for me is understanding how to encode closures (nested functions) in an efficient manner.

None of the standard tools for bounded model checking that I know of allow nested anonymous functions, so I haven't been able to study any existing encoding methods. I would greatly appreciate any hints about how to encode these closures.

Here's the Jot interpreter written in Python which I'm trying to unroll into a boolean formula:

def S(x): return lambda y: lambda z: x(z)(y(z))
def K(x): return lambda y: x
def X(x): return x(S)(K)
def B(x): return lambda y: lambda z: x(y(z))
def I(x): return x
def J(n): return (B if n & 1 else X)(J(n >> 1)) if n else I

Answer 1

It's important to remember that SAT can only encode problems that are in $NP$, unless you use more than polynomial-length formulas. I'm not 100% sure, but I'm doubting your problem is in $NP$.

Consider the following function:

$F = \lambda x\ y \ldotp x x (\lambda y . y y)$

Now consider evaluating $F F (\lambda z \ldotp z)$.

This clearly runs forever, but we can also see that the argument given as $y$ will grow exponentially with the number of $\beta$ reductions you do.

Now, some things that aren't clear from the question:

non-deterministically represented candidate program

What does this mean? Is the program non-deterministic? Or its representation? What even is a non-deterministic representation?

static once created and have a small number of predefined variables within each combinator

Again, what does this mean? My example doesn't seem to fit this, but if whatever you're dealing with us Turing Complete, my gut says your problem is likely to be $EXPTIME$-hard.