Question about behavior of existsence operator

[StarGazerM]

According to document ! with unbound meta var name can be used to create a placeholder, but seems following code, can't create any placehold? By definition this should be an infinity loop to show the continuous of foo?

foo(1).
foo(!y) :- foo(?x).

@export  foo :- csv {}.

And I also tried

foo(1).
foo(!y), bar(!y) :- foo(?x).

@export  foo :- csv {}.
@export  bar :- csv {}.

I this test example, a empty placeholder is generated for both foo and bar, but seems never used to inference another? I also check existence op paper https://iccl.inf.tu-dresden.de/w/images/f/f6/An_Existential_Rule_Framework_for_Computing_Why_Provenance_On_Demand_for_Datalog_%282%29.pdf

In the paper, existence operator is suppose to wit why provenance, which is a invariant tracks where each tuple comes could possibly comes from, so each of these place holder should be able to map to root node of an concrete proof tree. Does nemo's existence operator the same thing as whats in why-provenance-on-demand paper?

[monsterkrampe]

The behavior of the ! or exists operator depends a bit on the variant of the chase algorithm that is used. Nemo implements the standard chase, also known as the restricted chase. From a brief look at the paper you sent, they are apparently also considering the standard chase.

In this setting, the intuitive meaning of the exists operator is: "Create a new element if no matching one exists yet."
So in your first example, since foo(1) is given, the rule foo(!y) :- foo(?x) will not create a new placeholder, as we can replace !y by 1 to satisfy the rule.
In your second example, we need to create one placeholder for !y since we could not satisfy bar(!y) otherwise. But once we have such a placeholder, let's call it n, when we try to apply the rule again with foo(n), then we can reuse n to satisfy both foo and bar on the left hand side.

To witness non-terminating behavior, one would need to "connect" the existential variable to an existing value. For example, the following program will not terminate:

R(a,b).
R(?y, !z) :- R(?x, ?y).

This will create an infinite chain of Rs.

I hope this helps. I'm happy to answer more questions if you have any :)

A formal definition of the standard chase can be found in paragraph "Universal models and the chase" of the preliminaries of the following paper: https://proceedings.kr.org/2020/60/kr2020-0060-krotzsch.pdf But there is also plenty of other papers that define the standard chase in their preliminaries.

[StarGazerM]

Thank you for you great explaination! That helps a lot! I will close the issue soon