From 40376c3ea009eab4db9ba27837e61d8bec310b8f Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 03:15:25 -0300 Subject: negation, quantifiers and membership criteria as schema domains --- docs/vm.org | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) (limited to 'docs') 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, -- cgit v1.2.3