negation, quantifiers and membership criteria as schema domains

1 files changed, 35 insertions, 0 deletions

diff --git a/docs/vm.org b/docs/vm.org
index e104b0f..6f3c454 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -65,6 +65,41 @@ the admission proof becomes a runtime termination measure: the
 witness shrinks structurally at every unfolding and the search
 bottoms out.
 
+* Negation and quantifiers
+
+=:not= is decidable denial. =u :not d= establishes the universe =u=
+and then refutes =d=; the denial only runs when its variables are
+ground, deferring like any other goal, so negation as failure over
+open goals cannot happen.
+
+=Exists= lowers to a conjunction at loading, since query variables
+are existential already; its =variable:= is renamed apart so the
+scope cannot be forged. =ForAll= runs when its quantifier is
+decidable: every solution of the quantifier must satisfy the body. A
+universal over an infinite domain is a non total plan, rejected, as
+decision 10 requires. Variables that live only under a universal are
+not answer variables.
+
+* Membership criteria as domains
+
+A schema attribute is constrained by a primitive domain or by a
+criterion: any relational expression with exactly one free variable,
+the subject, bound to the attribute value at admission.
+
+#+BEGIN_SRC sol
+Relation named: Employee schema: #(
+  [name domain: String]
+  [dept domain: ([Department id: D])]
+  [score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])]
+)
+#+END_SRC
+
+A foreign key is the criterion =([Department id: D])=, nothing more
+special than that. Criteria run against the complete extension, so
+the order facts appear in the source does not matter, the same way a
+committed state is judged whole. A fact whose attribute fails its
+criterion is an integrity violation and the program gets no world.
+
 * Builtins
 
 Domains check membership once ground: Integer, Natural, Rational,