Author name cluster

Gordon Plotkin

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.

5 papers

1 author row

I&C Journal 2009 Journal Article

On the completeness of order-theoretic models of the λ-calculus

Furio Honsell
Gordon Plotkin

Scott discovered his domain-theoretic models of the λ-calculus, isomorphic to their function space, in 1969. A natural completeness problem then arises: whether any two terms equal in all Scott models are convertible. There is also an analogous consistency problem: whether every equation between two terms, consistent with the λ-calculus, has a Scott model. We consider such questions for wider sets of sentences and wider classes of models, the pointed (completely) partially ordered ones. A negative result for a set of sentences shows the impossibility of finding Scott models for that class; a positive result gives evidence that there might be enough Scott models. We find, for example, that the order-extensional pointed ω-cpo models are complete for Π 1 -sentences with positive matrices, whereas the consistency question for Σ1-sentences with equational matrices depends on the consistency of certain critical sentences asserting the existence of certain functions analogous to the generalized Mal’cev operators first considered in the context of the λ-calculus by Selinger.

Details DOI

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

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

I&C Journal 1996 Journal Article

On a Question of H. Friedman

Gordon Plotkin

In this paper we answer a question of Friedman, providing anω-separable model M of theλβη-calculus. There therefore exists anα-separable model for anyα⩾0. The model M permits no non-trivial enrichment as a partial order; neither does it permit an enrichment as a category with an initial object. The open term model embeds in M: by way of contrast we provide a model which cannot embed in any non-trivial model separating all pairs of distinct elements

Details DOI

TCS Journal 1981 Journal Article

Petri nets, event structures and domains, part I

Mogens Nielsen
Gordon Plotkin
Glynn Winskel

The general aim of this paper is to find a theory of concurrency combining the approaches of Petri and Scott (and others). In part I we introduce our formalisms. To connect the abstract ideas of events and domains of information, we show how casual nets induce certain kinds of domains where the information points are certain sets of events. This allows translations between the languages of net theory and domain theory. Following the idea that events of causal nets are occurrences, we generalise causal nets to occurrence nets, by adding forwards conflict. Just as infinite flow charts unfold finite ones, so transition nets can be unfolded into occurrence nets. Next we extend the above connections between nets and domains to these new nets. Event structures which are intermediate between nets and domains play an important part in all our work. Finally, as an example of how concepts translate from one formalism to the other, we show how Petri's notion of confusion ties up with Kahn and Plotkin's concrete domains. In part II we shall continue the job of connecting up notions within net theory and the theory of domains. In particular, we shall examine the idea of states of computations.

Details DOI