Equilogical spaces and filter spaces
Giuseppe Rosolini · CINECA IRIS Institutial Research Information System (University of Genoa) · 2000
The paper is about the comparison between (apparently) different cartesian closed extensions of the category of topological spaces. Since topological spaces do not in general allow formation of function spaces, the problem of determining suitable categories with such a property—and nicely related to that of topological spaces—was studied from many different perspectives: general topology, functional analysis, measure theory, computability. From a computational perspective, the interest about topological properties of the function spaces arose after the discovery of topological models of the λ-calculus by D.S. Scott, see [22], and the work of Ersov on the partial continuous functionals, see [12]. At the same time, work on cartesian closed extensions of the category of topological spaces in general topology produced interesting quasitoposes of filter spaces where a notion of convergence replaced that of neighbourhood system, see [23] for a complete review. The semantical analysis of computer behaviour requires that the mechanical black box which is the computer is simply a rule-executing grinder which determines values/outputs from given arguments/inputs. Although the mathematical concept of a Turing machine explains very precisely how the grinder operates, it is extremely useful to be able to have a more conceptual intuition about what a machine does. One of the most useful approximations to this intuition produced so far is the following: a computer executing a program evaluates a partial function. It follows that one of the most important things to know is whether, given a certain collection of inputs, the function evaluates on them all. Since programs can be stored in the machine, and operated upon by the grinder, a direct consequence is that extensional models of programs are to be cartesian closed categories. By an extensional model, here we mean a mathematical structure where two maps are distinguished by their values on global elements, e.g. a category where the terminal object generates. This does not necessarily mean that a general notion of model of computation