nLab partial evaluation

Contents

Context

Higher algebra

Algebra

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

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+53+4+5” can be evaluated to “1212”, but also partially evaluated to “7+57+5”.

Definition

Let (T,μ,η)(T,\mu,\eta) be a monad on Set, and let (A,a)(A,a) be an algebra over TT. Given two elements p,qTAp,q\in T A, a partial evaluation from pp to qq is an element rTTAr\in T T A such that μ(r)=p\mu(r)=p, and Ta(r)=qT a(r)=q.

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

The partial evaluation relation on TAT A is defined by: pqp\to q if and only if there exists a partial evaluation from pp to qq. 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,qTAp,q\in T A, rTTAr\in T T A one can take generalized elements (i.e. arrows) p,q:XTAp,q:X\to T A, r:XTTAr:X\to T T A.

Examples

Properties

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

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

  • The partial evaluation relation is the smallest internal relation (in the category of TT-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.

See also

References

Last revised on July 21, 2024 at 16:09:08. See the history of this page for a list of all contributions to it.