<p><strong>Summary</strong>: 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?</p>

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

<pre><code>p(x)
~p(5)
</code></pre>

<p>By the rule that we can substitute specific for general, we can derive</p>

<pre><code>p(5)
~p(5)
</code></pre>

<p>and q &amp; ~q => false.</p>

<p>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).</p>

<p>Translating this into combinator logic gives</p>

<pre><code>p = K true
~(p 5)
</code></pre>

<p>Substituting the value of p gives</p>

<pre><code>~(K true 5)
</code></pre>

<p>Evaluating gives</p>

<pre><code>~true
</code></pre>

<p>Which is false, QED.</p>

<p>But it doesn't look so good when we try a more complex expression</p>

<pre><code>p(f(f(x)))
~p(f(f(5)))
</code></pre>

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

<pre><code>S (K p) (S (K f) f) = K true
~(p (f (f 5)))
</code></pre>

<p>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</p>

<pre><code>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))
</code></pre>

<p>So we have</p>

<pre><code>p (f (f 5)) = K true 5
p (f (f 5)) = true
</code></pre>

<p>Substituting into the second expression from the original problem gives</p>

<pre><code>~true
</code></pre>

<p>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?</p>

<p>One that suggests itself is to feed in a variable, which would give</p>

<pre><code>p (f (f x)) = true
</code></pre>

<p>From which the standard first-order unification algorithm could be used.</p>

<p>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.</p>

<p>Still, is there a better method that I'm missing?</p>

<p>(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.)</p>

CC BY-SA 3.0
2011-06-25T14:31:47.960Z
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.
Rob Simmons
CC BY-SA 3.0
2011-06-26T00:56:34.123Z
[cross-posted on MO](http://mathoverflow.net/questions/41686/combinator-logic-and-unification)
Kaveh
CC BY-SA 3.0
2011-06-26T04:03:23.480Z
@kaveh it did not get a good answer there IMO
Jeff Atwood
CC BY-SA 3.0
2011-06-26T04:11:13.720Z
@Jeff, yes, I know, I just added the link for completeness.
Kaveh
<lo.logic>
Combinator logic and unification
rwallace
# Combinator logic and unification

(Asked by: username_0 on 2010-10-07)

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
p(x)
~p(5)

By the rule that we can substitute specific for general, we can derive
p(5)
~p(5)

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
~true

Which is false, QED.
But it doesn't look so good when we try a more complex expression
p(f(f(x)))
~p(f(f(5)))

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
~true

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.)

**Tags:** lo.logic

> **Comments:**
> **username_1**: 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.  
> **username_2**: [cross-posted on MO](http://mathoverflow.net/questions/41686/combinator-logic-and-unification)  
> **username_3**: @kaveh it did not get a good answer there IMO  
> **username_2**: @Jeff, yes, I know, I just added the link for completeness.  

---

## 0 answers

