Recurring Duties

[aacraf]

Reading through contract semantics I got a question regarding recurring duties.

In 5.4, these are stated as:

performed(a, x, s, Σ) :=
    ∃(a', x', s', t) ∈ Σ.performed :
        a' = a ∧ (x' = x ∨ x' includedIn⁺ x) ∧ s' matches s

Σ.performed records exact actions as they occur.

I see t in the tuple but not in the conditions, and since each occurrence keeps the same subject, action and asset, it looks like a duty fulfilled on day 1 would still count as fulfilled on day 2. Would adding t to the evaluation help here, or is it intended to be read in another manner?

[jgeluk]

Good catch — this is a real gap in §5.4, and you're reading it correctly: t is carried in the Σ.performed tuple but never constrained, so the check is intended-but-incomplete rather than deliberately time-blind.

Confirmed core problem. Since instantiate(duty, t) (§5.5) carries the same subject/action/asset into every occurrence instance, a single performance record satisfies performed() for all instances, past and future. A duty fulfilled on day 1 immediately fulfills the day-2 instance the moment it activates, and D-VIOLATE can never fire for later occurrences — recurring duties degenerate into "fulfill once, fulfilled forever."

Two adjacent defects that the same fix resolves:

1. Stuck-Active state in the non-recurring case. D-FULFILL (§5.2) requires performed = true ∧ deadline ≥ Σ.clock, while D-VIOLATE requires performed = false ∧ clock > deadline. If the action was performed before the deadline but evaluation only runs after it, neither rule applies and the duty stays Active forever. Constraining the performance time (rather than the evaluation clock) makes fulfillment decidable at any later clock.
2. Pre-activation performances count. A performance recorded before the duty ever activated (even before the agreement existed) currently fulfills it.

Proposed direction — window-parameterize the check, i.e. yes, adding t to the evaluation is exactly the right move:

performed(a, x, s, w, Σ) :=
    ∃(a', x', s', t) ∈ Σ.performed :
        a' matches a ∧ x' matches x ∧ s' matches s ∧ t ∈ w

with w = [Σ.activatedAt(d), effectiveDeadline(d, Σ)] in D-FULFILL/D-VIOLATE. For a schedule instance activated at occurrence time tᵢ this naturally becomes [tᵢ, tᵢ + deadline], so each occurrence needs its own performance inside its own window. D-FULFILL's deadline ≥ Σ.clock premise can then be dropped, since the window subsumes it.

One related inconsistency worth folding into the same change: §5.4 defines agent subsumption (a₁ matches a₂ ⟺ a₁ = a₂ ∨ a₁ memberOf⁺ a₂), yet the performed formula uses exact a' = a. Either the formula should use a' matches a (as above) or the agent-matching paragraph is dead text.

We'll address this on the schedule-model branch (#184) where this semantics landed.

[jgeluk]

@rivettp @tonyseale @matthiasautrata please add your view to this?