D IAGRAMMES Y VES L AFONT Primitive recursive categories and machines Diagrammes, tome 22 (1989), p. 7-13 © Université Paris 7, UER math., 1989, tous droits réservés. L’accès aux archives de la revue « Diagrammes » implique l’accord avec les conditions générales d’utilisation (http://www.numdam.org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright. Article numérisé dans le cadre du programme Numérisation de documents anciens mathématiques http://www.numdam.org/ VOLUME DIAGRAMMES ACTES DES JOURNEES N are primitive recursive. • If / i , . . . , / p : N n - » N and g : Np—>N are primitive recursive, then the function h : N n -> N such that h(u) = g(fi(u),...Jp(u)) is also primitive recursive. Notation: h = g o ( / i , . . . , / p ) (substitution). • The constant zéro 0 : N° —* N and the successor function S : N —• N are primitive recursive. • If / : N n —+ N et g : N 2 + n —• N are primitive recursive, then the function h : N 1 + n -* N such that h(0,u) = /(u) /i(Sar,w) = g(x,h(x,u),u) is also primitive recursive. Notation: /i = Rec(/, #) (primitive recursion). This class is very big indeed: the reader can check that ail usual arithmetical functions are primitive recursive, for example: plus(0,y) times(0,2/) fact(O) = = = y 0 SO plus(Sx,y) times(Sx,y) fact(Sx) = = = S(plus(x,î/)) plus(times(x, ?/), y) times(fact(:r),S:c) L e m m a 1 (encoding tuples) For ail n > 0, there are primitive recursive functions 7 : N n - + N and 7T1,. ..,7r n : N -* N such that x* O 7 = IP for i = 1,.. . , n . Define 7(2:1,^2,^3,...) = 2 r i 3 X 2 5 X 3 . . . which is obviously primitive recursive. Proving that the corresponding 7T 1 ,... ,7rn : N —• N are also primitive recursive is a bit harder (see [Kleene]). Primitive recursive functions are traditionally introduced to define the gênerai recursive functions, i.e. the ones that are computable, at least in theory. But we shall not consider them from this viewpoint. 2 Primitive Recursive Catégories In the category of sets, and more generally in a topos, the object of natural numbers N is characterised by the axiom of Lawvere: 1 —• N •— N is initial among the diagrams 1 —> A <— A (where 1 is the terminal object). In other words, for any such diagram, there is a unique lter(^, 0) : N —• A such that the following diagram commutes: ter(v?,T/>) However, this notion, which is a spécial case of Kan extension, is to weak to capture primitive recursion in catégories which are not Cartesian closed, and since primitive recursion has nothing to do with functionality (i.e. existence of exponentials), we need a stronger axiom: A primitive recursive category is a category with finite products and a parametrised object of natural numbers 1 —• N <— N . So for each object A, there is a unique () : X —*• 1, and for each diagram B < t— AA — —*C Cthere thereis is a unique (, ip) : N x B —• A such that the following diagram commutes: N x B^ — N xB (Rec(^^),n2) Rec(c^,i/;) il> •AxB In particular B = 1 gives the axiom of Lawvere. The structure of primitive recursive category with explicit choice of products and object of natural numbers is obviously (projectively) sketchable (although not algebraic over graphs, see [CopLair]). Consequently, there is a free primitive recursive category V, and a canonical functor T : V —» Set, since *Se£ is clearly a primitive recursive category. Using lemma 1, it is quite easy to see that the J-(N in V are precisely the primitive recursive functions. Note that, by standard diagonalisation arguments, T is neither full (for example, Akermannn's function is not primitive recursive) nor faithful1 (some primitive recursive algorithms are extensionally equal although distinct in V). 3 Getting rid of Cartesian products Although primitive recursive functions are explicitly defined in terms of projections and substitution, there are good reasons (see [Burroni]) to interpret this notion in catégories that are not necessarily Cartesian. A Burroni category2 is just a category with an object of natural numbers B - £ MB <£ MB over each object B: for any diagram B -£ A 2- A, there is a unique lter(,^) TL lter(y>,^) - A A primitive recursive category is clearly a Burroni category with MB = N x B . The converse is false, since nothing forces a Burroni category to be Cartesian (consider for example a discrète category with two points), and even if it is, MA may hâve nothing to do with Ml X A (as it is the case in the dual category of Set). However, we hâve the quite surprising fact: T h e o r e m 1 [Burroni] The free Burroni category B[X] over one object X admits fxnite products. Since the objects of B[X] are of the form MnX for n 6 N , we guess that the terminal object is M°X = X and MPX X MqX = Arp+<*X. But of course, the main point of the proof is to construct ail required morphisms. Corollary 1 The category B[X] is équivalent to V. 1 2 There is an élégant proof of this in [Burroni], using Matijasevic's Theorem. This is called a Peano-Lawvere category in [Burroni]. 10 There are indeed two canonical functors $ : B[X] -* V such that $ X = 1 and \p - -p-+ B[X]. It is easy to see that # o $ is the identity functor on B[X], and $ o $ is naturally isomorphic to the identity on V. Corollary 2 If G is the canonical functor B[X\—• Set such that QX = 1, fAe (7(v?) /or y? : MPX —• -/VX in 5[-ï] are precisely the primitive recursive functions. Thèse results express that B[X] is the category of formai primitive functions. 4 recursive From catégories to machines Following Lambek's terminology, morphisms in the free catégories V and B[X] are syntacticly described as équivalence classes of categorical combinators. Thèse combinators are truly programs written in a very low level language for a machine we shall describe precisely, at least in the case of B[X]. One major différence between V and B[X] is the structure of types (or objects). In V, types are trees and data should be represented similarly: X / \ x / Nv \ \ N / N / N \ S S I I S 0 0 0 In B[X], the corresponding type would be MMMX and the datum SSSOSOSSSSO, which can be implemented as a stack on a computer, whereas trees would require pointers, with usual problems of memory allocation and garbage collection. Theorem 2 [Burroni] Every morphism X -> MX in B[X] is of the form S n o 0 for some n G N . More generally, every morphism X —» MPX is of the form S 0 . . . 0 S 0 O 0 . . . 0 S 0 . . . 0 S^oQ ni times for some (n\,..., np times n p ) in N p . 11 (standard tuple) This resuit can be proved elegantly by applying the uni versai property of B[X] to the gluing of B[X] and Set along the functor A »-> Hom(X, A). Alternatively, it is enough to check: L e m m a 2 If

, VO : pop S until you reach 0 , pop 0, exécute y?, and exécute ip as many times as you popped S. On usual computers, the code is a séquence of instructions followed by Return. Hence Id will be compiled into an empty séquence,