OpenCogPrime:VariableAndCombinatorNotation

From OpenCog
Jump to: navigation, search

Variable and Combinator Notation

One of the most important aspects of combinatory logic, from a OCP perspective, is that it allows one to represent arbitrarily complex procedures and patterns without using variables in any direct sense. In OCP, variables are optional, and the choice of whether or how to use them may be made (by OCP itself) on a contextual basis.

This page deals with the representation of variable expressions in a variable-free way, in a OCP context. The general theory underlying this is well-known, and is usually expressed in terms of the elimination of variables from lambda calculus expressions (lambda lifting). Here we will not present this theory but will restrict ourselves to presenting a simple, hopefully illustrative example, and then discussing some conceptual implications.

Why Eliminating Variables is So Useful

Before launching into the specifics, a few words about the general utility of variable-free expression may be worthwhile.

Some expressions look simpler to the trained human eye with variables, and some look simpler without them. However, the main reason why eliminating all variables from an expression is sometimes very useful, is that there are automated program-manipulation techniques that work much more nicely on programs (schemata, in OCP lingo) without any variables in them.

As will be discussed later (e.g. in the chapter on evolutionary learning, although the same process is also useful for supporting probabilistic reasoning on procedures), in order to mine patterns among multiple schema that all try to do the same (or related) things, we want to put schema into a kind of "hierarchical normal form." The normal form we wish to use generalizes Holman's Elegant Normal Form (which is discussed in Moshe Looks' PhD thesis) to program trees rather than just Boolean trees.

But, putting computer programs into a useful, nicely-hierarchically-structured normal form is a hard problem — it requires one have a pretty nice and comprehensive set of program transformations.

But the only general, robust, systematic program transformation methods that exist in the computer science literature require one to remove the variables from one's programs, so that one can use the theory of functional programming (which ties in with the theory of monads in category theory, and a lot of beautiful related math).

So: In large part, we want to remove variables so we can use functional programming tools to normalize programs into a standard and pretty hierarchical form, so we can mine patterns among them effectively.

However, we don't always want to be rid of variables, because sometimes, from a logical reasoning perspective, theorem-proving is easier with the variables in there. (Sometimes not.)

So, we want to have the option to use variables, or not.

An Example of Variable Elimination

Consider the PredicateNode

AND
  InheritanceLink X cat
  eats X mice

Here we have used a syntactically sugared representation involving the variable X. How can we get rid of the X?

Recall the C combinator, defined by

C f x y = f y x

Using this tool,

InheritanceLink X cat

becomes

C InheritanceLink cat X

and

(eats X) mice

becomes

C (eats) mice X

so that overall we have

AND
  C InheritanceLink cat
  C eats mice

where the C combinators essentially give instructions as to where the virtual argument X should go.

In this case the variable-free representation is basically just as simple as the variable-based representation, so there is nothing to lose and a lot to gain by getting rid of the variables. This won't always be the case — sometimes execution efficiency will be significantly enhanced by use of variables.

Standard Approaches to Variable Elimination

Combinatory logic is of course the standard tool for eliminating variables in programs, but apparently a variety of approaches are used by logicians to eliminate variables in quantified statements, which may or may not be of interest to OCP in the future; the Wikipedia:Predicate_functor_logic article lists many such approaches.