Markdown for LLMs

Count a completed set of conclusions

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# Count a completed set of conclusions

## Intention

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

## Incorrect form and why it stays silent

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

```law title="Incorrect form"
rule Feedback strict { for p: Person; for n: Integer; when size(p, n); then reach(p, p); }
```

## Correct form

```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 |

```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;

}
```

```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;

}
```

```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](/recipes/v-negation/missing-not-zero/).

## Pitfall

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