Count a completed set of conclusions

Intention

I want to count reachable vertices after all producers have finished.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

A producer that depends back on the count result forms a completion cycle:

Incorrect form

rule Feedback strict { for p: Person; for n: Integer; when size(p, n); then reach(p, p); }

Correct form

Arxo Law

language "law.core" version "0.2";
package recipes.v.r08 version "0.1.0";
namespace "urn:recipe:v-negation:08";

entity Person;
relation edge(a: Person, b: Person);
relation reach(a: Person, b: Person);
rule Base strict {
    for a: Person; for b: Person;
    when edge(a, b);
    then reach(a, b);
}
rule Step strict {
    for a: Person; for b: Person; for c: Person;
    when monotone(reach(a, b)) and edge(b, c);
    then reach(a, c);
}
relation root(p: Person);
relation size(p: Person, n: Integer);
rule Count strict {
    for p: Person;
    when root(p);
    then size(p, count(collect x: Person where monotone(reach(p, x))));
}

Frozen execution scene

Facts	Question	Answer
root(a), chain a→b→c	size(a,2)	TRUE_ONLY
same facts	size(a,1)	NEITHER
root(a), no edges	size(a,0)	TRUE_ONLY
add Feedback	check	E4102

full closure counts two

Arxo Law

test "full closure counts two" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert root(entity_ref("urn:recipe:v-negation:08:a"));
        assert edge(entity_ref("urn:recipe:v-negation:08:a"), entity_ref("urn:recipe:v-negation:08:b"));
        assert edge(entity_ref("urn:recipe:v-negation:08:b"), entity_ref("urn:recipe:v-negation:08:c"));
    }
    evaluate truth(size(entity_ref("urn:recipe:v-negation:08:a"), 2));
    expect truth_status == TRUE_ONLY;

}

wrong early count stays unknown

Arxo Law

test "wrong early count stays unknown" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert root(entity_ref("urn:recipe:v-negation:08:a"));
        assert edge(entity_ref("urn:recipe:v-negation:08:a"), entity_ref("urn:recipe:v-negation:08:b"));
        assert edge(entity_ref("urn:recipe:v-negation:08:b"), entity_ref("urn:recipe:v-negation:08:c"));
    }
    evaluate truth(size(entity_ref("urn:recipe:v-negation:08:a"), 1));
    expect truth_status == NEITHER;

}

childless root counts zero

Arxo Law

test "childless root counts zero" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert root(entity_ref("urn:recipe:v-negation:08:a"));
    }
    evaluate truth(size(entity_ref("urn:recipe:v-negation:08:a"), 0));
    expect truth_status == TRUE_ONLY;

}

Counterfactual

teaches adds Feedback. monotone inside collect does not turn enumerating a set into a point reading; the cycle is rejected with E4102. E4112 applies to a defeater without a candidate, not to this cycle.

Boundary

An aggregate in the head always waits for completion. The exception for a monotone guard in the body cannot be moved onto the count value. Empty count yields zero; empty sum is the separate case of Distinguish an unknown sum from zero.

Pitfall

The scenes check the full number and the absence of a premature one: an aggregate must wait for completion before counting.