Assembly (realizability)

In theoretical computer science and mathematical logic, assemblies can be informally described as sets equipped with representations for elements. Realizability toposes are completions of assembly categories.

Motivation

Algorithms do not directly manipulate objects such as graphs or lists, but representations of these objects. There may be several types of representations available. For example, graphs (viewed modulo isomorphism, i.e., two isomorphic graphs are the same) may be represented with adjacency lists or adjacency matrices. Furthermore, a given object may have several equivalent representations, e.g., a graph could be presented with any order of the vertices, and graph algorithms should give equivalent results whatever the order of the vertices in the input is. The basic idea behind assemblies is to consider sets (such as the set of finite graphs, modulo isomorphism) where each element has a number of realizers, which are understood as its algorithmic representations. A morphism between assemblies is a function between their underlying sets which can be “algorithmically realized”, in the sense that given a representation of an element of the domain, one can compute a representation of its image. For example, the function which maps a graph to the multiset of its connected components is realized: there is an algorithm which, given a representation of a graph, computes a list (which is a reasonable representation for a multiset) of representations of its connected components.Template:R

In the context of realizability, it is useful not to restrict the definition to algorithms in the Church–Turing sense. Instead, assemblies are defined over a specific partial combinatory algebra, which abstracts the model of computation. It is a set equipped with an operation thought of as program execution. The archetypal example, modelling Church–Turing computability, is the first Kleene algebra, which is $\mathbb{N}$ where $px$ is the output (if defined) of the Turing machine represented by the integer $p$ when run on the input $x$ (thus integers are used to represent all data as well as all programs).

A possibly surprising aspect of the definition is that elements may share realizers. While unusual algorithmically, this is important to the logical side of realizability.Template:R

Definition

Let $A$ be a fixed partial combinatory algebra.

An assembly $S$ (over $A$) is simply a set $|S|$ equipped with a relation ${⊩}_S$, read “realizes”, between $A$ and $|S|$, such that every element of $|S|$ has a realizer, i.e., for all $s\in |S|$, there exists $a\in A$ with $a{⊩}_{S}s$.Template:RTemplate:R

Assemblies are equipped with a categorical structure as follows. A morphism $f:S\to T$ between assemblies $S$ and $T$ is a function $f:|S|\to |T|$ between their underlying sets, for which there exists an element $p$ such that for all element $s\in |S|$ realized by $a\in A$, the application $pa$ is defined in the pca $A$ and the element $f(s)\in |T|$ is realized by $pa$. The category of assemblies over $A$ is denoted by $\mathrm{Asm}(A)$.Template:RTemplate:R

An assembly $S$ is said to be modest when elements do not share realizers, i.e., for all $s,s^{\prime }\in S,a\in A$, if $a{⊩}_{S}s$ and $a{⊩}_S{s}^{\prime }$ then $s=s^{\prime }$. The category of modest assemblies over $A$ is denoted $\mathrm{Mod}(A)$ and is a full subcategory of $\mathrm{Asm}(A)$.Template:R

Examples

The unit assembly $1$ is carried by a singleton $\{\star \}$, where $\star$ is realized all elements of the pca (alternatively, giving $\star$ any non-zero number of realizers gives an isomorphic object).Template:R

The empty assembly $0$ is carried by the empty set.Template:R

The assembly of natural numbers is carried by $\mathbb{N}$ where each natural number $n$ is realized only by its associated Curry numeral $\overline{n}$.Template:R

At the extreme opposite of modest assemblies, the constant assembly $\mathrm{\nabla }X$ is carried by the set $X$, where all elements of $X$ are realized by all elements of the pca.Template:R

The assembly of classical truth values is the constant assembly on a two-element set, i.e., $\mathrm{\nabla }\{0,1\}$. The assembly of decidable truth values or booleans, is carried by $\{0,1\}$, where 0 is realized by $\overline{0}$ and 1 is realized by the $\overline{1}$.Template:R

An intermediate between decidable and classical truth values is the assembly of semidecidable truth values. It is carried by $\{0,1\}$, and all realizers are programs which compute infinite sequences of bits, i.e., elements $p$ from the pca such that for all $n$ the application $p\overline{n}$ is defined and has value $\overline{0}$ or $\overline{1}$. The realizers of 1 are those which compute a sequence that contains the bit 1, and the realizers of 0 are the others.Template:R

Given two assemblies $S$ and $T$, we may form their binary product $S\times T$ as follows: its carrier is the Cartesian product of the carriers $|S|\times T$, and a pair $(a,b)\in |S|\times |T|$ is realized by elements $p$ such that $𝖿𝗌𝗍p$ realizes $a$ and $𝗌𝗇𝖽p$ realizes $b$. Here, $𝖿𝗌𝗍$ and $𝗌𝗇𝖽$ are the projection functions in some encoding of pairs inside the pca, e.g., $𝗉𝖺𝗂𝗋:=⟨xyz⟩zxy,𝖿𝗌𝗍:=⟨p⟩p(⟨xy⟩x),𝗌𝗇𝖽:=⟨p⟩p(⟨xy⟩y)$.)Template:R

We may also form the binary coproduct $S+T$, whose carrier is the disjoint union $|S|\bigsqcup |T|$ and where a realizer of $s\in S$ is $𝗂𝗇𝗅a$ for $a$ a realizer of $s$, while a realizer of $t$ is $𝗂𝗇𝗋b$ for $b$ a realizer of $t$. Here, $𝗂𝗇𝗅$ and $𝗂𝗇𝗋$ are the constructors for some encoding of disjoint unions, e.g., $𝗂𝗇𝗅:=⟨x⟩𝗉𝖺𝗂𝗋\overline{0}x,𝗂𝗇𝗋:=⟨x⟩𝗉𝖺𝗂𝗋\overline{1}x$.Template:R

Categorical structure

The category $\mathrm{Asm}(A)$ has the following properties:

• It is finitely complete. The unit assembly is a terminal object. Binary products correspond to category-theoretic binary products. The equalizer of two morphisms $f,g:S\to T$ may be formed exactly as in the category of sets, as the canonical injection to $|S|$ from the subset $\{s\in |S||f(s)=g(s)\}$. Each element of the subset is equipped with the same realizers as in $S$, and the canonical injection is realized by $i:=⟨x⟩x$.Template:RTemplate:R
• It is finitely cocomplete. The empty assembly is initial and binary coproducts correspond to category-theoretic binary coproducts. Similarly to equalizers, the coequalizer of two morphisms $f,g:S\to T$ may be formed exactly as in the category of sets, as the canonical surjection from $|S|$ to the quotient $S/\equiv$, where $\equiv$ is the equivalence relation generated by the relations $f(s)\equiv g(s),s\in S$. The realizers of an equivalence class are all the realizers of its elements in $S$. Again, the canonical surjection is realized by $i:=⟨x⟩x$.Template:RTemplate:R
• It is regularTemplate:RTemplate:R and cartesian closed.Template:RTemplate:R
• A morphism is mono if and only if its underlying function is injective, and epi if and only if its underlying function is surjective.Template:RTemplate:R