Summary: if we are trying to use combinator logic to solve first-order logic type problems, is the best method to feed in free variables and use the standard first-order unification algorithm?

In standard first-order logic, consider the problem of deducing that the following is a contradiction


By the rule that we can substitute specific for general, we can derive


and q & ~q => false.

The particular choice of the constant 5 to substitute for x is obtained using the standard unification algorithm, which in the case of first-order logic is computable (and indeed quite efficient).

Translating this into combinator logic gives

p = K true
~(p 5)

Substituting the value of p gives

~(K true 5)

Evaluating gives


Which is false, QED.

But it doesn't look so good when we try a more complex expression


In standard first-order logic, unification works just as well here as for the simpler case. The translation to CL, however, is

S (K p) (S (K f) f) = K true
~(p (f (f 5)))

This isn't a problem we can solve with simple substitution. One approach we could try is to feed both sides of an equation the same value; if we take the number 5 as a value, the left-hand side of the equation evaluates as

S (K p) (S (K f) f) 5
K p 5 (S (K f) f 5)
p (S (K f) f 5)
p (S (K f) f 5)
p (K f 5 (f 5))
p (f (f 5))

So we have

p (f (f 5)) = K true 5
p (f (f 5)) = true

Substituting into the second expression from the original problem gives


So we have solved the problem, but we did it by guessing the correct value to feed both sides of the equation, by inspection. Is there a general method that could be used?

One that suggests itself is to feed in a variable, which would give

p (f (f x)) = true

From which the standard first-order unification algorithm could be used.

Have we just established that the only way to solve problems in CL is to convert them back into standard logic? Perhaps it's not that bad; at least we have eliminated lambda and the other quantifiers, and their associated bound variables, leaving only free variables.

Still, is there a better method that I'm missing?

(I'm omitting consideration of types here; because combinator logic is Turing complete, presumably type checking will also be needed to avoid the paradoxes of the sort that make simple untyped lambda calculus unsound.)

  • $\begingroup$ Why do you think that "p(x)", a predicate, should be translatable into "p = K true", which declares that p is a function from arbitrary values to true? Or, to make the question more concrete, how would you translate "p(5)"? There may well be a citation here that I'm unfamiliar with, but that would be helpful. $\endgroup$ Jun 25 '11 at 14:31
  • $\begingroup$ cross-posted on MO $\endgroup$
    – Kaveh
    Jun 26 '11 at 0:56
  • $\begingroup$ @kaveh it did not get a good answer there IMO $\endgroup$ Jun 26 '11 at 4:03
  • $\begingroup$ @Jeff, yes, I know, I just added the link for completeness. $\endgroup$
    – Kaveh
    Jun 26 '11 at 4:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.