Let a term in ski-combinator calculus be called "complete" if every primitive is partially applied (so all S's are applied to at most two arguments, all K's to at most 1, and all I's are not applied).
So for instance:
S(II)I
is not complete, but it can be rewritten as SII
which is complete.
SII(SII)
is not complete and cannot be rewritten in any way to make it complete.
S(K(SII))(S(S(KS)K)(K(SII)))
is complete, but can't be used for much because when applied to any <x>
, it results in a term SII(S(K<x>)(SII))
which is usually incompletable (unless <x>
happens to be something like KI
).
Some complete expressions for arithmetic operations on church numerals:
successor (\x -> x + 1): S(S(KS)K)
addition (\x -> \y -> x + y): SI(K(S(S(KS)K)))
multiplication (\x -> \y -> x * y): S(S(KS)(S(K(SI))(S(KK)(SI(K(S(S(KS)K)))))))(K(K(KI)))
predecessor (\x -> x - 1): S(K(SI(K(KI))))(S(SI(K(S(K(S(K(S(SI(K(KI)))))K))(S(S(SI(KK))(SI(K(KI))))(S(K(S(S(KS)K)))(SI(K(KI))))))))(K(S(SI(KK))(K(KI)))))
(the last one took me a long time to figure out. Basically, start with a pair (true, 0) and then apply n times "if the head is true, change it to false, otherwise add one to the tail" and then at the end extract the tail)
Are there computable operations on church numerals which cannot be expressed as complete terms?
Note: I'm not counting functions like Collatz-length since that's only well defined on a not-known-to-be-computable subset; no skirting the computability requirement by restricting the function to an uncomputable subset of inputs.