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