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||-||TV||Use cog-evaluate! to evaluate it.|
|PresentLink||free||and||TV||All of the terms must be present.|
|ChoiceLink||free||or||TV||At least one term must be present.|
|AbsentLink||free||?||TV||Term must be absent.|
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.
|GetLink||DualLink||Pattern matching is the task of finding all data that match a particular pattern. Pattern recognition is the task of finding all patterns 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.|
Note that MapLink resembles BindLink; however, MapLink only searches its argument list, while BindLink searches the entire atomspace.
Imperative vs. Declarative
There is a mirror symmetry between many link types used by PLN, and the link types used by the pattern matcher. The convention is that the PLN link types are "declarative", whereas the pattern matcher links are "imperative". The distinction here is that the PLN link types assert some fact that is meant to hold; the truth of that fact is given a valuation by the associated TV: the PLN links "declare" facts. The pattern matcher link types are instead transformations to be applied: when the pattern matcher runs, the application of an "imperative" link type causes something to happen.
|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)|
|ForAllLink (?)||PresentLink||Do all of the elements exist (in the atomspace)?|
|ExistsLink (?)||ChoiceLink||Does at least one element exist (in the atomspace)?|
|ChoiceLink||ChoiceLink||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".
- It is probably wrong to say that ExistsLink is a declarative form of ChoiceLink. Currently, ExistsLink is defined to act only on predicates, viz, to state "there exists an $x for which P($x) is true". By contrast, ChoiceLink is saying "you can choose $x because it is on the menu of things that exist". Both are saying something about existence, but in different ways.
- 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. Therefor, many of the correspondences noted in Curry–Howard correspondence have an analog, or should have an analog in the AtomSpace. Exactly what these are remains a bit confusing, and needs to be clarified.
- 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 have a ForAllLink and an ExistsLink, but these only work for predicates, and not for atoms. We have a procedural PresentLink, but we do not have a declarative form of this. That is, the AtomSpace provides a way to say "there exists an atom $x such that P($x) is true": that is what ExistsLink does. We currently do not have a way of saying "there exists an atom A($x) for some other atom $x (that exists)". However, the PresentLink does allow us to say "find me all the atoms A($x) when some other atom $x exists".
- 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. I wrote the wikipedia article on currying which describes the tensor-hom thing 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, provisional table repeating he 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|
|ExistsLink||? ChoiceLink ?||?||Existential quantification|
|ForAllLink||? PresentLink ?||?||Universal quantification|
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.