Completeness proofs in categorical semantics usually proceed by building a syntactic category whose composition is given by substitution. For untyped effectful Call-by-Value languages, this runs into a basic obstacle: there is no canonical notion of simultaneous substitution of computations, since evaluation order is semantically meaningful. We address this by taking single computation substitutions, that is, binding steps, as primitive, and representing computation substitution by finite sequential lists composed by concatenation. We formalize this idea in a one-object Freyd-multicategorical setting. We introduce Freyd operads, separating a cartesian operad of values from a symmetric Ren-cartesian preoperad of computations, connected by a Freyd functor, and from any Freyd operad we construct a corresponding Freyd PROP of substitutions. We prove that this construction is representable and, in the strict one-object setting, left adjoint to restriction to codomain 1. Using the induced term model, we interpret untyped computational lambda-calculus with procedures and higher-order functions in weakly closed Freyd operads, and prove soundness, initiality, and completeness. This yields a categorical semantics tailored to untyped effectful computation and broad enough to encompass realizability-oriented models such as monadic combinatory algebras.

翻译：范畴语义中的完备性证明通常通过构建一个其组合由替换给出的句法范畴来进行。对于无类型有效按值调用语言，这面临一个基本障碍：由于求值顺序具有语义意义，因此不存在计算的同时替换的规范概念。我们通过将单一计算替换（即绑定步骤）视为原语，并将计算替换表示为通过连接构成的有限顺序列表来解决这个问题。我们在单对象Freyd-多范畴设定中形式化了这一思想。我们引入了Freyd Operad，将值的笛卡尔Operad与计算的对称Ren-笛卡尔前Operad分离，通过Freyd函子连接，并从任何Freyd Operad中构造对应的替换Freyd PROP。我们证明了该构造是可表示的，并且在严格单对象设定中，它是限制到余域1的左伴随。利用诱导的项模型，我们在弱封闭Freyd Operad中解释带有过程和更高阶函数的无类型计算λ演算，并证明了其可靠性、初始性和完备性。这产生了一种针对无类型有效计算的范畴语义，且足够广泛以涵盖面向可实现性的模型，如单子组合代数。