nLab operator


This entriy about operators in the sense of higher-order logic, which is the original sense and which has only that name. For operators in the sense of functional analysis, see linear operator. For the relation between these, see under Examples below. For yet other kinds of operators see at operation.



In a type theory with function types, given a type XX, an operator of base type XX is a term of type (X X) X X(X^X)^{X^X} aka (XX)(XX)(X \to X) \to (X \to X). This should be distinguished from a functional, which is a term of type X X XX^{X^X} aka (XX)X(X \to X) \to X, and a function, which (in this context) is a term of type X XX^X aka XXX \to X.

More generally, any term whose type has the form (A B) C D(A^B)^{C^D} aka (DC)(BA)(D \to C) \to (B \to A) may be called an operator, although usually not if any of these types is very trivial (since any type has this form, up to equivalence, if B,C,D1B,C,D \coloneqq 1).

Although one typically interprets type theory within set theory so that operations between types become functions, one may also use partial functions, which is necessary for the connection to linear operators in functional analysis.

An operator could also be interpreted within category theory as a globular 2-morphism in the 2-category of sets.


The Church numerals are operators in the (possibly typed) lambda-calculus:

  • 0(f(xx))0 \coloneqq (f \mapsto (x \mapsto x)),
  • 1(f(xfx))1 \coloneqq (f \mapsto (x \mapsto f x)),
  • 2(f(xffx))2 \coloneqq (f \mapsto (x \mapsto f f x)),
  • etc.

If we interpret XX as the real line, then X XX^X consists of real-valued maps of a real variable, which form a vector space. The partially defined linear maps from X XX^X to itself are the original linear operators. In functional analysis, we now replace X XX^X with an arbitrary topological vector space VV (originally but no longer necessarily taken to be a subspace? of X XX^X) and consider partial linear maps from VV to itself instead; so these linear operators are actually functions (meaning endofunctions) in a type-theoretic sense. In operator theory?, we go further and replace V VV^V with an arbitrary operator algebra (originally but no longer necessarily taken to be a subalgebra? of V VV^V); so these operators are unstructured terms in a type-theoretic sense.

A differential operator is a good example of something that is both an operator in the logical sense (since it turns functions into functions) and a linear operator in the sense of functional analysis (since differentiable functions form a vector space and differentiation acts linearly).

Last revised on January 10, 2020 at 10:37:08. See the history of this page for a list of all contributions to it.