A non-uniform finitary relational semantics of system \(T\) (Q2842243)

This work concerns a finitary relational interpretation of Gödel's system \(T\). The author employs a lazy, nonflat interpretation of natural numbers which enables him to define a finitary recursion operator in the category deduced from the relational model of linear logic -- this is the main result of the paper (Theorem 4.8). In doing so, he extends previous work of \textit{T. Ehrhard}, where a restricted form of recursion was addressed, namely tail-recursive iteration [Math. Struct. Comput. Sci. 15, No. 4, 615--646 (2005; Zbl 1084.03048)]. Furthermore, by use of a notion of uniformity which expresses boundedness of information on the input, he provides semantic evidence for a result of \textit{M. Parigot}, according to which iteration cannot support the definition of the predecessor function like recursion does in system \(T\) [Lect. Notes Comput. Sci. 440, 309--321 (1990; Zbl 0925.03149)]. The author regards his work as part of a general attempt to extend \textit{J.-Y. Girard}'s quantitative semantics of lambda calculus in vectorial finiteness spaces [Ann. Pure Appl. Logic 37, No. 2, 129--177 (1988; Zbl 0646.03056)] to functional programming with base types [\textit{L. Vaux}, Math. Struct. Comput. Sci. 19, No. 5, 1029--1059 (2009; Zbl 1186.03025); \textit{C. Tasson}, Lect. Notes Comput. Sci. 5608, 325--340 (2009; Zbl 1246.03081)].NEWLINENEWLINENEWLINEAfter a detailed introduction, Section 2 starts by recounting the basics of the categories \( \mathbf{Rel} \) and \( \mathbf{Fin} \). The objects of \( \mathbf{Rel} \) are sets and its arrows are multirelations, that is, relations between finite multisets and sets. The category \( \mathbf{Fin} \) is more intricate. For a given set \( A \) and a collection \( \mathfrak{F} \) of subsets of \( A \), collect in \( \mathfrak{F}^\bot \) these subsets of \( A \) which have a finite intersection with every element of \( \mathfrak{F} \); it is \( \mathfrak{F} \subseteq \mathfrak{F}^{\bot\bot} \). A \textit{finiteness structure on \( A\)} is an \( \mathfrak{F} \) with the additional closure property that \( \mathfrak{F}^{\bot\bot} \subseteq \mathfrak{F}\). A \textit{finiteness space} then is a pair \( \mathcal{A} = ( |\mathcal{A}| , \mathfrak{F} (\mathcal{A})) \) where \( |\mathcal{A}| \) is a set and \( \mathfrak{F} (\mathcal{A}) \) is a finiteness structure on \( |\mathcal{A}| \). A \textit{finitary multirelation} between two finiteness spaces \(\mathcal{A}\) and \(\mathcal{B}\) is a multirelation between \(|\mathcal{A}|\) and \(|\mathcal{B}|\) which, for every \(a \in \mathfrak{F}(\mathcal{A})\), maps the finite multisets of \(a\) into \(\mathfrak{F}(\mathcal{B})\) and the inverse image of every singleton subset of \(|\mathcal{B}|\) has a finite intersection with the finite multisets of \(a\) (in the words of the author, ``the preimage of a singleton is \textit{anti-finitary}''). Finiteness spaces together with finitary multirelations between them form the category \(\mathbf{Fin}\). Both \(\mathbf{Rel}\) and \(\mathbf{Fin}\) are Cartesian closed, but only the first is cpo-enriched; indeed, \(\mathbf{Fin}\) is not meant to accommodate all fixpoint operators, as they generally cannot afford a finitary interpretation, and thus, by design, aims lower than modeling Plotkin's \(\mathrm{PCF}\).NEWLINENEWLINENEWLINEIn Section 3, the relational semantics of a generic typed \(\lambda\)-calculus with products is given and is proved invariant under standard conversions (Theorem 3.1). Moreover, it is shown that the interpretation works within \(\mathbf{Fin}\) (Theorem 3.2). After an overview discussion of the internal languages of \(\mathbf{Rel}\) and \(\mathbf{Fin}\), Gödel's \(T\) is recalled in three versions, whose mutual relations are discussed: the version with an \textit{iterator} \(\mathsf{I}\) for each type \(\mathsf{Nat} \to (A \to A) \to A \to A\) with the rules NEWLINE\[NEWLINE \mathsf{I}\;0\;u\;v = v, \quad \mathsf{I}\;(St)\;u\;v = u (\mathsf{I}\;t\;u\;v) , NEWLINE\]NEWLINE the one with a \textit{recursor} \(\mathsf{R}\) for each type \(\mathsf{Nat} \to (\mathsf{Nat} \to A \to A) \to A \to A\) with the rules NEWLINE\[NEWLINE \mathsf{R}\;0\;u\;v = v, \quad \mathsf{R}\;(St)\;u\;v = u t (\mathsf{R}\;t\;u\;v) , NEWLINE\]NEWLINE and one with a \textit{tail-recursive iterator} \(\mathsf{J}\) for each type \(\mathsf{Nat} \to (A \to A) \to A \to A\) with the rules NEWLINE\[NEWLINE \mathsf{J}\;0\;u\;v = v, \quad \mathsf{J}\;(St)\;u\;v = \mathsf{J}\;t\;u\;(u v) . NEWLINE\]NEWLINE It is explained why the interpretation of \(\mathsf{J}\) as done in [Ehrhard, loc. cit.] cannot work for \(\mathsf{I}\) or \(\mathsf{R}\) in \(\mathbf{Rel}\) and \(\mathbf{Fin}\).NEWLINENEWLINENEWLINEThe explanation carries over to Section 4, where it is made clearer that the handicap of the interpretation of \(\mathsf{J}\) à la Ehrhard is due to the \textit{strictness} of the denotation of the successor. The author instead chooses to interpret \(\mathsf{Nat}\) by \textit{lazy natural numbers}, namely by a finiteness space \(\mathcal{N}_l\) where the carrier, besides the (total) natural numbers \(k\), contains also \textit{partial numbers} \(k^>\), and the finiteness structure is taken to consist of all finite subsets of the carrier. In this model, the successor is interpreted as mapping the empty multiset \([\,]\) to the first partial number \(0^>\), and then, roughly speaking, every \(k\) to \(k+1\) and every partial \(k^>\) to the partial \((k+1)^>\). With this understanding of successor, the author proceeds to obtain recursion operators as fixpoints of appropriate step operators; these fixpoints turn out to be finitary (Theorem 4.8). Thus, a finitary relational model of system \(T\) is obtained.NEWLINENEWLINENEWLINESection 5 discusses the relation between iteration and recursion in the relational model. Firstly, the finitary interpretation of \(\mathsf{I}\) and consequently the existence of a weak natural numbers object in \(\mathbf{Rel}\) and \(\mathbf{Fin}\) are established. A set of lazy numbers is called \textit{uniform} if it is bounded by some number, meaning that it is a subset of the latter's downward closure. It is shown that iterators consider only uniform (supports of multi-) sets of lazy numbers (Lemma 5.4), a property that the recursors in \(\mathbf{Rel}\) generally evade -- hence, the title of the article (Lemma 5.5). Based on this last observation, it is further argued that, for the version of system \(T\) with iterators, no term of the form \(\lambda_x t\) can be a valid implementation of recursion, under certain hypotheses for \(t\) -- for example if all occurrences of \(x\) in \(t\) appear as \(\mathsf{I} x\) (Corollary 5.10). These remarks show that even the usual implementation of \(\mathsf{R}\) in terms of \(\mathsf{I}\) and pairing must fail in the relational model, thus echoing Michel Parigot's results on a semantical basis.NEWLINENEWLINEThe paper ends with a discussion of related and future work.