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.
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.
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".
PutLink SatisfyingSetLink EvaluationLink PredicateNode "breathe" ListLink VariableNode "$X" ConceptNode "air" ConceptNode "animals"
when reduced, will give the EvaluationLink above.
Equivalence to ConceptNode
The above example is equivalent to the
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".
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.
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