Skip to content

How deeply may a policy nest its loops? (star height)

A policy written as text can say "repeat this", and inside that, "repeat this", and inside that again. Each extra level of repetition makes the policy harder for a reviewer to read and harder to predict. This page explains how the library measures that nesting (the policy's star height), why it refuses to compile a policy with more than three nested levels, what the mathematics behind the number three does and does not say, and what to do when your policy is rejected.

It assumes you have seen a policy written in the text language (the write a policy guide) and know what a regular expression is. The plain-language version of this check is Policy shape. Symbols and trust levels are explained in How to read these pages.

The question and the product situation

The question: is the written policy simple enough to audit?

Take an access-provisioning workflow. A request is submitted; an approver either approves it (the library proposes provision) or rejects it (it proposes close); then the next request can arrive. In the policy language that is one repetition around a sequence:

(test(submit) ; (test(approve) ; act(provision) | test(reject) ; act(close)))*

test(x) means "event x arrives", act(y) marks the action the policy proposes at that point, ; is "then", | is "or", and * is "repeat zero or more times". This is the policy in the workflow_liveness example.

Under deadline pressure, someone will want to encode "retry the approval, and retry the retry" by wrapping more * around parts of it. Every such policy is still a valid regular expression, but a reviewer reading four nested loops cannot easily say which events lead to which actions. The library therefore caps nesting at compile time: a policy with more than three nested * is rejected before any decision is made.

Intuition: count the loops inside loops

Draw the policy as a tree. Leaves are events (test), actions (act) and the empty step (eps). Inner nodes are "then", "or", "repeat" and "not". The star height is the largest number of "repeat" nodes you meet on any path from the root down to a leaf.

graph TD
    R["repeat *  (height 1)"] --> S["then ;  (height 0)"]
    S --> T1["test(submit)  0"]
    S --> U["or |  (height 0)"]
    U --> A["then ;  0"]
    U --> B["then ;  0"]
    A --> A1["test(approve)  0"]
    A --> A2["act(provision)  0"]
    B --> B1["test(reject)  0"]
    B --> B2["act(close)  0"]

The provisioning policy has one "repeat" on every path, so its height is 1. Two loops side by side, (test(a))* ; (test(b))*, still have height 1: neither is inside the other. Only nesting counts.

Note that height is about readability, not about how large the compiled machine gets. (((test(a))*)*)* has height 3 but describes the same thing as (test(a))*, and compiles to a tiny machine. A flat policy with many alternatives can have height 0 and still be large. Size has its own limits (max_nfa_states, max_dfa_states; see Defaults and limits).

Worked example from the code

Height by hand, for a few policies (the numbers below come from grounded_decision.grammar.height.star_height applied to grounded_decision.grammar.parse(...) of each string):

Policy text Height Why
test(a) ; act(b) 0 no repetition
(test(a))* ; (test(b))* 1 two loops side by side, neither nested
((test(a))* ; (test(b))*)* 2 a loop around a sequence that contains loops
(((test(a))*)*)* 3 three nested loops: the largest allowed
not((test(a))*) 1 not(...) does not add a level
((((test(a))*)*)*)* 4 rejected

The provisioning policy has height 1. Compiled, it becomes a machine (a DFA, deterministic finite automaton) with 5 states over the events approve, reject, submit:

  • 3 states with no action: the start state, the state after submit, and a dead state (no continuation: what an out-of-order event such as approve before any submit would lead to);
  • 2 states with an action: one proposes provision, one proposes close.

The statechart built from it leaves the dead state out, so it has 4 states, and an out-of-order event is simply not handled: the entity stays where it is and nothing is proposed.

The workflow_liveness example runs this policy and also tries to compile a four-level policy:

uv run grounded-decision examples workflow_liveness

Its closing lines read:

    policy star-height 1 (max 3); the four-loop policy was rejected at compile time
    also: star_height=1; illegal_rejected=star-height 4 exceeds max 3 (catalog 134); ...

The step-by-step example shows only the rejection:

uv run grounded-decision examples step_star_height_reject

  OUTPUT star-height 4 exceeds max 3 (catalog 134)
  NEXT   fix the policy text; there is no state to persist

There is no decision record for a rejected policy, because no module is ever built.

The precise statement

Definitions

Ordinary regular expressions are built from letters with union, concatenation and star. Generalized regular expressions also allow complement (and therefore intersection). The star height \(h\) of an expression \(E\) is defined by structural recursion:

\[ h(\text{letter}) = h(\varepsilon) = 0,\quad h(E_1 E_2) = h(E_1 \mid E_2) = \max\bigl(h(E_1), h(E_2)\bigr),\quad h(\lnot E) = h(E),\quad h(E^{\ast}) = 1 + h(E). \]

The star height of a language is the least height of any expression for it. The ordinary and generalized versions differ because complement can sometimes replace a star. For example, over the alphabet \(\{a, b\}\), the language \((ab)^{\ast}\) needs one star in an ordinary expression, but it is star-free: it is the complement of "starts with \(b\), or ends with \(a\), or contains \(aa\) or \(bb\)", where "anything" is written as the complement of the empty set. So its generalized star height is 0.

What is known

Where this result stands

In the wider literature: the generalized star-height problem is open. It is not even known whether any regular language needs generalized star height 2 or more. By contrast, ordinary star height is well understood: there are languages of every ordinary height (Eggan 1963; Dejean and Schützenberger 1966), and computing it is decidable (Hashiguchi 1988).

**In this project's math catalog (result 134):** the manuscripts claim
that every regular language over a finite alphabet has a generalized
expression of star height at most 3. This is checked by a Lean
statement of that uniform bound in the companion math catalog (kept
outside this repository). Treat it as a catalog claim that would settle a long-open
question, not as established mathematics.

**What this library relies on:** nothing about that claim affects
correctness. The library only measures the height of the expression
you wrote and rejects it if the height is above
`Limits.max_star_height` (default 3). The number 3 is taken from the
catalog as an auditability policy. See
[Where each result stands](status.md).

What the catalog statement would and would not give you

If the catalog claim is right, every regular policy language can be written with at most three nested stars, so the cap of 3 never forbids a behaviour, only a way of writing it. It would not tell you how to find the shorter expression, and the library does not search for one.

What the code does, and how it differs from the theorem

  • It measures the expression as written. check_star_height(expr, limits) computes \(h\) on the parsed tree with exactly the rules above and raises StarHeightError if \(h\) exceeds max_star_height. It does not compute the height of the language, does not minimise the automaton first, and does not rewrite your expression.
  • The check runs once, at compile time. compile_expr and Module.from_expr call it before building any automaton. The integer is cached on the module and reported on every decision record in the certificate check (metrics.star_height, trust=lean). Modules built directly from a statechart, such as the two-path examples (clinical_triage, fraud_review), have no source expression and report height 0.
  • not(...) is complement over the events named inside it. The compiler determinises the inner expression over the events that appear in it and flips which states accept. Events not mentioned inside the not(...) are not part of that complement. So textbook identities that rely on a global "any event" (such as writing "anything" as eps | not(eps)) do not hold in the policy language. Use not(...) for simple exclusions and test the compiled behaviour.
  • Actions are not events. act(provision) marks a state; it is not something the policy waits for. Only test(...) names contribute to the event alphabet.
  • Events with no arrow leave the state unchanged. An event the policy never mentions, or one it mentions arriving where the policy does not expect it, does not move the entity and proposes nothing (the decision record says the event is not handled).
Trust level What it covers here
proven (lean) The tag on the certificate check. It names the catalog statement the cap is taken from; the library does not run Lean and does not depend on that statement being true.
published (paper) Not used by this check.
practical (operational) Not used: the height is an exact integer, so there is no stand-in.

Parser details (grammar file, error messages, precedence) are in Grammar compile internals.

Limits, and what to do when a policy is rejected

What the check does not establish:

  • That the policy is small. A height-3 policy with many alternatives can still exceed max_nfa_states (512) or max_dfa_states (256); that is a separate CompileError.
  • That the policy is correct, or that every action is reachable. Height says nothing about which actions the policy can propose.
  • That no shorter equivalent exists, or that one does. It is a statement about your text.

StarHeightError: what now

The error is star-height 4 exceeds max 3 (catalog 134). Fix it by removing nesting that does not change meaning, or by splitting the workflow.

  1. Collapse redundant stars. A star directly inside a star adds nothing: ((test(a))*)* means the same as (test(a))*. So ((((test(access_requested))*)*)*)* from the step example can be written (test(access_requested))*, height 1.
  2. Flatten "repeat a repeat". \((x^{\ast} y^{\ast})^{\ast}\) is the same language as \((x \mid y)^{\ast}\) (any mix of \(x\) and \(y\)). For example:
((test(retry))* ; (test(escalate))*)*        # height 2
(test(retry) | test(escalate))*              # height 1, same events

Only do this when no act(...) sits between the inner loops, since the rewrite changes where an action could be marked.

  1. Split the workflow. If the nesting reflects real structure (an outer case lifecycle and an inner retry loop), model the inner loop as its own module and combine the verdicts with compose_parent; see Composition.

Raising Limits.max_star_height above 3 is possible but defeats the point: the cap exists so a reviewer can read the policy. Lowering it (to 1 or 2 for a tenant who writes simple policies) is a reasonable restriction. Parameter guidance is in Choose parameters.