A fibrational framework for possible-world semantics of \textsc{Algol}-like languages (Q879351): Difference between revisions

Reynolds and Oles [\textit{J. C. Reynolds}, ``The essence of ALGOL'', in: J. W. de Bakker et al. (eds.), Algorithmic languages. Proc. Int. Sympos. Algorithmic Languages, Amsterdam, 345--372 (1981; Zbl 0483.68001)] had shown how block-structured storage management in ALGOL-like languages can be explicated via functor categories \(\mathcal{W} \Rightarrow \mathcal{S}\), where \(\mathcal{W}\) is a category of ``worlds'' characterizing local aspects of storage structure and \(\mathcal{S}\) is a conventional semantic category of sets or domains. Every programming-language type \([\theta]\) is interpretd as a functor \([\theta] : \mathcal{W} \to \mathcal{S}\) and every programming-language term-in-context \(\pi \vdash X:\theta\) is interpreted as a natural transformation \([{\pi \vdash X:\theta}] : [{\pi \vdash X:\theta}]:[{\pi}] \dot\to [{\theta}]\). \textit{P. W. O'Hearn} and \textit{R. D. Tennent} [``Parametricity and local variables'', J. Assoc. Comput. Mach. 42, No. 3, 658--709 (1995; Zbl 0885.68039)] get a more precise analysis of block structure, using structures of the form \(\mathcal{W} \Rightarrow \mathcal{S}\), but \(\mathcal{W}\) and \(\mathcal{S}\) are now reflexive graphs. \textit{P. W. O'Hearn} and \textit{J. C. Reynolds} [``From ALGOL to polymorphic linear lambda-calculus'', J. ACM 47, No. 1, 167--223 (2000; Zbl 1094.68535)] use an alternative approach: the source language is translated into a polymorphic linear lambda-calculus which is then interpreted using a semantics with relational parametricity constraints. The paper under review uses the notion of fibration (alternatively fibred category) to express and compare these approaches. The use of fibrations is relevant for three reasons: 1. models of indexing by worlds; 2. categories of ``relations'' above categories; 3. models of polymorphic languages. Section 2, ``From functor categories to fibrations using slices'', starts by defining the fibration on \(\mathcal{W}\) whose fibres are functor categories, obtained from the functors \(\mathcal{W}\) and \(\mathcal{S}\). This is done by defining categories indexed on \(\mathcal{W}\), i.e. by defining a pseudo-functor \(S\) from \(\mathcal{W}^{\text{op}}\) to the category Cat of locally small categories and applying the Grothendieck construction. In the present situation, given \(\mathcal{W}\) and \(\mathcal{S}\), define the functor \(S: \mathcal{W}^{\text{op}}\to \text{Cat}\) as follows: for any world \(w\), the relevant fibre category \(S(w)\) is the category \((\mathcal{W}/w)^{\text{op}}\Rightarrow \mathcal{S}\) of all contravariant functors from \(\mathcal{W}/w \to \mathcal{S}\), where the slice category \(\mathcal{W}/w\) is defined as usually. This construction retains in \(S(w)\) information about the behaviour of any functor \(F: \mathcal{W}^{\text{op}}\to \mathcal{S}\) in possible future worlds derived from \(w\), given that we think of a morphism \(f: x \to w\) as a projection from an expanded world \(x\) to \(w\), the contravariant action of \(F\) on \(f\) being a ``logical weakening'' of the object to the expanded context. Proposition. For any small category \(\mathcal{W}\), if \(\mathcal{S}\) is Cartesian closed and complete, so is \((w)\) for every \(w \in \mathcal{W}\). The definition rendering \(S\) a functor is as usual. One obtains then (via the Grothendick construction) a split fibration on \(\mathcal{W}\). Proposition. If \(\mathcal{S}\) is complete and Cartesian closed, the fibration \(p:\text{Slices}({\mathcal W},{\mathcal S}) \to \mathcal{W}\) admits products; dually if \(\mathcal{S}\) is co-complete, it admits co-products. Obviously if \(\mathcal{W}\) has a terminal object 1, the functor category \(\mathcal{W}^{\text{op}}\to \mathcal{S}\) is equivalent to the fibre over 1. More generally: Proposition. For any \(\mathcal{W}\), the functor category \(\mathcal{W}^{\text{op}}\to \mathcal{S}\) is equivalent to the category of Cartesian sections of \(p :\text{Slices}(\mathcal{W}, \mathcal{S}) \to \mathcal{W}\); that is, all functors \(s: \mathcal{W} \to {\text{Slices}(\mathcal W,\mathcal S)}\) such that \(s\circ p= \text{id}_\mathcal{W}\) and for every \(\mathcal{W}\)-morphism \(f\), \(s(f)\) is cartesian. Section 3, ``Relations'', studies, via several examples, how to impose relation-preservation constraints on objects and morphisms analoguous to the ``parametric'' functors and natural transformations of [O'Hearn and Tennent, loc. cit.]. Section 4, ``Categories of worlds and relations'', presents categories of worlds and relations that have been used in programming-language semantics as fibrations. Section 5, ``Discussion'', gives a brief discussion of some properties and different approaches of the previous sections. Appendix A, ``A relational setting for polymorphism'', sketches how a fibration Fib provides a categorical model of ``logical relations'' over a polymorphic lambda calculus. Appendix B, ``Proofs'', gives proofs of propositions that were omitted in the body of the paper. Appendix C, ``Fibrations over fibrations'', discusses fibrations in Fib.