Author name cluster

John 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.

18 papers

2 author rows

TCS Journal 2014 Journal Article

Category theoretic structure of setoids

Yoshiki Kinoshita
John Power

A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category Setoid and prove it is Cartesian closed with coproducts. We then enrich it in the Cartesian closed category Equiv of sets and classical equivalence relations, extend the above results, and prove that Setoid as an Equiv -enriched category has a relaxed form of equalisers. We then recall the definition of E -category, generalising that of Equiv -enriched category, and show that Setoid as an E -category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.

Details DOI

CSL Conference 2011 Conference Paper

Coalgebraic Derivations in Logic Programming

Ekaterina Komendantskaya
John Power

Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove correctness and full abstraction results.

Details

JELIA Conference 2008 Conference Paper

Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness

Ekaterina Komendantskaya
John Power

Abstract We introduce a fibrational semantics for many-valued logic programming, use it to define an SLD-resolution for annotation-free many valued logic programs as defined by Fitting, and prove a soundness and completeness result relating the two. We show that fibrational semantics corresponds with the traditional declarative (ground) semantics and deduce a soundness and completeness result for our SLD-resolution algorithm with respect to the ground semantics.

Details

TCS Journal 2007 Journal Article

Combining algebraic effects with continuations

Martin Hyland
Paul Blain Levy
Gordon Plotkin
John Power

We consider the natural combinations of algebraic computational effects such as side-effects, exceptions, interactive input/output, and nondeterminism with continuations. Continuations are not an algebraic effect, but previously developed combinations of algebraic effects given by sum and tensor extend, with effort, to include commonly used combinations of the various algebraic effects with continuations. Continuations also give rise to a third sort of combination, that given by applying the continuations monad transformer to an algebraic effect. We investigate the extent to which sum and tensor extend from algebraic effects to arbitrary monads, and the extent to which Felleisen et al. ’s C operator extends from continuations to its combination with algebraic effects. To do all this, we use Dubuc’s characterisation of strong monads in terms of enriched large Lawvere theories.

Details DOI

I&C Journal 2006 Journal Article

Coalgebraic semantics for timed processes

Marco Kick
John Power
Alex Simpson

We give a coalgebraic formulation of timed processes and their operational semantics. We model time by a monoid called a “time domain”, and we model processes by “timed transition systems”, which amount to partial monoid actions of the time domain or, equivalently, coalgebras for an “evolution comonad” generated by the time domain. All our examples of time domains satisfy a partial closure property, yielding a distributive law of a monad for total monoid actions over the evolution comonad, and hence a distributive law of the evolution comonad over a dual comonad for total monoid actions. We show that the induced coalgebras are exactly timed transition systems with delay operators. We then integrate our coalgebraic formulation of time qua timed transition systems into Turi and Plotkin’s formulation of structural operational semantics in terms of distributive laws. We combine timing with action via the more general study of the combination of two arbitrary sorts of behaviour whose operational semantics may interact. We give a modular account of the operational semantics for a combination induced by that of each of its components. Our study necessitates the investigation of products of comonads. In particular, we characterise when a monad lifts to the category of coalgebras for a product comonad, providing constructions with which one can readily calculate.

Details DOI

TCS Journal 2006 Journal Article

Combining effects: Sum and tensor

Martin Hyland
Gordon Plotkin
John Power

We seek a unified account of modularity for computational effects. We begin by reformulating Moggi's monadic paradigm for modelling computational effects using the notion of enriched Lawvere theory, together with its relationship with strong monads; this emphasises the importance of the operations that produce the effects. Effects qua theories are then combined by appropriate bifunctors on the category of theories. We give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer and an interactive input/output monad transformer. We further give a theory of the commutative combination of effects, their tensor, which yields Moggi's side-effects monad transformer. Finally, we give a theory of operation transformers, for redefining operations when adding new effects; we derive explicit forms for the operation transformers associated to the above monad transformers.

Details DOI

TCS Journal 2006 Journal Article

Discrete Lawvere theories and computational effects

Martin Hyland
John Power

Countable Lawvere theories model computational effects such as exceptions, side-effects, interactive input/output, nondeterminism and probabilistic nondeterminism. The category of countable Lawvere theories has sums, tensors, and distributive tensors, modelling natural combinations of such effects. It is also closed under taking images. Enrichment in a category such as ω Cpo allows one to extend this modelling of computational effects to account for partiality and recursion. Sum and tensor extend to enriched countable Lawvere theories, but distributive tensor and image do not. So here we introduce discrete countable enriched Lawvere theories in order to allow natural definitions and accounts of distributive tensor and image. A discrete countable enriched Lawvere theory is, in a sense we make precise, an enriched Lawvere theory with discrete arities. We show that they include all our leading examples of computational effects and are closed under sum and tensor. And we develop notions of enriched operad and enriched multicategory to support the definition.

Details DOI

TCS Journal 2006 Journal Article

Generic models for computational effects

John Power

A Freyd-category is a subtle generalisation of the notion of a category with finite products. It is suitable for modelling environments in call-by-value programming languages, such as the computational λ -calculus, with computational effects. We develop the theory of Freyd-categories with that in mind. We first show that any countable Lawvere theory, hence any signature of operations with countable arity subject to equations, directly generates a Freyd-category. We then give canonical, universal embeddings of Freyd-categories into closed Freyd-categories, characterised by being free cocompletions. The combination of the two constructions sends a signature of operations and equations to the Kleisli category for the monad on the category Set generated by it, thus refining the analysis of computational effects given by monads. That in turn allows a more structural analysis of the λ c -calculus. Our leading examples of signatures arise from side-effects, interactive input/output and exceptions. We extend our analysis to an enriched setting in order to account for recursion and for computational effects and signatures that inherently involve it, such as partiality, nondeterminism and probabilistic nondeterminism.

Details DOI

TCS Journal 2004 Journal Article

Category theory for operational semantics

Marina Lenisa
John Power
Hiroshi Watanabe

We use the concept of a distributive law of a monad over a copointed endofunctor to define and develop a reformulation and mild generalisation of Turi and Plotkin's notion of an abstract operational rule. We make our abstract definition and give a precise analysis of the relationship between it and Turi and Plotkin's definition. Following Turi and Plotkin, our definition, suitably restricted, agrees with the notion of a set of GSOS-rules, allowing one to construct both an operational model and a canonical, internally fully abstract denotational model. Going beyond Turi and Plotkin, we construct what might be seen as large-step operational semantics from small-step operational semantics and we show how our definition allows one to combine distributive laws, in particular accounting for the combination of operational semantics with congruences.

Details DOI

I&C Journal 2003 Journal Article

Modelling environments in call-by-value programming languages

PaulBlain Levy
John Power
Hayo Thielecke

In categorical semantics, there have traditionally been two approaches to modelling environments, one by use of finite products in cartesian closed categories, the other by use of the base categories of indexed categories with structure. Each requires modifications in order to account for environments in call-by-value programming languages. There have been two more general definitions along both of these lines: the first generalising from cartesian to symmetric premonoidal categories, the second generalising from indexed categories with specified structure to κ-categories. In this paper, we investigate environments in call-by-value languages by analysing a fine-grain variant of Moggi’s computational λ-calculus, giving two equivalent sound and complete classes of models: one given by closed Freyd categories, which are based on symmetric premonoidal categories, the other given by closed κ-categories.

Details DOI

TCS Journal 2002 Journal Article

Combining a monad and a comonad

John Power
Hiroshi Watanabe

We give a systematic treatment of distributivity for a monad and a comonad as arises in giving category theoretic accounts of operational and denotational semantics, and in giving an intensional denotational semantics. We do this axiomatically, in terms of a monad and a comonad in a 2-category, giving accounts of the Eilenberg–Moore and Kleisli constructions. We analyse the eight possible relationships, deducing that two pairs are isomorphic, but that the other pairs are all distinct. We develop those 2-categorical definitions necessary to support this analysis.

Details DOI

TCS Journal 2002 Journal Article

Fixpoint operators for domain equations

John Power
Giuseppe Rosolini

We investigate fixpoint operators for domain equations. It is routine to verify that if every endofunctor on a category has an initial algebra, then one can construct a fixpoint operator from the category of endofunctors to the category. That construction does not lift routinely to enriched categories, using the usual enriched notion of initiality of an endofunctor. We show that by embedding the 2-category of small enriched categories into the 2-category of internal categories of a presheaf topos, we can recover the fixpoint construction elegantly. Also, we show that in the presence of cotensors, an enriched category allows the fixpoint construction.

Details DOI

TCS Journal 2002 Journal Article

Premonoidal categories as categories with algebraic structure

John Power

We develop the study of premonoidal categories. Specifically, we reconcile premonoidal categories with the usual study of categories with algebraic structure by adding a little extra structure. We further give a notion of closedness for a premonoidal category with such extra structure, and show that every premonoidal category fully embeds into a closed one.

Details DOI

CSL Conference 2001 Conference Paper

An Algebraic Foundation for Higraphs

John Power
Konstantinos Tourlas

Abstract Higraphs, which are structures extending graphs by permitting a hierarchy of nodes, underlie a number of diagrammatic formalisms popular in computing. We provide an algebraic account of higraphs (and of a mild extension), with our main focus being on the mathematical structures underlying common operations, such as those required for understanding the semantics of higraphs and Statecharts, and for implementing sound software tools which support them.

Details

TCS Journal 2001 Journal Article

On the structure of categories of coalgebras

Peter Johnstone
John Power
Toru Tsujishita
Hiroshi Watanabe
James Worrell

Consideration of categories of transition systems and related constructions leads to the study of categories of F-coalgebras, where F is an endofunctor of the category of sets, or of some more general ‘set-like’ category. It is fairly well known that if E is a topos and F: E→E preserves pullbacks and generates a cofree comonad, then the category of F-coalgebras is a topos. Unfortunately, in most of the examples of interest in computer science, the endofunctor F does not preserve pullbacks, though it comes close to doing so. In this paper we investigate what can be said about the category of coalgebras under various weakenings of the hypothesis that F preserves pullbacks. It turns out that almost all the elementary properties of a topos, except for effectiveness of equivalence relations, are still inherited by the category of coalgebras; and the latter can be recovered by embedding the category in its effective completion. However, we also show that, in the particular cases of greatest interest, the category of coalgebras is not itself a topos.

Details DOI

CSL Conference 2000 Conference Paper

Logical Relations and Data Abstraction

John Power
Edmund Robinson

Abstract We prove, in the context of simple type theory, that logical relations are sound and complete for data abstraction as given by equational specifications. Specifically, we show that two implementations of an equationally specified abstract type are equivalent if and only if they are linked by a suitable logical relation. This allows us to introduce new types and operations of any order on those types, and to impose equations between terms of any order. Implementations are required to respect these equations up to a general form of contextual equivalence, and two implementations are equivalent if they produce the same contextual equivalence on terms of the enlarged language. Logical relations are introduced abstractly, soundness is almost automatic, but completeness is more difficult, achieved using a variant of Jung and Tiuryn’s logical relations of varying arity. The results are expressed and proved categorically.

Details

CSL Conference 1999 Conference Paper

Data-Refinement for Call-By-Value Programming Languages

Yoshiki Kinoshita
John Power

Abstract We give a category theoretic framework for data-refinement in call-by-value programming languages. One approach to data refinement for the simply typed λ-calculus is given by generalising the notion of logical relation to one of lax logical relation, so that binary lax logical relations compose. So here, we generalise the notion of lax logical relation, defined in category theoretic terms, from the simply typed? - calculus to the computational λ-calculus as a model of data refinement.

Details

CSL Conference 1998 Conference Paper

Categories with Algebraic Structure

John Power

Abstract We give an exposition of a unified study of categories with extra structure that arise in computer science and mathematics. We consider several examples of structures that arise, showing that with a precise formulation of the notion of category with algebraic structure, they are categories with algebraic structure. We then outline the central results and issues in the study of categories with algebraic structure, with an account of why those issues are of computational interest. We illustrate general theorems that yield substantial results in examples given by familiar structures. In particular, we explain known mathematics that supports the idea of a programming language being freely generated by basic data and specified algebraic structure. We then show in detail how the concept of algebraic structure may be used in defining new category theoretic structures by showing how it affected the precise formulation of premonoidal category, as has recently been proposed to account for contexts.

Details