Realizability models allow to define categories with very rich mathematical structure starting from untyped computational models, typically partial Combinatory Algebras (pCAs). We propose a generalization of realizability models, in which pCAs are replaced by monoids of maps (on a set of data), which allow to consider also restricted computational models, where complexity constrains can be taken into account (e.g., the monoid of maps on bit strings computable in linear time). We give some examples of monoids (on bit strings) based on complexity classes, and state how the mathematical structure of these categories relates to properties of the corresponding monoid.
This communication is related to a journal submission, which proposes categories where one can
interpret calculi for collection types (aka bulk types), like those in [
Realizability Models and Complexity Theory. The way realizability models use Category Theory
in relation to Computability Theory works as follows: 1) one starts from a computational model,
typically a pCA (, · ), where the elements of can be interpreted as data or programs and the binary
application · (when defined) returns the output produced by executing program with input ;
2) then one defines a category using the pCA; 3) and finally one studies how category-theoretic
properties of relate to properties of the pCA. The seminal example of this approach is in [
Lextensive categories have finite limits (in particular products) and well-behaved finite sums, where the
definition of well-behaved is formalized by the notion of extensive category (see [
The theorem above implies that a satisfying the assumption is (equivalent to) a lextensive sub-category of S, which contains the category S of finite sets as a full lextensive sub-category.
The rational for considering lextensive categories is that in them one can define • an object of booleans, namely 2 =Δ 1 + 1 • decidable predicates1 on an object , i.e., arrows > 2 • when an object has a decidable equality, i.e., a (necessarily unique) arrow : × > 2 classifying the diagonal sub-object ⊂ > × .
In a lextensive category some objects may not have a decidable equality, The following constructions define lextensive full sub-categories of , where all objects have a decidable equality. Theorem 2.2. If is lextensive, let be the full sub-category of the objects ∈ with a decidable equality, then is a lextensive sub-category of .
Theorem 2.3. If is lextensive and ∈ has a decidable equality and the objects 1, + and × are retracts of , let P[] be the full sub-category of consisting of the decidable sub-objects2 of , then P[] is a lextensive sub-category of .
In a lextensive category, where all objects have a decidable equality, one can interpret a typed language, where the BNF for types is : : = | 0 | 1 | 1 + 2 | 1 * 2 | {: |}, with base type and boolean formula (or equivalently a term of type 1 + 1). A possible BNF for boolean formulas is : : = ⊤ | 1 = 2 | 1 ∧ 2 | ¬, with 1 and 2 terms of the same type. Note that the last clause {: |} in the BNF for types means that the language has dependent types.
2Alternatively decidable predicates on .
We introduce the category of assemblies A[] for a sub-monoid of the monoid → of total
maps on a set , and some of its full sub-categories. The aim is to provide realizability-like models for
low-complexity Domain Specific Languages (DSL), where is the set of data manipulated by programs
in the DSL, and are the maps computed by such programs. The idea (following [
The faithful forgetful functor from A[] to S maps to ||.
Remark 3.2. If is a sub-monoid of → , then one can define a computability structure C with
one datatype and the set of relations C(, ) consisting of the graphs of maps in . In this way
A[] coincides with the category of assemblies for the computability structure C [
Example 3.3. Examples of monoids on the set N of natural numbers are: 1. the set TR of total recursive maps 2. the set PR of primitive recursive maps 3. the set E of maps in the -th level of Grzegorczyk hierarchy.
The following inclusions hold: E ⊂ E+1 ⊂ ⋃︀ E = PR ⊂ TR. E3 coincides with the set of Kalmar elementary maps, that are defined without using bounded recursion.
Before giving examples of monoids on the set * of bit-strings, where = {0, 1}, we recall some
notions and results from Computational Complexity (see [
Definition 3.4. If : * → * and : N → N (monotone and ≥ 1), then
Δ 1. ∈ () ⇐⇒ the map ↦→ max||≤ | ()| is in ()
Δ 2. ∈ () ⇐⇒ there is a TM computing and working in time ()
Δ 3. ∈ () ⇐⇒ there is a TM computing and working in space ()4. 3We assume that a TM computing a partial map on * has one read-only input tape (where the input is written before the computation starts), one write-only output tape (where the output is written before the end of the computation), several working tapes (on which may use symbols from a larger alphabet ⊇ ). 4For space complexity only the cells on working tapes used in the computation count, the cells on the read-only input tape and the write-only output tape are ignored.
LO = () ⊃
LS = () ∩ LO ⊃
LT = ()
The output classes contain also non-computable maps, but they are useful in combination with the classes defined in terms of Turing Machines. For instance, the class () is not closed under composition when > 1, while () ∩ () is a sub-monoid of * → * . We recall well-known inclusions between diferent types of complexity classes (see [8, Thm 9.4]): () ⊆ () ∩ () and () ⊆ ⋃︁ ( * ()) >0 Lemma 3.5. If all maps , , : N → N are monotone, then the following hold: 1. If ∈ () for = 1, 2, then ∃ > 0.2 ∘ 1 ∈ (2( * 1())). 2. If ∈ () ∩ () for = 1, 2, then
∃ > 0.2 ∘ 1 ∈ (1() + 1() + 2( * 1())). 3. If ∈ () ∩ () for = 1, 2, then
∃ > 0.2 ∘ 1 ∈ (1() + log 1() + 2( * 1())).
Example 3.6. By Lemma 3.5, the subsets in Figure 1 are sub-monoids of * → * . We consider two remarkable full sub-categories of A[]: M[] of modest sets and P[] of predicates. Definition 3.7 (Special assemblies).
Given an assembly ∈ A[] we say that Δ 1. is a modest set ( ∈ M[]) ⇐⇒ ⊢ is the graph of a partial surjective map from to | |.
Δ 2. is a predicate ( ∈ P[]) ⇐⇒ | | ⊆ and ⊢ is the identity relation Δ|| on | |. M[] is replete (i.e., an assembly isomorphic in A[] to a modest set is a modest set) and essentially small, because it is equivalent to the small category of PERs (Partial Equivalence Relations) on . P[] is small, but not replete. However, one can modify the definition of P[] to make it replete. The following properties of imply that A[], M[] and P[] satisfy the assumptions of Thm 2.1. Definition 3.8. Given a sub-monoid ⊆ → we consider the properties: K has at least two elements (say 0 and 1) and : . ∈ for every ∈ P there is a map : 2 → and two maps 0, 1 ∈ s.t.
• ((0, 1)) = for every 0, 1 ∈ • : .(0, 1) ∈ for every 0, 1 ∈ E there is a map ∈ s.t. (((0, 1), (2, 3))) = (2 if 0 = 1 else 3).
Property (P), i.e., encoding of pairs, is needed to express (E), i.e., equality testing; (K) and (P) implies that is infinite. All monoids in Examples 3.3 and 3.6 satisfy properties (K,P,E).
Theorem 3.9. If a sub-monoid ⊆ → has properties (K,P,E), then: 1. A[], M[] and P[] are lextensive categories, and Γ is lextensive. 2. In P[] every object has a decidable equality. 3. The forgetful functor : A[] > S is isomorphic to Γ.
4. A map is epi in A[] (M[] or P[]) ⇐⇒ Γ is epi in S.
When ̸= ∅, the following relations among categories hold, where ⊣ means “F left-adjoint to ” Moreover, under the assumptions of Theorem 3.9, one has the following lextensive functors, where S is the category of countable sets. Moreover, P[] and M[] are equivalnet to S when = → with countable.
> S ⊂ S ⊂ ∩ ∨ P[] ⊂ > S ∧ > M[] ⊂ > A[] If has finite products, then one can ask whether has a NNO 1 > > or a list monad L, given by the adjuntion between and the category of monoids in (in this case L1 is a NNO). 0 Theorem 3.10. If a sub-monoid ⊆ → has properties (K,P,E) and is closed under primitive recursion, then A[], M[] and P[] have a parametric NNO and a strong list monad L. Among the monoids in Example 3.3 and 3.6 only TR and PR are closed under primitive recursion, in all other cases the category A[] (M[] and P[]) fails to have a NNO (and consequently a list monad). A lex sub-category of S may have a NNO-structure 1 0 > > , which does not have the universal property of a NNO in , but it does in S. In this case we say that the structure behaves like a NNO. Similarly, we say that a (strong) monad L on behaves like a list monad, when it is the restriction of a list monad on S. Since structures satisfying a universal property are unique up to (unique) isomorphism, NNO-structures in that behave like a NNO are isomorphic in S, but may fail to be isomorphic in . However, some of these unique isomorphisms in S are morphisms in , thus these structures form a preorder. For instance, in P[], where is any of the monoids in Figure 1, the unary and binary encodings, N1 and N2, of the natural numbers behave like a NNO. However, only the isomorphism from N1 to N2 in S is a morphism also in P[].
It is relatively easy to prove (basically an encoding exercise), that for all in Examples 3.3 and 3.6 the category A[] (M[] and P[]) have structures that behave like a NNO and like a list monad, with the caveat that for the monoid LO and its sub-monoid LS and LT, the obvious monad L behaving like a list monad is not strong, i.e., it does not have a tensorial strength 1 × L(2) > L(1 × 2). Declaration on Generative AI