nLab partial evaluation

Idea

A partial evaluation is an instruction to evaluate a formal expression? piecewise, without necessarily obtaining the final result.

For a simple example, the sum “$3+4+5$” can be evaluated to “$12$”, but also partially evaluated to “$7+5$”.

Definition

Let $(T,\mu,\eta)$ be a monad on Set, and let $(A,a)$ be an algebra over $T$. Given two elements $p,q\in T A$, a partial evaluation from $p$ to $q$ is an element $r\in T T A$ such that $\mu(r)=p$, and $T a(r)=q$.

Equivalently, partial evaluations are the 1-simplices of the bar construction (considered as a simplicial set) of the algebra $(A,a)$.

(…)

Examples

(…)

• For many probability monads, partial evaluations correspond to conditional expectation of functions;
• For the free cocompletion monad, partial evaluations correspond to pointwise left Kan extensions.

See also

• bar construction, monad, algebra over a monad, operad, algebra over an operad
• simplicial set, Segal space, Segal conditions, Kan complex

References

• Tobias Fritz and Paolo Perrone, Monads, partial evaluations, and rewriting. (arXiv)

• Carmen Constantin?, Tobias Fritz, Paolo Perrone and Brandon Shapiro?, Partial evaluations and the compositional structure of the bar construction. (arXiv)

• Paolo Perrone, Walter Tholen, Kan extensions are partial colimits, Applied Categorical Structures, 2022. (arXiv:2101.04531)