Request to add links specification as the single source of truth

[stellarspot]

The problem of the current AtomSpace project implementation is that there is no one single document which describes links behavior.

For example it is possible to change PutLink behavior in code so if it has ListLink argument and ListLink has an executable atom inside and if the result of execution of the atom is SetLink then only the first element of the SetLink is used (See #2307). Such change is declared only in code.

Usually computer languages have specification that describes how the language constructions should behave. If there are differences between the specification and the language code execution either it is considered as a bug and it should be fixed or the specification itself needs to be updated.

The advantage is that anyone can read this specification and understand how the link should behave.

Such specification does not make the existing Wiki obsolete because the Wiki can give more explanation and examples than the specification.

Existing Wiki does not mean that specification is redundant because there is no need to describe some special technical details in Wiki.

One more advantage of the specification is that it allows to write unit tests which makes the project itself more robust.

The first candidate for the specification is PutLink where should be explicitly mentioned how it behaves in case:

• PutLink argument is executable link
• PutLink argument is SetLink
• PutLink argument is ListLink

[linas]

How do you want to write the specification? Using some sort of formal verification language?

[linas]

Also, please note: PutLink is one of the more complicated links. The unit test PutLinkUTest has more than 40 different behaviors that it tests. A full specification, either formal or informal, would need to describe all of those behaviors.

They haven't been documented for two reasons:

1. The complexity of PutLink grew slowly over time, starting out as a very simple thing, and then accumulating more and more features as more and more uses were found.

2. The added features are kind-of "obvious", or "what one might expect" if one knows lambda-calculus. It does beta reduction, eta conversion, alpha renaming, partial substitution and composition. The driving force for most of this was a need to implement natural deduction -- https://en.wikipedia.org/wiki/Natural_deduction so that PLN uses PutLink as if it was the horizontal line of a formation rule, with judgments as inputs, and inferences as outputs.

[ferrouswheel]

I think this is related to #2232 - which is to document the existing behaviour and ensure it's visible. This also allows people to say "the documentation says this, but the code does this. we should fix one of them."