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:
Eric
Document D2:
Eric
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).