Use a subset of FOL to reason about different use cases
=======================================================

Case study:

0: Entailment
1: Parsing twice
2: Splitting / merging (exchange inbetween)
3: Refer from another document


Anonymous nodes as existential variables:
----------------------------------------

URI constants: C = {c1,...,cN,...}

Relation symbol: t

{ exists, & }

Variables: {x1,...,xN,...}

graph/document = formula w/o free variables (most general consensus?)


Applications exchange documents in intermediate format (BLOB), but get
formulae (graphs) in the end.

d1 = t(c1, c2, c3)
d2 = exists x1 t(c1, c2, x1)
d3 = exists x1 [ t(c1, c2, x1) & t(x1, c3, c4) ]


Equivalence:

Let -> be entailment

d1 = d2 <=> d1 -> d2 and d2 -> d1



ad 0): t(c1, c2, c3) -> exists x1 t(c1, c2, x1)    [Inference that DanC did not
want]

ad 1): d1 = exists x1 t(c1, c2, x1)
       d2 = exists x2 t(c1, c2, x2)

       d1 -> d2 and d2 -> d1 => d1 = d2 (fine)

ad 2): d1 = exists x [ t(c1, c2, x) & t(x, c3, c4) ]

       How split?

       d1' : exists x1 t(c1, c2, x1)
       d1'': exists x2 t(x2, c3, c4)

       Merge: d1''' = exists x1 t(c1, c2, x1) & exists x2 t(x2, c3, c4)

       d1 -> d1''', but d1''' -/-> d1  => d1 != d1'''

       irreversible change when docs are split and merged (bad?)

ad 3): impossible to refer to anon. nodes in another document within the formal
model
 
       d1 = exists x1 t(c1, c2, x1)
       d2 = exists x2 t(c1, c2, x2)

       no way to ask: is x1 in d1 same as x2 in d2?


Anonymous nodes as local constants:
-----------------------------------
(Implementation perspective)

URI constants: C = {c1,...,cN,...}

Local constants: PRG1 = {l1_1,...l1_N,...}, PRG2 = {l2_1, ..., l2_N,...}

Rule: prg1 cannot see constants in document


ad 0): t(c1, c2, c3) -/->, <-/- t(c1, c2, l1)  [fine]

ad 1): d1 = t(c1, c2, l1_1), second parse d2 = t(c1, c2, l1_2)
       d1 != d2 [bad?]

ad 2): splitting d1 = t(c1, c2, l1_1) & t(l1_1, c3, c4)
       d1''' = d1 [fine]


ad 3): C != PRG1 != PRG2 etc.

       prg1: t(c1, c2, l1_1)
       prg2: t(c1, c2, l2_1)

       still cannot ask l1_1 =? l2_1 because variables invisible:
       each time serialized docs are passed from prg1 to prg2,
       local variables become different


Anonymous nodes as global constants
-----------------------------------

URI constants:    C = {c1,...,cN,...}
Global constants: A = {a1,...,aN,...}      A and C are disjoint.

Imagine there is a way to assign variables to anon. nodes based on
structural properties of a formulae/document in a unique fashion.

Example:      t(c1,c2,__) & t(__, c3, c4)   => uniquely assigned say a1

ad 0): t(c1, c2, c3) -/-> t(c1, c2, a1)   [fine]

ad 1): t(c1, c2, a1), second parse t(c1, c2, a1) => d1=d2 [fine]

ad 2): Splittng fine

ad 3): pass document => constants from A are reassigned, but in the same fashion
       => effectively can refer

Observations:

- A does not contain URIs (disjoint). If A and C overlap, we cannot
  distinguish anon. nodes from the others. But: since the same procedure
  for assigning constants from A, this is irrelevant.
  A can be viewed as subset of C that is (extremely) unlikely to be used by
someone.

- application that need not communicate may use local IDs. If
  communicate using syntax that contains "holes", fine. No global
  autogeneration algorithm required.

- if no standard assignment algorithm is required, ad 1) is still violated!
  (parsing twice)


Anonymous nodes as hybrid of global and local constants:
-------------------------------------------------------

Both C, A, PRG1, ... PRGN, ...

implications?



EXAMPLE:

parsing the same document D twice.

Document D1:

<rdf:Description>
   <dc:Creator>Eric</dc:Creator>
</rdf:Description>

Document D2:

<rdf:Description>
   <dc:Creator>Eric</dc:Creator>
</rdf:Description>


Interpretation 1 (anonymous nodes as existential variables):

d1 = exists x t(x, dc:Creator, "Eric")
d2 = exists y t(y, dc:Creator, "Eric")

d1 -> d2, d2 -> d1 => d1 = d2 (still the same???!!!)

Only Interpretation 2 makes them different, i.e. when local variables
are assigned!

d1 = t(x, dc:Creator, l1)
d2 = t(y, dc:Creator, l2)

d1 != d2

With respect to equivalence, Interpretation 3 (autogeneration) is
equivalent with Interpretation 1 (existential variables).