Markdown for LLMs
Procedures: states, transitions, carrier, fold
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# Procedures: states, transitions, carrier, fold
**In one sentence:** these constructs answer the question "where
the case stands now and how it got here". Take them when the case history is an
automaton: states, transitions on carrier events, transition conditions; and
the core derives where the case stands (`current_state`) from the history of
attempts.
A case history is an automaton — states, transitions on carrier events, guards — and the engine folds the attempt history into the current state.
## 1. When to take it and when not to
| Instead of | Selection rule |
|---|---|
| Procedure vs a set of `strict` rules | Case history is a sequence of states with strict order ("filing first, review after") — procedure: the order comes from carrier time, not from rule positions in the file. Independent unordered conditions — plain rules |
| `on E` vs a transition without `on` | Carrier is a domain event (filing, opening, signing) — an `on` clause with a declared event; the carrier type is checked (`LDC-E1344`, `TRANSITION_CARRIER_TYPE_MISMATCH`). A step with no domain event — a transition without `on`, carrier is a synthetic `<P>Step` with `id`/`time` |
| `entered_state(x, S, e)` vs `current_state(x, S)` | "Entered BY this event" (re-entry is a new fact with a new carrier) — `entered_state` with a carrier; "where it stands now" (projection of the end of history) — `current_state`; "starts in" — `initial_state`. The two-argument `entered_state` no longer exists |
| `when` vs `requires` | Condition on world facts — guard `when` (sees the prefix state); condition on completion of another procedure/instance — `requires completed(P, y)`. A guard reading a power effect or a rule over the fold — `LDC-E1348` |
| `parallel` with regions vs two procedures | One step — two independent motions (two tokens, one carrier) — `parallel` regions with `join`; two separate histories — two procedures. One carrier — one atomic step, otherwise `CARRIER_REUSED` |
## Grammar: event and record constructor (EBNF verbatim from the grammar)
An event declaration — fields with mandatory constructor `id`/`time` (without them — `LDC-E1343`):
```ebnf
event_decl = "event", identifier,
[ ":", type_ref ], "{",
{ field_decl | label_item | metadata_item },
"}" ;
```
A record constructor — the same record in `const`, case-`const`, and assertion-argument positions (executable in three positions):
```ebnf
record_literal = qualified_name, "{",
[ record_field, { ",", record_field }, [ "," ] ],
"}" ;
record_field = identifier, ":", expression ;
```
## 2. Minimal example
Package `research.procedure.accreditation`: an application goes `Draft → Submitted`
on the `ApplicationFiled` event when the application is complete; then —
`Accredited`.
```law
procedure Accreditation(app: Application) {
state Draft initial;
state Submitted;
state Accredited terminal;
transition Submit {
from Draft;
to Submitted;
on ApplicationFiled;
when application_complete(app);
}
transition Grant {
from Submitted;
to Accredited;
}
}
```
Case 1: instance + `application_complete` + a `Submit` attempt with carrier
`ApplicationFiled { id, time: @2026-04-14T10:00:00+05:00 }`. Query:
`evaluate truth(current_state(app17, Submitted))`. Case 2: instance only;
query `initial_state(app17, Draft)`.
Observed engine answer (installed `law`, semantics `law.core/0.2`):
```text
law test research.procedure.accreditation: мир research.procedure.accreditation
ok [research.procedure.accreditation#authored] tests/01-submitted.lawtest / urn:query:research-procedure-01
ok [research.procedure.accreditation#authored] tests/02-no-attempt.lawtest / urn:query:research-procedure-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```
`law engine check` — `check OK`, no warnings. Case 1 answers
`TRUE_ONLY` with `COMPUTED`: the transition is valid (state before the carrier —
`from`, type matched `on`, guard true), the fold publishes
`valid_transition`, `left_state(Draft)`, `entered_state(Submitted)`.
Case 2 — `initial_state(Draft)` — `TRUE_ONLY`: history empty, the initial
state holds without a carrier. Sensitivity: removing the attempt from case 1
changes the answer from `current_state(Submitted)` to the initial state (case 2);
removing `application_complete` leaves the case in `Draft` — see the second
package.
Second package `research.procedure.chain` — same procedure, two outcomes:
| Facts | Question | Answer | Why |
|---|---|---|---|
| instance + `Submit` attempt, guard false | `current_state(Draft)` | `TRUE_ONLY` | transition invalid — the attempt stays an attempt, state unchanged |
| instance + completeness + `Submit`, then `Grant` with synthetic `AccreditationStep` | `current_state(Accredited)` | `TRUE_ONLY` | two history steps, order by carrier `time` |
## 3. Example by domain
- **Law:** RK procurement (package `kz.corpus.procurement`, Kazakhstan) — transitions `on BidsOpeningHeld` / `on
ContractConcluded` (see `corpus-forms.md`): domain carrier events with guards.
- **Standard/protocol:** this page's examples —
the same device in miniature (`ApplicationFiled`, synthetic
`AccreditationStep`); the teaching package repeats it almost verbatim.
- **Sport:** FIDE chess (package `fide.laws.chess`, international sport) — synthetic carriers `GamePlayStep`:
no domain events for moves — case steps, `entered_state` with
carrier and `left_state` in queries.
- **Religion/custom:** the "Queue" queue — absence and roll-call events as
attempt carriers; the neighbouring link — the duty activation formula
`entered_state(x, Draft, e)` reads entry with a carrier,
initial entry — predicate `initial_state(x, S)` without a carrier.
## 4. How the engine answers
Table — observed runs of this directory's examples (installed
`law`, semantics `law.core/0.2`):
| Facts | Question | Answer | Why |
|---|---|---|---|
| instance + completeness + `Submit` attempt | `current_state(Submitted)` | `TRUE_ONLY` | all four validity conditions |
| instance only | `initial_state(Draft)` | `TRUE_ONLY` | empty history, initial holds |
| instance + attempt without completeness | `current_state(Draft)` | `TRUE_ONLY` | guard false — state unchanged |
| full chain + `Grant` with synthetic carrier | `current_state(Accredited)` (plus `left_state(Draft, e_submit)` — `TRUE_ONLY`, `current_state(Draft)` — `NEITHER`) | `TRUE_ONLY` | fold of two carriers by time; left-behind and no-longer-current — from the full-chain scenario ("draft left" / "case no longer in draft") |
| instance + completeness + `Submit` attempt with an `AccreditationStep` carrier | `valid_transition(Submit, e)` | `NEITHER` + `TRANSITION_CARRIER_TYPE_MISMATCH` | carrier type mismatched `on` |
- The instance history is attempts with `supported` support at version-chain
heads, ordered by carrier `time` start; equal starts for one instance —
fatal `SIMULTANEOUS_EVENTS`; for different instances —
not a refusal (a group reads the state before the group).
- An invalid transition (false guard, another instance's `from`, mismatched `on` type) —
a routine outcome: the attempt stays an attempt, state unchanged; carrier
type missing `on` gives `TRANSITION_CARRIER_TYPE_MISMATCH` (warning),
a fact about another instance — `EVENT_OUTSIDE_PROCEDURE` (warning).
- A guard sees only the prefix before its carrier; reads of neighbouring
predicates go inside the fold as prefix state; a predicate
produced above the fold (rule over the fold, power effect,
status atom) — `LDC-E1348` / fatal `NON_EXECUTABLE_UNSTRATIFIED`.
- Guard and `requires` — carriers of the judgment channel:
a live transition with an open judge answers `NEITHER` with
`REQUIRES_JUDGMENT`; a rule reading transition facts inherits judges.
- `current_state` is non-monotone (end projection), the rest is monotone over
the prefix; one law for the whole history (`legal_time` — on the document).
## 5. Common mistakes
1. Record order in the case instead of carrier `time` — history is ordered by
the start of canonical `time`; records are read as a set
(`pitfalls.md`, item 1).
2. Two-argument `entered_state(x, S)` — the form no longer exists: "stands" —
`current_state`, "starts" — `initial_state`, "entered by this" —
`entered_state` with a carrier (`pitfalls.md`, item 2).
3. Same-name members of two procedures — a bare name resolves via the package
member table; a duplicate — `LDC-E1351` (`pitfalls.md`, item 3).
4. Guard reading a power effect or a status — `LDC-E1348`: rewrite to
empirics or `requires completed(P, y)` (`pitfalls.md`, item 4).
5. One carrier for two transitions of one region — fatal `CARRIER_REUSED`;
concurrency — only in independent `parallel` regions
(`pitfalls.md`, item 5).
6. Initial entry presented as `entered_state` — forbidden: it has
no carrier; the activation formula does not bind it (binding it would
fail reading `e.time`; `pitfalls.md`, item 6).
## 6. References
- Tutorials: [procedure](/tutorials/procedure/), [procedure exercise](/tutorials/exercise-procedure/);
the process layer (frames across editions, decision journals) lives in tooling, not in the core fold.