Author

Alex Simpson

92 papers · 1920–2026

1967peak 9 in 20212026

Frequent co-authors

Papers

showing 1–25 of 92 RSS

Sequent calculi for induction and infinite descent

J G. Brotherston, Alex Simpson

Artificial Intelligence · Journal of Logic and Computation · 30 Sep 2010 · cited 126× · DOI ↗ · more like this ·

This article formalizes and compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system.The first system, LKID, supports traditional proof by induction, with induction rules formulated as rules for introducing inductively defined predicates on the left of sequents.We show LKID to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary. The second system, LKIDω, uses infinite (non-well-founded) proofs to represent arguments by infinite descent. In this system, the left-introduction rules for inductively defined predicates are simple case-split rules, and an infinitary, global condition on proof trees is required in order to ensure soundness.We show LKIDω to be cut-free complete with respect to standard models, and again infer…

Complete axioms for categorical fixed-point operators

Alex Simpson, Gordon Plotkin

Artificial Intelligence · Edinburgh Research Explorer (University of Edinburgh) · 7 Nov 2002 · cited 123× · DOI ↗ · more like this ·

We give an axiomatic treatment of fixed-point operators in categories. A notion of iteration operator is defined embodying the equational properties of iteration theories. We prove a general completeness theorem for iteration operators, relying on a new, purely syntactic characterisation of the free iteration theory. We then show how iteration operators arise in axiomatic domain theory. One result derives them from the existence of sufficiently many bifree algebras (exploiting the universal property Freyd introduced in his notion of algebraic compactness). Another result shows that, in the presence of a parameterized natural numbers object and an equational lifting monad, any uniform fixed-point operator is necessarily an iteration operator.

Relational Parametricity for Computational Effects

Rasmus Ejlers Møgelberg, Alex Simpson

cs.PL · June 2009 · cited 89× · arXiv ↗ · more like this ·

According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. Relational parametricity provides a powerful tool for establishing data abstraction properties, proving equivalences of datatypes, and establishing equalities of programs. Such properties have been well studied in a pure functional setting. Many programs, however, exhibit computational effects, and are not accounted for by the standard theory of relational parametricity. In this paper, we develop a foundational framework for extending the notion of relational parametricity to programming languages with effects.

Masculinity and Class in the Context of Dirty Work

Natasha Slutskaya, Ruth Simpson, Jason Hughes +2 more

Gender Studies · Gender Work and Organization · 5 Jan 2016 · cited 80× · DOI ↗ · more like this ·

Through an ethnographic study of ‘dirty work’ (refuse collection and street cleaning), this article explores how masculinity and class intersect — how, in a mutually constitutive sense, they produce attitudes and practices, strengths and vulnerabilities, which are shaped by shifting relations of privilege and power. We find resistance to class subordination through adherence to traditional forms of masculinity and through esteem‐enhancing social comparison (e.g., with women; with migrant workers). Men also mobilized powerful nostalgic themes around the loss of traditional jobs as well as trade union power. We argue that displays of masculine resilience in the face of devaluation are less indicative of a culture of masculine dominance but more an expression of vulnerability and social dislocation, serving both as a source of resistance whilst simultaneously reinforcing anchors of social…

Lessons from photoelicitation: encouraging working men to speak

Natasha Slutskaya, Alex Simpson, Jason Hughes

Sociology and Political Science · Qualitative Research in Organizations and Management An International Journal · 4 May 2012 · cited 79× · DOI ↗ · more like this ·

Purpose The purpose of this paper is to explore the possibilities of incorporating such visual methods as photoelicitation and photovoice into qualitative research, in order to retrieve something that, as a result of particular group socialisation, has been hidden, unspoken of or marginalised. Design/methodology/approach The research design combines 40 in‐depth verbal interviews with male butchers, with the use of photoelicitation and photovoice, in order to increase participant control of data generation. Findings Results suggest that photoelicitation enabled working‐class men to engage with themes which are rarely reflected on or discussed; which may sit uneasily with desired presentations of self; and which challenge traditional notions of gendered work. It prompted participants to elaborate and translate their daily experiences of physical labour into more expressive and detailed…

Beyond the symbolic: a relational approach to dirty work through a study of refuse collectors and street cleaners

Jason Hughes, Ruth Simpson, Natasha Slutskaya +2 more

Sociology and Political Science · Work Employment and Society · 7 Sep 2016 · cited 67× · DOI ↗ · more like this ·

Drawing on a relational approach and based on an ethnographic study of street cleaners and refuse collectors, we redress a tendency towards an overemphasis on the discursive by exploring the co-constitution of the material and symbolic dynamics of dirt. We show how esteem-enhancing strategies that draw on the symbolic can be both supported and undermined by the physicality of dirt, and how relations of power are rooted in subordinating material conditions. Through employing Hardy and Thomas’s taxonomy of objects, practice, bodies and space, we develop a fuller understanding of how the symbolic and material are fundamentally entwined within dirty work, and suggest that a neglect of the latter might foster a false optimism regarding worker experiences.

A Generic Operational Metatheory for Algebraic Effects

Patricia Johann, Alex Simpson, Janis Voigtländer

Artificial Intelligence · NC Digital Online Collection of Knowledge and Scholarship (The University of North Carolina at Greensboro) · July 2010 · cited 53× · DOI ↗ · more like this ·

We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of {algebraic effects}, and incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power's structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive "basic preorder" on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational…

Complete Sequent Calculi for Induction and Infinite Descent

J G. Brotherston, Alex Simpson

Artificial Intelligence · Edinburgh Research Explorer · 2007 · cited 44× · DOI ↗ · more like this ·

This paper compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system. The first system supports traditional proof by induction, with induction rules formulated as sequent rules for introducing inductively defined predicates on the left of sequents. We show this system to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary. The second system uses infinite (non-well-founded) proofs to represent arguments by infinite descent. In this system, the left rules for inductively defined predicates are simple case-split rules, and an infinitary, global condition on proof trees is required to ensure soundness. We show this system to be cut-free complete with respect to standard models, and again infer the eliminability of cut. The…

A uniform approach to domain theory in realizability models

John Longley, Alex Simpson

Artificial Intelligence · Mathematical Structures in Computer Science · October 1997 · cited 44× · DOI ↗ · more like this ·

We propose a uniform way of isolating a subcategory of predomains within the category of modest sets determined by a partial combinatory algebra (PCA). Given a divergence on a PCA (which determines a notion of partiality), we identify a candidate category of predomains, the well-complete objects . We show that, whenever a single strong completeness axiom holds, the category satisfies appropriate closure properties. We consider a range of examples of PCAs with associated divergences and show that in each case the axiom does hold. These examples encompass models allowing a ‘parallel’ style of computation (for example, by interleaving), as well as models that seemingly allow only ‘sequential’ computation, such as those based on term-models for the lambda-calculus. Thus, our approach provides a uniform approach to domain theory across a wide class of realizability models. We compare our…

A Convenient Category of Domains

Ingo Battenfeld, Matthias Schröder, Alex Simpson

Computational Theory and Mathematics · Electronic Notes in Theoretical Computer Science · April 2007 · cited 43× · DOI ↗ · more like this ·

We motivate and define a category of topological domains, whose objects are certain topological spaces, generalising the usual ω-continuous dcppos of domain theory. Our category supports all the standard constructions of domain theory, including the solution of recursive domain equations. It also supports the construction of free algebras for (in)equational theories, can be used as the basis for a theory of computability, and provides a model of parametric polymorphism.

Topological and limit-space subcategories of countably-based equilogical spaces

Matı́as Menni, Alex Simpson

Mathematical Physics · Mathematical Structures in Computer Science · December 2002 · cited 40× · DOI ↗ · more like this ·

There are two main approaches to obtaining ‘topological’ cartesian-closed categories. Under one approach, one restricts to a full subcategory of topological spaces that happens to be cartesian closed – for example, the category of sequential spaces. Under the other, one generalises the notion of space – for example, to Scott's notion of equilogical space. In this paper, we show that the two approaches are equivalent for a large class of objects. We first observe that the category of countably based equilogical spaces has, in a precisely defined sense, a largest full subcategory that can be simultaneously viewed as a full subcategory of topological spaces. In fact, this category turns out to be equivalent to the category of all quotient spaces of countably based topological spaces. We show that the category is bicartesian closed with its structure inherited, on the one hand, from the…

Behavioural Equivalence via Modalities for Algebraic Effects

Alex Simpson, Niels Voorneveld

cs.LO · April 2019 · cited 39× · arXiv ↗ · more like this ·

The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability, are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe's method. We show that the openness and decomposability conditions hold for several examples of algebraic effects…

Compositionality via cut-elimination: Hennessy-Milner logic for an arbitrary GSOS

Alex Simpson

Computational Theory and Mathematics · Edinburgh Research Explorer (University of Edinburgh) · 19 Nov 2002 · cited 36× · DOI ↗ · more like this ·

We present a sequent calculus for proving that processes in a process algebra satisfy assertions in Hennessy-Milner logic. The main novelty lies in the use of the operational semantics to derive introduction rules (on the left and right of sequents) for the different operators of the process calculus. This gives a generic proof system applicable to any process algebra with an operational semantics specified in the GSOS format. We identify the desirable property of compositionality with cut-elimination, and we prove that this holds for a class of sequents. Further, we show that the proof system enjoys good completeness and /spl omega/-completeness properties relative to its intended model.

CONSTRUCTIVE SET THEORIES AND THEIR CATEGORY-THEORETIC MODELS

Alex Simpson

Artificial Intelligence · 6 Oct 2005 · cited 30× · DOI ↗ · more like this ·

Abstract This chapter advocates a pragmatic approach to constructive set theory, using axioms based solely on set-theoretic principles that are directly relevant to (constructive) mathematical practice. The aim is to leave the notion of set as unconstrained as possible, while remaining consistent with the ways in which sets are actually used in mathematical practice. Following this approach, the chapter presents theories ranging in power from weaker predicative theories to stronger impredicative ones. The theories considered all have sound and complete classes of category-theoretic models, obtained by axiomatizing the structure of an ambient category of classes together with its subcategory of sets. In certain special cases, the categories of sets have independent characterizations in familiar category-theoretic terms, and one thereby obtains a rich source of naturally occurring…

A universal characterization of the closed Euclidean interval

Martı́n Hötzel Escardó, Alex Simpson

Computational Theory and Mathematics · University of Birmingham Research Portal (University of Birmingham) · 13 Nov 2002 · cited 28× · DOI ↗ · more like this ·

We propose a notion of interval object in a category with finite products, providing a universal property for closed and bounded real line segments. The universal property gives rise to an analogue of primitive recursion for defining computable functions on the interval. We use this to define basic arithmetic operations and to verify equations between them. We test the notion in categories of interest. In the category of sets, any closed and bounded interval of real numbers is an interval object. In the category of topological spaces, the interval objects are closed and bounded intervals with the Euclidean topology. We also prove that an interval object exists in and elementary topos with natural numbers object.

Probabilistic Observations and Valuations

Matthias Schröder, Alex Simpson

Artificial Intelligence · Electronic Notes in Theoretical Computer Science · May 2006 · cited 25× · DOI ↗ · more like this ·

We give a universal property for an “abstract probabilistic powerdomain” based on an analysis of observable properties of probabilistic computation. The universal property determines an abstract notion of integration satisfying the usual equational laws. In the category of topological spaces, the abstract probabilsitic powerdomain is given explicitly by the space of continuous probability valuations with weak topology. Thus our abstract notion of integration coincides with the usual integration for probability valuations. We end by discussing how our approach might adapt to provide “abstract effect spaces” for other computational effects.

Łukasiewicz mu-Calculus

Matteo Mio, Alex Simpson

cs.LO · 4 Sep 2013 · cited 24× · arXiv ↗ · more like this ·

The paper explores properties of Łukasiewicz mu-calculus, a version of the quantitative/probabilistic modal mu-calculus containing both weak and strong conjunctions and disjunctions from Łukasiewicz (fuzzy) logic. We show that this logic encodes the well-known probabilistic temporal logic PCTL. And we give a model-checking algorithm for computing the rational denotational value of a formula at any state in a finite rational probabilistic nondeterministic transition system.

Compactly generated domain theory

Ingo Battenfeld, Matthias Schröder, Alex Simpson

Computational Theory and Mathematics · Mathematical Structures in Computer Science · April 2006 · cited 24× · DOI ↗ · more like this ·

We propose compactly generated monotone convergence spaces as a well-behaved topological generalisation of directed-complete partial orders (dcpos). The category of such spaces enjoys the usual properties of categories of ‘predomains’ in denotational semantics. Moreover, such properties are retained if one restricts to spaces with a countable pseudobase in the sense of E. Michael, a fact that permits connections to be made with computability theory, realizability semantics and recent work on the closure properties of topological quotients of countably based spaces (qcb spaces). We compare the standard domain-theoretic constructions of products and function spaces on dcpos with their compactly generated counterparts, showing that these agree in important cases, though not in general.

Category-theoretic Structure for Independence and Conditional Independence

Alex Simpson

Artificial Intelligence · Electronic Notes in Theoretical Computer Science · April 2018 · cited 19× · DOI ↗ · more like this ·

Relations of independence and conditional independence arise in a variety of contexts. Stochastic independence and conditional independence are fundamental relations in probability theory and statistics. Analogous non-stochastic relations arise in database theory; in the setting of nominal sets (a semantic framework for modelling data with names); and in the modelling of concepts such as region disjointness for heap memory. In this paper, we identify unifying category-theoretic structure that encompasses these different forms of independence and conditional independence. The proposed structure supports the expected reasoning principles for notions of independence and conditional independence. We further identify associated notions of independent and local independent product, in which (conditional) independence is represented via a (fibred) monoidal structure, which is present in many…

Using Synthetic Domain Theory to Prove Operational Properties of a Polymorphic Programming Language Based on Strictness

Alex Simpson, Giuseppe Rosolini

Artificial Intelligence · 2004 · cited 17× · OpenAlex ↗ · more like this ·

We present a simple and workable axiomatization of domain theory within intuitionistic set theory, in which predomains are (special) sets, and domains are algebras for a simple equational theory. We use the axioms to construct a relationally parametric set-theoretic model for a compact but powerful polymorphic programming language, given by a novel extension of intuitionistic linear type theory based on strictness. By applying the model, we establish the fundamental operational properties of the language. 1.

Relating Topos Theory and Set Theory Via Categories of Classes

Steve Awodey, University, Carnegie Mellon, Alex Simpson +1 more

Geometry and Topology · Figshare · 29 Jun 2018 · cited 13× · DOI ↗ · more like this ·

We investigate a certain system of intuitionistic set theory from three points of view: an elementary set theory with bounded separation, a topos with distinguished inclusions, and a category of classes with a system of small maps. The three presentations are shown to be equivalent in a strong sense.

Relating First-Order Set Theories and Elementary Toposes

Steve Awodey, Carsten Butz, Alex Simpson +1 more

Artificial Intelligence · Bulletin of Symbolic Logic · September 2007 · cited 12× · DOI ↗ · more like this ·

Abstract We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo–Fraenkel set theory (IZF).

Two constructive embedding‐extension theorems with applications to continuity principles and to Banach‐Mazur computability

Andrej Bauer, Alex Simpson

Computational Theory and Mathematics · Mathematical logic quarterly · 18 Aug 2004 · cited 9× · DOI ↗ · more like this ·

Abstract We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space (CSM) without isolated points, X , in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non‐compact CSM. Both results rely on having careful constructive formulations of the concepts involved. As a first application, we derive new relationships between “continuity principles” asserting that all functions between specified metric spaces are pointwise continuous. In particular, we give conditions that imply the failure of the continuity principle “all functions from X to ℝ are continuous”, when X is an inhabited…

Equational Lifting Monads

Anna Bucalo, Carsten Führmann, Alex Simpson

Artificial Intelligence · Electronic Notes in Theoretical Computer Science · 1999 · cited 9× · DOI ↗ · more like this ·

We introduce the notion of an “equational lifting monad” : a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial map classifier such that the Kleisli category of the former fully embeds in the partial category of the latter. Thus equational lifting monads precisely capture the (partial) equational properties of partial map classifiers. The representation theorem also provides a tool for transferring non-equational properties of partial map classifiers to equational lifting monads.

Two preservation results for countable products of sequential spaces

Matthias Schröder, Alex Simpson

Computational Theory and Mathematics · Mathematical Structures in Computer Science · February 2007 · cited 8× · DOI ↗ · more like this ·

We prove two results for the sequential topology on countable products of sequential topological spaces. First we show that a countable product of topological quotients yields a quotient map between the product spaces. Then we show that the reflection from sequential spaces to its subcategory of monotone ω-convergence spaces preserves countable products. These results are motivated by applications to the modelling of computation on non-discrete spaces.