ForAllLink

From OpenCog
Jump to: navigation, search

The ForAllLink is a type of Link is a type of Link used to represent universal quantification.

For example, ∀x.(if x eats haggis then x gets sick) is written as

ForAllLink
     VariableNode $X
     ImplicationLink
         EvaluationLink eats ($X, haggis)
         InheritanceLink $X sick

ForAllLink and ExistsLink are both subtypes of ScopeLink, that is, they bind any variables occurring under the link, so that those variables are not free. So, in the above example, the variable $X is not a free variable.

The AlwaysLink is a form of ForAllLink which does not bind it's variables, but keeps them free. This allows the AlwaysLink to be composed with other links having the same variable names, so as to form more complex patterns. Likewise, PresentLink is the non-binding form for ExistsLink.

Keeping this in mind, the above is equivalent to

LambdaLink
     VariableNode $X
     AlwaysLink
        ImplicationLink
            EvaluationLink eats ($X, haggis)
            InheritanceLink $X sick

See the link comparison chart for further discussion.