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

(…)

Examples

(…)

See also

References

Last revised on January 14, 2021 at 05:25:01. See the history of this page for a list of all contributions to it.