After trying without success for several days to find a proper software/website that can correctly simplify lambda terms (see this question), I ended up deciding to use JavaScript to do the same. The primary code that I set up was this. However, when I tried to create a function that checks whether a Church-encoded numeral is divisible by another and returns a Church boolean as a result, I came into a problem.
The lambda function I created was a sort of recursive combinator like this: $$rec:=\lambda{abf}.greaterThanOrEqual(a)(b)(\,f(subtract(a)(b))(b)(f)\,)(isZero(a))$$ $$isDivisible:=\lambda{mn}.rec(m)(n)(rec)$$ My idea was this: to check if $m$ is divisible by $n$, subtract $n$ from $m$ and repeat this till the result is less than $n$. At that time check if the result is $0$. If it is zero, then return True, else return False. Now the problem I ran into was this: JavaScript is not a lazy compiler, so it decided to solve the recursive part first and got locked into a series of infinite $\beta$-reductions, with no $\beta$-normal form in sight. However, if the compiler had decided to try each recursion step before the entire simplification, it would have reduced the term to a normal form.
So my problems are:
Is the recursive combinator I have written correct? That is, does it truly check divisibility?
If it is correct, can anyone suggest a better option for software based lambda term simplification? That is, I will just write the lambda terms and they will be simplified to normal forms (if possible)
