SatisfyingSetLink

From OpenCog
Jump to: navigation, search

The SatisfyingSetLink is used to convert a predicate to a concept. That is, given a predicate that expresses truth, the SatisfyingSetLink is used to declare the set of all things that satisfy that predicate: that set becomes a new concept.

More formally, it is used to bind free variables occurring in an expression. Any item or items that can ground or satisfy the bound variables is, by definition, a member of the satisfying set. The SatsifyingSetLink is essentially identical to the GetLink, except that the SatisfyingSetLink is declarative, and GetLink is imperative. That is, the execution of GetLink can be forced by calling the cog-execute! function, which then returns a SetLink of all of the items currently in the AtomSpace that satisfy it.

In its most common, frequent usage, SatsifyingSetLink is used with an EvaluationLink; it will connects a PredicateNode to a ConceptNode, by means of an EquivalenceLink. See the section on EquivalenceLink, below. Since satisfying sets are sets, their members can be declared with the MemberLink.

Because all atoms in the AtomSpace carry a truth value, the concept of a predicate in OpenCog is more general than that of a predicate in first-order logic. it is more closely akin to an characteristic function in probability theory, or a classifying topos in mathematical logic.

General form

The general form of the SatisfyingSetLink is

  SatisfyingSetLink
     <optional variable declarations>
     <predicate containing free variables>

The SatisfyingSetLink will then bind all of the free variables occurring in the predicate expression.

At this time, PLN does not allow the optional variable declaration; thus, the current semantics are that all free variables occurring in the predicate are implicitly bound.

Example

An example:

 SatisfyingSetLink
   EvaluationLink
     PredicateNode "breathe"
     ListLink
       VariableNode "$X"
       ConceptNode "air"

specifies the indicator function "things $X that breathe air". The use of the SatisfyingSetLink here indicates that variable $X occuring in the EvaluationLink is the bound variable for this expression. This then allows set membership to be indicated as follows:

 MemberLink
   ConceptNode "animals"
   SatisfyingSetLink
     EvaluationLink
       PredicateNode "breathe"
       ListLink
         VariableNode "$X"
         ConceptNode "air"

which states that "animals" belong to the set of "things $X that breath air". The above can be understood to be a beta redex, and, by applying beta-reduction, it can be reduced to the much smaller and simpler constant expression:

  EvaluationLink
     PredicateNode "breathe"
     ListLink
       ConceptNode "animals"
       ConceptNode "air"

which just states that "animals breath air".

Note that MemberLinks resemble PutLinks in reverse order. The PutLink is the normal way of writing a beta redex in the AtomSpace; it is imperative, whereas the MemberLink is declarative. Thus,

 PutLink
   SatisfyingSetLink
     EvaluationLink
       PredicateNode "breathe"
       ListLink
         VariableNode "$X"
         ConceptNode "air"
   ConceptNode "animals"

when reduced, will give the EvaluationLink above.

PLN

In PLN, the MemberToEvaluationRule will perform the beta reduction, while the the EvaluationToMemberRule will perform the inverse operation.

Equivalence to ConceptNode

The above example is equivalent to the

 ConceptNode "the-set-of-all-things-that-breathe-air"

This equivalence can be made formal by using the EquivalenceLink: by asserting that the following is true:

 EquivalenceLink
   ConceptNode "the-set-of-things-that-breath-air"
   SatisfyingSetLink
     EvaluationLink
       PredicateNode "breathe"
       ListLink
         VariableNode "$X"
         ConceptNode "air"


This defines a new ConceptNode "the-set-of-things-that-breath-air" in terms of two previously existing ConceptNodes: those for "breath" and "air".

Truth values

By default, the SatisfySetLink binds all free variables in an expression. So, in the above EvaluationLink examples, the variable $X occurs "freely" (by the standard definition of "free"). Syntactically, the only thing that SatisfyingSetLink is doing in this example is to declare that $X is a variable, i.e. its binding it, so that $X is now "bound". That is, SatisfyingSetLink is acting just as lambda. Since it doesn't "do anything" except convert free to bound, the TruthValue (the "strength" and "confidence") of this should not be in dispute: thus, it should have (stv 1 1).

However, in the PLN interpretation, this is not the case: all atoms, including the satisfying set, are implicitly scoped over the universe of all things, and clearly, not all things breath air. Thus, the truth value on the SatisfyingSetLink will not be (stv 1 1), but will be considerably weaker.

Consider again the example above, this time with explicit truth values indicated:

 EquivalenceLink
   ConceptNode "the-set-of-things-that-breath-air" <TV1>
   SatisfyingSetLink  <TV2>
     EvaluationLink <TV3>
       PredicateNode "breathe"
       ListLink
         VariableNode "$X"
         ConceptNode "air"

In the PLN interpretation, one has that <TV1> == <TV2> == <TV3> and that all three truth values are small, given that most things don't breath. Very roughly, <TV> == "probability that something breaths air", which is low. To get high probabilities, use the ContextLink; the Contextlinks provide a way of encoding conditional probabilities; thus P(breathes air | animal) = 1.0; that is, the probability that something breathes air, conditioned on the prior that it is an animal, is 1.0, since all animals breathe air.

Variable declarations

At this time the declaratively-equivalent GetLink allows explicit variable declarations and type restrictions. Such explicit variable declarations, for the SatisfyingSetLink, are not currently supported in the current implementation of PLN.

Thus, for example, the following declares that the variable $X is not only bound, but that it's type must be restricted only to ConceptNodes. Again, although the below is conceptually valid, its is not currently supported by PLN.

  SatisfyingSetLink
       TypedVariableLink
            VariableNode $X
            TypeNode "ConceptNode"
       InheritanceLink 
            VariableNode $X 
            ConceptNode Famous@45678