Algebraic effects for bounded prompt pipelines: Lawvere theories, handlers, and outcome traces
摘要
Large language model (LLM) applications are often implemented as prompt pipelines rather than as isolated prompt calls. A single run may combine retrieval, memory updates, validation failures, LLM calls, external tool calls, logging, replay, and sandboxing. This paper gives a compositional semantics for a bounded class of such systems using algebraic effects, many-sorted equational theories, Lawvere theories, and handlers. The source language is a typed call-by-value calculus with primitive operations for retrieval, state, exceptions, LLM invocation, and typed tool invocation. Its equations make explicit the assumptions under which state, exception propagation, and read-only retrieval interact. The induced equational theory yields the usual free-algebra semantics; handlers interpret the same source term as live execution, logging, replay, sandboxing, or testing. The main observational construction is an outcome trace semantics. A trace records both the ordered list of requested tool symbols and whether the computation terminates normally or exceptionally. This additional outcome component is necessary: exception propagation discards the continuation after an error, so a trace semantics that counts syntactic tool calls in discarded continuations is not invariant under the equations. Conditional branching is treated syntactically and receives a may-trace interpretation over both branches. Cyclic orchestration graphs are represented only through finite-depth unrolling, giving a precise semantics for bounded executions while leaving unbounded recursion and probabilistic LLM behavior to extensions of the theory. A worked case study formalizes a bounded retrieval–tool–validation agent with retry and reports the resulting trace classes as the retry budget increases.