id: 05541585
dt: b
an: 05541585
au: van Oosten, Jaap
ti: Realizability. An introduction to its categorical side.
so: Studies in Logic and the Foundations of Mathematics 152. Amsterdam:
    Elsevier (ISBN 978-0-444-51584-1/hbk). xvi, 310~p. EUR~125.00 (2008).
py: 2008
pu: Amsterdam: Elsevier
la: EN
cc: 
ut: effective topos; tripos; partial combinatory algebra; partial recursive
    functions; realizability topos; assemblies; arithmetic; set theory;
    synthetic domain theory; axiomatic computability theory; geometric
    morphism
ci: Zbl 0651.18004; Zbl 0762.18001
li: 
ab: This book aims at beginning researchers in the field of realizability and
    so emphasizes technical tools rather than any overview of methods or
    results. The central object here which created the categorical approach
    to realizability is Martin Hyland’s effective topos called Eff. The
    author advises that readers interested in getting directly to that
    topos can skip Chapter 1 and will only need “some parts of Chapter
    2” (p. xii). However, that opening material will be needed for any
    research career on this and other realizability toposes. The reader is
    assumed to know some amount of general category theory as well as to
    have an “acquaintance with the notion of a topos” (p. vi).  The
    tools are presented very clearly and this is especially advantageous
    for the idea of a tripos. The standard reference on triposes has been
    {\it Andrew Pitts}’s 1982 Ph.D. dissertation [The theory of triposes.
    Cambridge: Univ. Cambridge (1982)]. Considerable simplification has
    been possible since that pioneering work. This book gives a very clear
    exposition and should become the reference.  Chapter 1 deals with the
    idea of a partial combinatory algebra or pca and gives a dozen kinds of
    examples. The paradigm pca is the set of natural numbers, regarded as
    codes of partial recursive functions, so that one natural number $n$
    may or may not have a defined value when applied as a partial recursive
    function to another number $m$. The most obvious variants use partial
    recursive functions relative to some oracle. Other variants use other
    models of computation or of data types. This chapter gives clear proofs
    of various standard theorems showing to what extent certain kinds of
    pcas share classical features of the partial recursive functions. 
    Chapter 2 explains the idea of a tripos and shows a canonical
    construction on any tripos which produces a topos, with the internal
    logic of that topos closely related to the tripos. Then Chapter 2 shows
    how each pca gives a tripos, with the corresponding topos called a
    realizability topos. That term comes from the way an element $a$ of a
    pca may realize a formula $φ$ in the logic of the tripos or the topos,
    in the rough sense that $a$ encodes calculations or data which show
    $φ$ is true.  Chapter 3 on the effective topos Eff is half of the
    book. It recapitulates the necessary material from Chapter 2 so it is
    relatively self-contained. Indeed, this chapter briefly describes Eff
    directly in terms of assemblies but treats this only as a theorem and
    does not mention that it suffices as a rigorous definition of the topos
    independent of the tripos machinery. Assemblies and this construction
    were introduced by {\it A. Carboni, P. J. Freyd} and {\it A. Scedrov}
    [Lect. Notes Comput. Sci. 298, 23‒42 (1988; Zbl 0651.18004)]; and
    some corrections are in the reviewer’s book [Elementary categories,
    elementary toposes. Oxford: Clarendon Press (1992; Zbl 0762.18001), pp.
    229‒239].  The chapter develops first-, second-, and third-order
    arithmetic in Eff. The first-order part coincides with classical Kleene
    realizability and notably it verifies a strong version of Church’s
    thesis saying every function from the natural numbers to themselves is
    recursive. Thus it refutes classical logic and the axiom of choice ‒
    although in fact it verifies countable choice. The result is allied to
    intuitionistic arithmetic and analysis. Later the chapter describes
    interpretations of intuitionistic or constructive set theory in Eff due
    to McCarty and to Lubarsky, Streicher, and van den Berg.  None of the
    results is exactly what any given intuitionist or constructivist might
    want. This is a crucial feature of the approach: it gives a canonical
    meaning to recursive realizability of any first- or higher-order
    statement of arithmetic independent of any philosophical conception of
    what ‘ought’ to count as intuitionistic or constructive. Other
    pcas, as described in Chapters 1 and then 4, give other notions of
    realizability. In effect one pca is one notion of first-order
    realizability, and the topos context gives each one of those a
    canonical higher-order extension.  Almost at the beginning of work on
    Eff, Hyland saw it contains striking new kinds of sets and categories:
    if we do set theory inside of Eff then a nontrivial ‘set’ $A$ may
    be the same size as the ‘set’ $A^A$ of all functions from it to
    itself. In classical set theory this happens only when $A$ is a
    singleton. As a more refined variant, a small category, that is, a
    category with a ‘set’ of arrows, may have arbitrary ‘set’ sized
    limits without just being a pre-order. Van Oosten gives an extensive
    but intuitive account of this in terms of fibrations without attempting
    the fully rigorous “mathematical core of the argument” (p. 179). 
    These things suggested computationally plausible kinds of data
    structures which exist in the most naive sense in Eff while these naive
    forms are impossible in classical set theory. Classically, a model of
    untyped $λ$-calculus cannot represent every function from terms to
    terms by a term ‒ unless there is only one term and so only one
    function from terms to terms! But each non-singleton ‘set’ $A$ in
    Eff which is the same size as the function set $A^A$ gives a nontrivial
    model of untyped $λ$-calculus with that naively desirable property.
    Chapter 3 discusses synthetic domain theory, which is more or less an
    axiomatic theory of categories of data types, and shows that many kinds
    of extremely powerful, simple, naive, and classically impossible
    constructions work in the internal logic of Eff. Similar results hold
    for an axiomatic computability theory developed by Andrej Bauer. Here
    an observation on fixed points by William Lawvere (p. 233) leads to
    naively simple, classically impossible, arguments which lead to
    classically valid results on computability.  Chapter 3 closes with
    general comments on open questions about Eff. Some are related to
    André Joyal’s characterization of Eff by a universal property. Van
    Oosten lays out several versions of this. Then he shows how little is
    yet known about the related question of geometric morphisms to or from
    Eff. This is particularly frustrating to the reviewer, since one
    advantage the tripos construction seems to have over constructing Eff
    directly from assemblies is that triposes themselves admit a natural
    notion of geometric morphism (p. 86ff.) and one could hope it would
    give a good theory of geometric morphisms between realizability toposes
    and others. But it has not yet.  Chapter 4 describes a great many
    variant notions of realizability. This is particularly close to van
    Oosten’s 1991 Ph.D. dissertation [Exercises in realizability.
    Amsterdam: Univ. Amsterdam (1991)] collecting several articles he
    published around that time. It covers a great deal done since then by
    himself and others.  Altogether, the book gives an extensive survey of
    research on realizability toposes with a 12-page bibliography.
rv: Colin McLarty (MR2479466)