Author name cluster

A.J. Power

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

TCS Journal 1999 Journal Article

Bireflectivity

P.J. Freyd
P.W. O’Hearn
A.J. Power
M. Takeyama
R. Street
R.D. Tennent

Motivated by a model for syntactic control of interference, we introduce a general categorical concept of bireflectivity. Bireflective subcategories of a category A are subcategories with left and right adjoint equal, subject to a coherence condition. We characterise them in terms of split-idempotent natural transformations on id A. In the special case that A is a presheaf category, we characterise them in terms of the domain, and prove that any bireflective subcategory of A is itself a presheaf category. We define diagonal structure on a symmetric monoidal category which is still more general than asking the tensor product to be the categorical product. We then obtain a bireflective subcategory of [C op, Set ] and deduce results relating its finite product structure with the monoidal structure of [C op, Set ] determined by that of C. We also investigate the closed structure. Finally, for completeness, we give results on bireflective subcategories in Rel(A), the category of relations in a topos A, and a characterisation of bireflection functors in terms of modules they define.

Details DOI

TCS Journal 1999 Journal Article

Syntactic control of interference revisited

P.W. O’Hearn
A.J. Power
M. Takeyama
R.D. Tennent

In “syntactic control of interference” (POPL, 1978), J. C. Reynolds proposes three design principles intended to constrain the scope of imperative state effects in Algol-like languages. The resulting linguistic framework seems to be a very satisfactory way of combining functional and imperative concepts, having the desirable attributes of both purely functional languages (such as PCF) and simple imperative languages (such as the language of while programs). However, Reynolds points out that the “obvious” syntax for interference control has the unfortunate property that β-reductions do not always preserve typings. Reynolds has subsequently presented a solution to this problem (ICALP, 1989), but it is fairly complicated and requires intersection types in the type system. Here, we present a much simpler solution which does not require intersection types. We first describe a new type system inspired in part by linear logic and verify that reductions preserve typings. We then define a class of “bireflective” models, which provide a categorical analysis of structure underlying the new typing rules; a companion paper “Bireflectivity”, in this volume, exposes wider ramifications of this structure. Finally, we describe a concrete model for an illustrative programming language based on the new type system; this improves on earlier such efforts in that states are not assumed to be structured using locations.

Details DOI

TCS Journal 1997 Journal Article

A representable approach to finite nondeterminism

S.O. Anderson
A.J. Power

We reformulate denotational semantics for nondeterminism, taking a nondeterministic operation V on programs, and sequential composition, as primitive. This gives rise to binary trees. We analyse semantics for both type and program constructors such as products and exponential types, conditionals and recursion, in this setting. In doing so, we define new category-theoretic structures, in particular premonoidal categories. We also account for equivalences of programs such as those induced by associativity, symmetry and idempotence of V, and we study finite approximation by enrichment over the category of ω-cpos with least element. We also show how to recover the classical powerdomains, especially the convex powerdomain, as three instances of a general, computationally natural, construction.

Details DOI

I&C Journal 1995 Journal Article

Why Tricategories?

A.J. Power

We outline a logical framework, based on the theory of categories with extra structure, for logics that arise in computer science. We list many representative examples of structures that have arisen, then we classify them in terms of equational, and the more general essentially algebraic, structure. In both cases, we outline the main results and their significance for the logical framework. This study gives rise to coherence questions. We explain the issues, and then outline the category theoretic concepts, such as tricategories, that arise in resolving the coherence problems.

Details DOI