operator

This is 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.

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

More generally, any term whose type has the form $(A^B)^{C^D}$ aka $(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,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 \coloneqq (f \mapsto (x \mapsto x))$,
- $1 \coloneqq (f \mapsto (x \mapsto f x))$,
- $2 \coloneqq (f \mapsto (x \mapsto f f x))$,
- etc.

If we interpret $X$ as the real line, then $X^X$ consists of real-valued maps of a real variable, which form a vector space. The partially defined linear maps from $X^X$ to itself are the original linear operators. In functional analysis, we now replace $X^X$ with an arbitrary topological vector space $V$ (originally but no longer necessarily taken to be a subspace? of $X^X$) and consider partial linear maps from $V$ 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^V$ with an arbitrary operator algebra (originally but no longer necessarily taken to be a subalgebra of $V^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 October 18, 2013 09:28:29
by Toby Bartels
(64.89.53.106)