#
#  Hi!
#     feel free to add comments, questions, mark parts you don't understand
#     feel free to fix grammar or reword anything
#
#     this text will be later posted on Reddit.
#

What current Tauchain code does?

But first, what is TML? See TML Tutorial (Unfinished Draft) written by Ohad, where is TML explained: https://github.com/IDNI/tau#tml-tutorial-unfinished-draft
	 
TML is a variant of Datalog https://en.wikipedia.org/wiki/Datalog TML is going to be a very advanced implementation of Datalog.

Back to what current code does... Let's see examples used by Ohad for debugging. (these examples can be found in file "in" https://github.com/IDNI/tau/blob/master/in)
The variables (single characters in the example) can be replaced with any(?) word. The meaning of the words don't matter to the functionality of the program, but in reality they will match some actual meaning in the real world - otherwise the program will be useless. The eventually massive amount of relationships in the knowledgebase will increase the accuracy of the definitions of each 'word' and their meanings by giving them context. So when reading the examples, try replacing the single characters with some meaningful nouns. Starting from example 3 might be the easiest. See chapter Models: https://github.com/IDNI/tau#models 


1st test - simple pairs (actually the 2nd example is way more simple than this one. # This is a sub-program, and probably doesn't make much sense in itself to laymen. - yes, I just renamed them from examples to tests. The purpose was to explain what these logic programs do and how do they work. I also used these because they simply exist, and are correct and are first programs I see giving some valid results. I myself don't know much about TML to create my own logic programs.)
 
Logic program:
 
1 2.
?y ?x :- ?x ?y.
3 ?x :- 2 ?x.
 
Output:

step: 1
1 2 

step: 2
1 2 
2 1 

step: 3
3 1 
1 2 
2 1 

step: 4
3 1 
1 3 
1 2 
2 1 

To explain the logic program, you can see there are statements (clauses) separated by ".". Same like sentences are separated in English.
Clauses can be facts or rules.

"1 2." is a fact - something which is supposed to be true.
1 2. means there is a connection (edge) from 1 to 2. you can imagine it as a pair 1 2.

"?y ?x :- ?x ?y." and "3 ?x :- 2 ?x." are rules. They have left (head) and right (body) side and these sides are separated by ":-" symbol.
These rules are called Horn clauses (https://en.wikipedia.org/wiki/Horn_clause) and they basically mean that HEAD is true if BODY is true. You can imagine these like facts with conditions.
You can read ":-" like "if".

?x and ?y are variables for substitution. The code uses all known facts and tries to substitute them in bodies of rules provided in the logic program.
When some fact matches a body of a rule, it creates new fact from the head of the rule.

You can read rule "?y ?x :- ?x ?y." like: there is an edge ?y ?x if there is an edge ?x ?y.
This rule makes any pair going in both directions.

Second rule "3 ?x :- 2 ?x." you can read like: there is an edge 3 ?x if there is an edge 2 ?x. so every edge coming from 2 to something is also coming from 3 to the same thing.

How does the substitution work step by step:

At the beginning the reasoner knows only the pair 1 2.

It tries to fit this pair into bodies of the rules and finds new fact:

?y ?x :- ?x ?y. (?x = 1, ?y = 2) => 2 1 :- 1 2. "There is a pair 2 1. if there is a pair 1 2.". We have a new fact: 2 1. We know that: 1 2. 2 1.

3 ?x :- 2 ?x. (?x = 1) => 3 1 :- 2 1. "There is a pair 3 1. if there is a pair 2 1.". We have new fact 3 1. We know that: 1 2. 2 1. 3 1.

Now it tries to fit the new known facts 2 1. and 3 1. into the bodies as well:

?y ?x :- ?x ?y. (?x = 2, ?y = 1) => 1 2 :- 2 1. "There is a pair 1 2. if there is a pair 2 1.". 1 2. It's nothing new, because we already know that.

?y ?x :- ?x ?y. (?x = 3, ?y = 1) => 1 3 :- 3 1. "There is a pair 1 3. if there is a pair 3 1.". We have a new fact: 1 3. We know that: 1 2. 2 1. 3 1. 1 3.

There is no other fact we can deduce.

Result is therefore: 1 2. 2 1. 3 1. 1 3.

You can see that reasoner returns all the facts which can be inferred from known facts and rules.


2nd test - yes, you can use strings :)

Logic program:

a a.
b b.
a 2.
b ?x :- a ?x.   # if there is any ?x where a ?x, then there is b ?x. it means that any edge coming from "a" comes from "b" as well.

Output:

step: 1
a 2 
a a 
b b 

step: 2
a 2 
a a 
b 2 
b a 
b b

a a. and a 2. fits into body of the only rule. we can infere new facts: b a. and b 2.


3rd test - transitive closure - recursion (does not work yet)

This is transitive closure and it is more complex universe than 1 2. 2 1. 1 3. 3 1.
It uses recursion and this example is causing Segmentation fault error. So it is does not work yet.
See https://github.com/IDNI/tau#example-transitive-closure for more information.

Logic program:

e 1 2.     # fact: edge from 1 to 2
e 2 3.     # fact: edge from 2 to 3
t ?x ?y :- e ?x ?y.     # if there is an edge from ?x to ?y then there is transition (path) from ?x to ?y
t ?x ?y :- t ?x ?z, e ?z ?y.     # if there is a transition from ?x to ?z and there is an edge from ?z to ?y then there is path from ?x to ?y (in datalog: "," means "and")

Think of ´e´ as "the type of relation between 1 and 2". ´e´ could be replaced with ´preceeds´, ´1´ with ´chicken´, and ´2´ with ´egg´. Thus: ´preceeds´ ´chicken´ ´egg´ would mean "chicken preceeds egg".

Output:

step: 1
e 2 3 
e 1 2 

Segmentation fault (core dumped)


This test/example uses recursion which should result into all possible paths through the graph.
I think the resulting knowledgebase should be:

e 1 2. 
e 2 3.
t 1 2.
t 2 3.
t 1 3.

inferred facts should come this way (fact fitting a body => new fact created from the body's head):
e 1 2. => t 1 2.
e 2 3. => t 2 3.
t 1 2, e 2 3. => t 1 3.


4th test - padding?

see steps pfp program outputs... you can see how it increases its knowledgebase in each step.

1 2.
1 2 3.
?y ?x :- ?x ?y.
3 ?x :- 2 ?x.
4 ?y ?x :- 2 ?x ?y.
5 ?y ?x :- 1 ?x ?y.

Output:

step: 1
1 2 3 
1 2 * 

step: 2
5 3 2 
1 2 3 
1 2 * 
2 1 * 

step: 3
3 1 * 
5 3 2 
1 2 3 
1 2 * 
2 1 * 

step: 4
3 1 * 
5 3 2 
1 3 * 
1 2 3 
1 2 * 
2 1 * 


Should be noted that all these examples are presumably just simple logic programs suitable for debugging basic features of TML.

Examples from other sources and Datalog variants

While TML still needs some time of debugging you can try different implementations of Datalog to learn how will TML look like. TML will be not that much different.
It will be much faster and advanced variant of Datalog. It removes limitation of negation in recursion (see number 2. in "Features, limitations and extensions"
https://en.wikipedia.org/wiki/Datalog#Features,_limitations_and_extensions)

It is difficult to imagine what negation in recursion means. It is said that you would be able to ask "What translators do not translate into German?"
You cannot ask these questions in current Datalog implementations.

For other examples you can check this often presented example with parent and ancestor relations/edges. https://en.wikipedia.org/wiki/Datalog#Example

You can also try datalog yourself: http://des.sourceforge.net/ (in Java - runs everywhere and contains lot of examples)

Or you can try datalog online: https://datalog.db.in.tum.de/ (examples in German but it should be easy to translate them with dictionary. There are only few words used in every example)

This datalog implementation looks little bit like English: https://github.com/harc/nl-datalog
live demo does not work anymore, but you can just download it, unpack it and open index.html in browser (works in firefox for me) and you can play with it.