This page summarizes some of the different atom types that play an important role in the pattern matcher, and in atomese in general, with the goal of comparing and contrasting their similarities and differences. There are many different link types that are "dual" to each other, in some way, or perform "opposite" tasks. Others perform similar tasks in "opposite" domains.
Various different atoms deal with the need to determine if some term is present or absent in the atomspace. This table illustrates how these are inter-related.
|GetLink||bound||-||Atom||Use cog-execute! to execute it.|
|SatisfactionLink||bound||-||Crisp TV||Use cog-evaluate! to evaluate it.|
|PresentLink||free||and||TV||"There exists": All of the terms must be present (with at least one grounding).|
|ChoiceLink||free||or||TV||At least one term must be present.|
|AbsentLink||free||-||TV||There must be no grounding of this term.|
|AlwaysLink||free||and||TV||"For all": Every grounding variant must be present.|
|ExistsLink||bound||and||TV||"There exists", declarative form.|
|ForAllLink||bound||and||TV||"For all": declarative form.|
The column indicated "variables" indicates whether or not the link binds its variables. Links that bind their variables can be evaluated or executed outside of the pattern matcher. Links that do not bind their variables can be used to define multi-clause patterns inside of links that do bind their variables.
The column marked "valuation" indicates how the different link types are meant to be valued: this can be either a TV or an atom. Thus, for example, executing a GetLink returns a set of atoms. Evaluating a SatisfactionLink returns a TV.
The primary difference between SatisfactionLink and ExistsLink is that SatisfactionLink can be directly evaluated, to return a crisp true/false value, for whether it can be satisfied with the current AtomSpace contents. By contrast, the ExistsLink is declarative, and is better suited for making declarations of uncertain knowledge, i.e as an anchor point for (uncertain) probabilities.
|GetLink||DualLink||Pattern matching is the task of finding all data that match a particular query. Pattern recognition is the task of finding all queries that match a particular bit of data.|
|MapLink||PutLink||PutLink performs beta-reduction. Maplink can "unput" or un-beta-reduce expressions, extracting values from them, using the supplied pattern template to locate values.|
|TypeProduct||TypeChoice||These implement the concept of product type and sum type in type theory. They correspond to the product and coproduct in the category of sets.|
In some ways, MapLink resembles BindLink; however, MapLink only searches its argument list, while BindLink searches the "entire" AtomSpace (in principle -- it behaves as if it searched the entire AtomSpace. In practice, it never needs to actually do so, and it focuses its search on a very limited set.)
The DualLink is a foundation-stone for chatbots and rule application systems. So for example, in a rule engine, one may have some initial starting point, and one wishes to find all possible rules that might be applicable to that data, that might be applied to that data to transform it. Chatbots behave similarly: given some utterance and the current conversational state, one searches for all possible rules that could be applied to obtain a conversational response. These kinds of searches are very much the opposite of SQL queries or SparQL queries or most normal (graph) database queries.
The DualLink is also a foundation-stone for chainers, forward or backward: as it can be used to find the subset of rules that can be validly applied to obtain the next step of a forward or backward inference. The DualLink implements a search for "what is possible".
Imperative vs. Declarative
There is a mirror symmetry between many link types used to declare knowledge (e.g. using PLN), and the link types used by the pattern matcher to define search-patterns. The general convention is that the PLN link types are "declarative" expressing some fact or state of knowledge, whereas the pattern matcher links are "imperative", and can be "executed" or "run". The distinction here is that the knowledge-representation (PLN) link types assert some fact, and associate that fact with some truth value, usually one or more uncertain probabilistic truth values. Such links "declare" facts.
The pattern matcher link types also differ from the declarative links by typically not binding any variables occurring in them, leaving them free. This allows them to be so assembled together into more complex patterns, and then evaluated at any point in time to obtain crisp true/false values (for that instant in time). They are "imperative" in the sense that they can be "run" to get an answer.
|ImplicationLink||BindLink||P implies Q; if P exists, create Q|
|SatisfyingSetLink||GetLink||What is the set of atoms that satisfy a predicate?|
|-||DualLink||What is the set of predicates that an atom satisfies?|
|EquivalenceLink||DefineLink||What formula or structure defines a predicate?|
|MemberLink||PutLink||An element belongs to a set; add an element to a set.|
|-||MapLink||Extract an element from a structured set (a graph)|
|ExistLink||PresentLink||Does some grouding exist (in the atomspace)?|
|ForAllLink||AlwaysLink||Does every variant grounding exist (in the atomspace)?|
|ChoiceLink||ChoiceLink|| Does at least one element exist (in the atomspace)?
(Menu of A or B; choose either A or choose B.)
|-||RandomChoiceLink||At execution time, pick an element randomly.|
- Note that ChoiceLink works both declaratively and procedurally. Declaratively, it is a menu of items, from which only one can be picked. The concept of a menu is required for linear logic, for the design of vending machines (for a dollar, you can pick only one!), and for the design of mutex locks and semaphores in computing (only one thread can enter a section protected by a semaphore or mutex lock; pick one!).
- The ChoiceLink is not at all like an OrLink! The OrLink, as currently defined in OpenCog, is a boolean operator that operates on predicates. In crisp logic, it is a boolean-or; in axiomatic probability theory (aka measure theory), it corresponds to set union. Neither the Boolean Or, nor the set union adequately capture the concept of choice. However, thanks to Curry–Howard correspondence, choice and boolean-or do "correspond".
- Note that, when taking a naive approach, the RandomChoiceLink does not seem to have a declarative analog: that is because the concept of "pick something now" is inherently anchored in time and space, and, once done, cannot be un-done. However, probabilistic programming does offer a declarative concept of random choice. The idea here is not to "execute" the program (and thus be forced to make a choice), but rather, to perform reasoning on the program: viz: "if I were to make a random choice here, then I would get a probability distribution like this, over there".
- The PutLink behaves a lot like an EvaluationLink, when it is used with DefinedPredicateNodes. See PutLink and EvaluationLink for examples.
- The PutLink behaves a lot like an ExecutionOutputLink, when it is used with DefinedSchemaNodes. See PutLink and LambdaLink for an example.
As noted above, OpenCog, PLN and the atomspace sometimes works with predicates, and sometimes works with atoms. In addition, the AtomSpace also has a fairly rich selection of types and type constructors. Therefore, many of the correspondences noted in Curry–Howard correspondence have an analog, or should have an analog in the AtomSpace.
- Clearly ChoiceLink and TypeChoice correspond between atoms and types; the later is explicitly the sum type of type theory. Both have a classic Curry–Howard correspondence to OrLink.
- We do not yet have an explicit TypeProduct that would be a product type, and correspond to AndLink. But maybe we should. Somewhat painfully-obviously the ListLink is the tuple or Cartesian product that corresponds to AndLink.
- We do have an ArrowLink that is used to define the type of functions. We do NOT have a TensorType, or any kind of tensor product link, which would be needed to capture the adjoint relationship (e.g. tensor-hom adjunction, currying, etc.) The internal language of the tensor categories is linear logic. The Curry–Howard correspondent to the ArrowLink is the ImplicationLink. The wikipedia article on currying describes tensor-hom adjunction in the general setting.
The general situation here is a bit confusing, and needs a more detailed discussion, analysis, and practical hands-on, how-to examples of code that actually works as advertised.
In the meanwhile, here's a provisional table repeating the above:
|ImplicationLink||BindLink||ArrowLink||P implies Q; if P exists, create Q; Given P, return Q.|
|OrLink||ChoiceLink||TypeChoiceLink||A or B is true; pick A or B; its type A or B|
|AndLink||ListLink||TypeProduct||A and B is true; A and B form a pair; product type|
Normally, the correct generalization of there-exists and for-all are arrived at through subobject classifiers and then the sigma and pi types on a pre-sheaf. But we don't really have any of these defined in the atomspace, except sort-of-ish the TypeChoiceLink which corresponds to the sum type, but isn't correctly designed to work as a real sigma type.
In type theory, the dependent type is used to encode there-exists and for-all. We do not have a clearly defined dependent type in opencog.
Dependent types are kind-of-like parametric polymorphism but different.
This is practically important and interesting, since we already have a kind of parametric polymorphism implemented in the /opencog/matrix code base, and the Rcpp bindings for the R language are going to be parametric-polymorphic (if only because that is how R and Rccp are designed.)
We also have some prototype sheaf code in the /opencog/sheaf directory.