Latex Maths

Sunday, February 12, 2012

unification = the calculus of concepts

Today I just had an insight:

Haskell Curry proposed combinatory logic as a logica universalis, but it ran into inconsistency problems.  (I'm trying to use fuzzy-probabilistic truth values to get around that problem, but that's a different topic.)

So, in 1963 JA Robinson discovered resolution, which is really unification + propositional resolution.  Unification decides if 2 terms can be made equationally identical.  Propositional resolution deals with the "calculus of thinking" at the proposition level.

Combinatory logic provides a free way to compose terms via "application".  I regard terms as concepts.  For example:
   "tall handsome guy"
is the combination of the concepts
   tall ∙ (handsome ∙ guy).

Now, a few examples:
"tall handsome guy" is equivalent to "handsome tall guy";
"very tall guy" implies "tall guy";  but
"very tall guy" does not equal "tall very guy";

Thus the unification theory is modulo some special rules akin to commutativity, associativity, etc, and certain reduction rules.  In other words, unification modulo a theory = "the calculus of concepts".

So we have a neat decomposition:
    calculus of thoughts = calculus of concepts
                                    + calculus of propositions

No comments:

Post a Comment