nLab partial function

Redirected from "partial anafunction".
Partial functions

Partial functions

Idea

A partial function f:ABf: A \to B is like a function from AA to BB except that f(x)f(x) may not be defined for every element xx of AA. (Compare a multi-valued function, where f(x)f(x) may have several possible values.)

In some fields (including secondary-school mathematics even today), functions are often considered to be partial by default, requiring one to specify a total function otherwise. As category-theoretic and type-theoretic formalisation spreads, this is difficult to treat as the basic concept, and the most modern idea is that a function must be total. If you want partial functions, then you can get them in terms of total functions as below.

Definitions

In type theory

As functions

In dependent type theory, given h-sets AA and BB, a partial function ff from AA to BB is an h-proposition-valued type family P fP_f on AA which states whether ff is defined for element a:Aa:A, and a section

x:A,p:P ff:Bx:A, p:P_f \vdash f:B

If the dependent type theory has function types and dependent sum types, then one could define the partial function directly as:

f:( a:AP f(a))Bf:\left(\sum_{a:A} P_f(a)\right) \to B

As partial anafunctions

In dependent type theory, given types AA and BB, a partial anafunction is a type family x:A,y:BR(x,y)typex\colon A, y \colon B \vdash R(x, y) \; \mathrm{type} which comes with a family of witnesses

x:Ap(x):isProp( y:BR(x,y))x \colon A \vdash p(x) \colon \mathrm{isProp}\left(\sum_{y:B} R(x, y) \right)

that for each element x:Ax\colon A, the dependent sum type y:BR(x,y)\sum_{y \colon B} R(x, y) is a mere proposition.

Historically, partial anafunctions are called functional relations, but nowadays in type theory one tends to use the term relation only for those type families which are valued in mere propositions.

For any partial anafunction, there is a partial function

x:A,p:isContr( y:BR(x,y))f(x,p):Bx:A, p:\mathrm{isContr}\left(\sum_{y:B} R(x, y) \right) \vdash f(x, p):B

which could be written as the function

f: x:AisContr( y:BR(x,y))Bf:\sum_{x:A} \mathrm{isContr}\left(\sum_{y:B} R(x, y) \right) \to B

since y:BR(x,y)\sum_{y:B} R(x, y) is already a proposition, one could simply use

x:A,p: y:BR(x,y)f(x,p):Bx:A, p:\sum_{y:B} R(x, y) \vdash f(x, p):B

instead, and by the rules of dependent sum types, it becomes

x:A,y:B,p:R(x,y)f(x,y,p):Bx:A, y:B, p:R(x, y) \vdash f(x, y, p):B

on the other side, the function can be written as

f:( x:A y:BR(x,y))Bf:\left(\sum_{x:A} \sum_{y:B} R(x, y) \right) \to B

 Examples

There are multiple examples of partial functions in mathematics.

The reciprocal function on the real numbers is only defined on the real numbers apart from zero, and so is given by the following rules:

ΓtypeΓ,x:,p:|x|>0() 1:\frac{\Gamma \vdash \mathbb{R} \; \mathrm{type}}{\Gamma, x:\mathbb{R}, p:\vert x \vert \gt 0 \vdash {(-)}^{-1}:\mathbb{R}}
ΓtypeΓ,x:,p:|x|>0recipax:x(x,p) 1= 1\frac{\Gamma \vdash \mathbb{R} \; \mathrm{type}}{\Gamma, x:\mathbb{R}, p:\vert x \vert \gt 0 \vdash \mathrm{recipax}:x \cdot {(x, p)}^{-1} =_\mathbb{R} 1}

The reciprocal function is given by the partial anafunction xy= 1x \cdot y =_\mathbb{R} 1.

Another example is the metric square root on the real numbers, which is only defined on the non-negative real numbers, and is given by the following rules:

ΓtypeΓ,x:,p:x0:\frac{\Gamma \vdash \mathbb{R} \; \mathrm{type}}{\Gamma, x:\mathbb{R}, p:x \geq 0 \vdash \sqrt{-}:\mathbb{R}}
ΓtypeΓ,x:,p:x0sqrtax:x,p 2= x\frac{\Gamma \vdash \mathbb{R} \; \mathrm{type}}{\Gamma, x:\mathbb{R}, p:x \geq 0 \vdash \mathrm{sqrtax}:\sqrt{x, p}^2 =_\mathbb{R} x}

In both cases, the witness pp is usually left implicit in informal notation, and the partial function is written as x 1{x}^{-1} or x\sqrt{x}.

In category theory

In the category of sets

Given sets AA and BB, a partial function ff from AA to BB consists a subset DD of AA and a (total) function from DD to BB. In more detail, this is a span

D ι f A B \array { & & D \\ & \swarrow_\iota & & \searrow^f \\ A & & & & B \\ }

of total functions, where ι:DA\iota: D \to A is an injection. (This condition can be dropped to define a partial multi-valued function, which is simply a span.)

AA and BB are called the source and target of ff as usual; then DD is the domain of ff and ι:DA\iota: D \to A is the inclusion of the domain into the source. By abuse of notation, the partial function ff is conflated with the (total) function f:DBf: D \to B.

Notice that the induced function DA×BD \to A \times B is an injection, so a partial function is the same as a functional relation seen from a different point of view.

We consider two partial functions (with the same given source and target) to be equal if there is a bijection between their domains that makes the obvious diagrams commute. You can get this automatically in a traditional set theory by requiring DD to be literally a subset of AA (with ι\iota the inclusion map).

General abstract

In terms of spans

If CC is a category with pullbacks, then a partial map from aa to bb may be defined to be a span

D i f A B\array{ & & D & & \\ & ^\mathllap{i} \swarrow & & \searrow^\mathrlap{f} & \\ A & & & & B }

where ii is monic. Such spans are closed under span composition, and as a locally full sub-2-category of Span(C)Span(C), the bicategory of partial maps in CC is locally preordered. In more down-to-earth terms, if (i,f)(i, f) and (i,f)(i', f') are partial maps from aa to bb, we have (i,f)(i,f)(i, f) \leq (i', f') if there exists (necessarily monic) jj such that i=iji = i' \circ j and f=fjf = f' \circ j.

Abstract bicategories of partial maps, parallel to bicategories of relations, were introduced by (Carboni 87).

In terms of the maybe monad

Notice that a partial function ff from AA to BB as above is (in classical mathematics) equivalently a genuine function from AA to the disjoint union (coproduct) of BB with the point (the singleton)

ϕ:AB*. \phi \;\colon\; A \longrightarrow B \coprod \ast \,.

The subset DAD \hookrightarrow A in the above is the preimage ϕ *(B)\phi^*(B); for xx in this preimage, f(x)=ϕ(x)f(x) = \phi(x). Conversely, an element xAx \in A is sent to *\ast by ϕ\phi if and only if ff is undefined at xx.

This in turn is equivalently a morphism in the Kleisli category of the maybe monad. Phrased this way, the concept of partial function makes sense in any category with coproducts and with a terminal object. It comes out as intended when the category is an extensive category (partial functions with complemented domain).

Examples

In secondary-school mathematics, one often makes functions partial by fiat, just to see if students can calculate the domains of composite functions and the like. This is not (only) busywork, as in applications one often has a function given by a formula that is really valid only on a certain domain. However, in more sophisticated analyses (such as those that Lawvere and his followers propose for physics and synthetic geometry), these domains and the total functions on them become the primary objects of study, with the partial functions being secondary (as ι\iota is seen as merely a way to place coordinates on DD).

In analysis, one often considers partial functions whose domains are required to be intervals in the real line, regions of the complex plane, or dense subsets of a Banach space.

In a field, the multiplicative inverse is a partial function whose domain is the set of non-zero elements of the field.

The category of sets and partial functions

The category Set partSet_part of sets and partial functions between them is important for understanding computation. However, one often replaces this with an equivalent category of sets and total functions.

Specifically, replace each set SS with the set S S_\bot of all subsets of SS with at most one element, otherwise known as the partial map classifier of Set. In this context, we identify an element xx of SS with the subset {x}\{x\} and write the empty subset as \bot. Then a partial function STS \to T becomes a total function S T S_\bot \to T_\bot such that inhabited subsets of TT are assigned only to inhabited subsets of SS. Then Set partSet_part is equivalent to the category Set Set_\bot of such sets and functions.

In classical mathematics S S⨿{}S_\bot \cong S \amalg \{\bot\}, although this is not true constructively. In this case, SS⨿{}S\mapsto S \amalg \{\bot\} is the maybe monad and Set Set_\bot is its Kleisli category. Moreover, since every algebra for this monad is free? this category is also equivalent to its Eilenberg-Moore category, which is the category Set *Set_* of pointed sets and total point-preserving functions. Traditionally, one uses the notation of Set Set_\bot but (unless one is a constructivist) thinks of this as simply different notation for Set *Set_*. It is still true constructively that SS S\mapsto S_\bot is a monad (the partial map classifier) and Set Set_\bot is its Kleisli category, but it is (probably) no longer true that every algebra is free.

For a more sophisticated analysis of computation, Set Set_\bot can be replaced with a suitable category of domains, such as directed complete partially ordered sets (DCPOs). The requirement that \bot be preserved can then be removed to model lazy computation, but now we are hardly talking about partial functions anymore.

Algebras of partial functions

The functions of high-school mathematics, consisting of real (or complex)-valued functions of one (or two or three) real (or complex) variables, are by default partial functions. As they take values in a field, one may consider adding or multiplying them. The usual rule is that dom(f+g)=domfdomg\dom(f + g) = \dom f \cap \dom g, etc, but this leads to an unusual algebra: a commutative semiring in which addition has an identity element (the always-defined constant zero function) and multiplication has an absorbing element (the never-defined empty function), but it fails to be a rig because these two elements are not the same. It has many other interesting properties, such as simultaneous additive and multiplicative idempotents (the zero functions with arbitrary domains).

An axiomatic treatment of such semirings may be found at the end of Richman 2012, as well as in the article category of partial endofunctions.

References

Last revised on January 28, 2024 at 04:41:57. See the history of this page for a list of all contributions to it.