# nLab partial evaluation

Contents

### Context

#### Higher algebra

higher algebra

universal algebra

## Theorems

#### Algebra

higher algebra

universal algebra

# Contents

## 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)$.

The partial evaluation relation on $T A$ is defined by: $p\to q$ if and only if there exists a partial evaluation from $p$ to $q$. In other words, it is the (0,1)-truncation of the bar construction.

Similar definitions can be given internally to any category: instead of elements $p,q\in T A$, $r\in T T A$ one can take generalized elements (i.e. arrows) $p,q:X\to T A$, $r:X\to T T A$.

## Properties

• Every expression $p\in T A$ admits a partial evaluation to itself (given by $T\eta(p)\in T T A$). This makes the partial evaluation relation reflexive.

• Every expression $p\in T A$ admits a partial evaluation to its total evaluation $\eta(a(p))\in T A$, given by $\eta(p)\in T T A$.

• The partial evaluation relation is the smallest internal relation (in the category of $T$-algebras) which relates a formal expression? to its result.

• If the multiplication $\mu$ of the monad is a weakly cartesian natural transformation (i.e. its naturality square is a weak pullback), the partial evaluation relation is transitive, and hence a preorder.