<p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Algebraic effects for bounded prompt pipelines: Lawvere theories, handlers, and outcome traces

  • J. J. Segura

摘要

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.