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.


The Church numeral?s 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).

Revised on June 8, 2017 09:58:56 by Urs Schreiber (