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

(…)

(…)