Any symbolic program with LLM calls is a select/call program

Type: kb/types/note.md · Status: seedling · Tags: computational-model

The decomposition lemma

Claim. Any program whose execution consists of:

  • symbolic computation over explicit machine state K
  • LLM calls r = call(P)

can be mechanically converted into the base loop:

while (P := select(K)) is not None:
    r  = call(P)
    K  = K + r

with select a symbolic function that returns either the next prompt or None, and with the same LLM calls in the same order.

Here K must contain the full symbolic machine state needed to resume execution: original inputs, prior call results, control location, loop counters, phase tags, pending work items, and any other symbolic locals the program consults between calls.

K + r means incorporating the call result into explicit symbolic state. In the simplest event-sourced case this is append-only: K stores the full trace, and later symbolic steps recompute derived views from it. Implementations may also cache derived state, but those caches are still explicit parts of K.

Why. Define select(K) as: run the program's symbolic transition logic from the current machine state until either program halt or the next LLM call site is reached. If symbolic execution reaches halt first, return None. If it reaches an LLM call site first, emit that prompt P.

Because all inter-call computation is symbolic, this check is exact. The halt-or-next-prompt decision is therefore a function of the current symbolic state alone. Iterating this construction reproduces the original program's call order and prompt contents, so the transformed loop makes the same LLM calls in the same order.

This is not a special property of LLM programs. It is the standard move behind operational semantics and abstract machines: execution is represented as transitions over explicit configurations, and control state that was implicit in source structure is reified into data.

Consequence. Once a program is shown to satisfy the preconditions, the base model's three invariants — per-call context limits, explicit state in K, symbolic orchestration — hold by construction. No additional invariant proof is needed for each program beyond checking those preconditions.

The ergonomic direction

The practical value runs opposite to the conversion: write in whatever style is natural (sequential phases, map/filter pipelines, nested loops) and the lemma guarantees it's a valid select/call program. You never need to flatten into a monolithic select — you just need to know you could.

Scope

LLM-mediated scheduling. The lemma requires inter-call computation to be symbolic. When the program uses an LLM call to decide what to do next (an LLM-mediated scheduler), that symbolic-computation precondition is violated and the symbolic-orchestration invariant no longer holds by construction.

Concurrency. Independent fan-out, barriers, and merges still fit the model: pending tasks and partial results can be represented in K, and the scheduler can serialize the coordination logic without changing which LLM calls occur. The real boundary is not concurrency itself but interaction that cannot be reduced to symbolic state transitions between calls — for example, mid-call visibility into another in-flight call, or dependence on external mutable state that is not represented in K.

Known lineage

The basis for the construction is standard programming-languages machinery rather than a special theorem about LLM systems:

  • Small-step / structural operational semantics represents execution as transitions over machine configurations.
  • Abstract-machine compilation reifies control state explicitly so the next transition is a first-order function of the current state.
  • CPS plus defunctionalization is the classic route when control flow needs to be turned into explicit symbolic state.

This note applies that generic compilation move to the specific case where the only non-symbolic steps are LLM calls.

Open questions

  • The decomposition heuristics might be expressible as transformations that increase call count while decreasing per-call complexity — the lemma guarantees the transformed program is still a valid select/call program.

Relevant Notes: