Open ericprud opened 4 months ago
I realize that, because now the typing contains labels and not shapes, isValid does not need to call satisfies.
If completeTyping contained only those who satisfy exactly, then the definition of isValid(G, Sch, ism) could be for every (n, sl, exact) in ism,
Now about the main question, does completeTyping need to have only the exactly satisfied shape expr labels, or also those that are satisfied by some descendant: I think we can do it this way. It is not yet completely clear for me whether the two are equivalent wrt the properties that we need for completeTyping, so I preferred to be conservative. But after some thoughts I'm relatively confident that completeTyping restricted to those that satisfy exactly could also be ok.
1.5.2 Validation Definition says:
n@sl EXACTLY ::- satisfies(n, def(s.label), G, Sch, completeTyping(G, Sch), neigh(n))
n@sl ::- satisfiesDescendant(n, def(s.label), G, Sch, completeTyping(G, Sch), neigh(n))
where I understand
completeTyping()
to be making sure that the same total truth is maintained regardless of which pieces of it you interrogate with isValid queries. The same section then defines a correct typing:Should the correct typing be ONLY
satisfies(…)
? This would allow it to answer shapemaps where EXACTLY is true.I'm guessing that the current text (post-review by Iovka and Labra) is fine because we're counting on the first two lines of this issue text to differentiate EXACTLY from, um, not EXACTLY. Just wanted your eyes to verify this.