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.
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 formula_1 where formula_2 is the output (if defined) of the Turing machine represented by the integer formula_3 when run on the input formula_4 (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.
Definition.
Let formula_5 be a fixed partial combinatory algebra.
An assembly formula_6 (over formula_5) is simply a set formula_8 equipped with a relation formula_9, read “realizes”, between formula_5 and formula_8, such that every element of formula_8 has a realizer, i.e., for all formula_13, there exists formula_14 with formula_15.
Assemblies are equipped with a categorical structure as follows. A morphism formula_16 between assemblies formula_6 and formula_18 is a function formula_19 between their underlying sets, for which there exists an element formula_3 such that for all element formula_13 realized by formula_14, the application formula_23 is defined in the pca formula_5 and the element formula_25 is realized by formula_23. The category of assemblies over formula_5 is denoted by formula_28.
An assembly formula_6 is said to be modest when elements do not share realizers, i.e., for all formula_30, if formula_15 and formula_32 then formula_33. The category of modest assemblies over formula_5 is denoted formula_35 and is a full subcategory of formula_28.
Examples.
The "unit assembly" formula_37 is carried by a singleton formula_38, where formula_39 is realized all elements of the pca (alternatively, giving formula_39 any non-zero number of realizers gives an isomorphic object).
The "empty assembly" formula_41 is carried by the empty set.
The "assembly of natural numbers" is carried by formula_1 where each natural number formula_43 is realized only by its associated Curry numeral formula_44.
At the extreme opposite of modest assemblies, the "constant assembly" formula_45 is carried by the set formula_46, where all elements of formula_46 are realized by all elements of the pca.
The assembly of "classical truth values" is the constant assembly on a two-element set, i.e., formula_48. The assembly of "decidable truth values" or "booleans", is carried by formula_49, where 0 is realized by formula_50 and 1 is realized by the formula_51.
An intermediate between decidable and classical truth values is the assembly of "semidecidable truth values". It is carried by formula_49, and all realizers are programs which compute infinite sequences of bits, i.e., elements formula_3 from the pca such that for all formula_43 the application formula_55 is defined and has value formula_50 or formula_51. The realizers of 1 are those which compute a sequence that contains the bit 1, and the realizers of 0 are the others.
Given two assemblies formula_6 and formula_18, we may form their "binary product" formula_60 as follows: its carrier is the Cartesian product of the carriers formula_61, and a pair formula_62 is realized by elements formula_3 such that formula_64 realizes formula_65 and formula_66 realizes formula_67. Here, formula_68 and formula_69 are the projection functions in some encoding of pairs inside the pca, e.g., formula_70.)
We may also form the "binary coproduct" formula_71, whose carrier is the disjoint union formula_72 and where a realizer of formula_73 is formula_74 for formula_65 a realizer of formula_76, while a realizer of formula_77 is formula_78 for formula_67 a realizer of formula_77. Here, formula_81 and formula_82 are the constructors for some encoding of disjoint unions, e.g., formula_83.
Categorical structure.
The category formula_28 has the following properties: