This entry 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. For yet other kinds of operators see at operation.
In a type theory with function types, given a type , an operator of base type is a term of type aka . This should be distinguished from a functional, which is a term of type aka , and a function, which (in this context) is a term of type aka .
More generally, any term whose type has the form aka 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 ).
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:
If we interpret as the real line, then consists of real-valued maps of a real variable, which form a vector space. The partially defined linear maps from to itself are the original linear operators. In functional analysis, we now replace with an arbitrary topological vector space (originally but no longer necessarily taken to be a subspace of ) and consider partial linear maps from 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 with an arbitrary operator algebra (originally but no longer necessarily taken to be a subalgebra? of ); 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 October 26, 2023 at 09:08:35. See the history of this page for a list of all contributions to it.