Distinguished Dissertations in Computer Science – serie

Computer vision is a rapidly growing field which aims to make computers 'see' as effectively as humans. In this book Dr Shapiro presents a new computer vision framework for interpreting time-varying imagery. This is an important task, since movement reveals valuable information about the environment. The fully-automated system operates on long, monocular image sequences containing multiple, independently-moving objects, and demonstrates the practical feasibility of recovering scene structure and motion in a bottom-up fashion. Real and synthetic examples are given throughout, with particular emphasis on image coding applications. Novel theory is derived in the context of the affine camera, a generalisation of the familiar scaled orthographic model. Analysis proceeds by tracking 'corner features' through successive frames and grouping the resulting trajectories into rigid objects using new clustering and outlier rejection techniques. The three-dimensional motion parameters are then computed via 'affine epipolar geometry', and 'affine structure' is used to generate alternative views of the object and fill in partial views. The use of all available features (over multiple frames) and the incorporation of statistical noise properties substantially improves existing algorithms, giving greater reliability and reduced noise sensitivity.

A common attraction to functional programming is the ease with which proofs can be given of program properties. A common disappointment with functional programming is the difficulty of expressing input/output (I/O), while at the same time being able to verify programs. Here, the author shows how a theory of functional programming can be smoothly extended to admit both an operational semantics for functional I/O and verification of programs engaged in I/O. He obtains operational semantics for the three most widely implemented I/O mechanisms for lazy languages, and proves that the three are equivalent in expressive power. He develops semantics for a form of monadic I/O and verifies a simple programming example. These theories of functional I/O are based on an entirely operational theory of functional programming, developed using Abramsky's 'applicative bisimulation'.

First published in 1993, this thesis is concerned with the design of efficient algorithms for listing combinatorial structures. The research described here gives some answers to the following questions: which families of combinatorial structures have fast computer algorithms for listing their members? What general methods are useful for listing combinatorial structures? How can these be applied to those families which are of interest to theoretical computer scientists and combinatorialists? Amongst those families considered are unlabelled graphs, first order one properties, Hamiltonian graphs, graphs with cliques of specified order, and k-colourable graphs. Some related work is also included, which compares the listing problem with the difficulty of solving the existence problem, the construction problem, the random sampling problem, and the counting problem. In particular, the difficulty of evaluating Pólya's cycle polynomial is demonstrated.

First published in 1991, this thesis concentrates upon the design of three-dimensional, rather than the traditional two-dimensional, circuits. The theory behind such circuits is presented in detail, together with experimental results. Winner of the Distinguished Dissertation in Computer Science award, this work will prove invaluable to both designers and hardware engineers involved in the development of practical three-dimensional integrated circuits.

This book was originally published in 1995. At the time of publication, distributed file systems were monolithic and only supported single file abstractions. Network storage devices needed to be able to accommodate emerging information media such as digital audio and video, with data radically different in characteristics to traditional text and binary that file systems were optimised for. By combining emerging and traditional media, information could be recorded and presented in the most suitable way, and the value of a piece of information could be further enhanced by linking together related pieces. However composite data and cross-reference between data items raised a number of system issues that had not been addressed properly before. In this book Dr Lo defined a multi-service storage architecture that could meet the needs of existing and emerging applications and support multiple file abstractions. He also explored a number of related design issues.

First published in 1991, this thesis concentrates upon the design of three-dimensional, rather than the traditional two-dimensional, circuits. The theory behind such circuits is presented in detail, together with experimental results. Winner of the Distinguished Dissertation in Computer Science award, this work will prove invaluable to both designers and hardware engineers involved in the development of practical three-dimensional integrated circuits.

First published in 1993, this thesis is concerned with the design of efficient algorithms for listing combinatorial structures. The research described here gives some answers to the following questions: which families of combinatorial structures have fast computer algorithms for listing their members? What general methods are useful for listing combinatorial structures? How can these be applied to those families which are of interest to theoretical computer scientists and combinatorialists? Amongst those families considered are unlabelled graphs, first order one properties, Hamiltonian graphs, graphs with cliques of specified order, and k-colourable graphs. Some related work is also included, which compares the listing problem with the difficulty of solving the existence problem, the construction problem, the random sampling problem, and the counting problem. In particular, the difficulty of evaluating Pólya's cycle polynomial is demonstrated.

This book was first published in 1993. Computing systems are becoming highly complex, harder to understand, and therefore more prone to failure. Where such systems control aircraft for example, system failure could have disastrous consequences. It is important therefore that we are able to employ mathematical techniques to specify the behaviour or safety critical systems. This thesis uses the theory of Communicating Sequential Processes (CSP) to show how a real-lime system may be specified. Included is a case study in which a local area network protocol is described at two levels of abstraction, and a general method 14 structuring CSP descriptions of layered protocols is given.

There are two radically different approaches to robot navigation: the first is to use a map of the robot's environment; the second uses a set of action reflexes to enable a robot to react rapidly to local sensory information. Hybrid approaches combining features of both also exist. This book is the first to propose a method for evaluating the different approaches that shows how to decide which is the most appropriate for a given situation. It begins by describing a complete implementation of a mobile robot including sensor modelling, map-building (a feature-based map and a grid-based free-space map), localisation, and path-planning. Exploration strategies are then tested experimentally in a range of environments and starting positions. The author shows the most promising results are observed from hybrid exploration strategies which combine the robustness of reactive navigation and the directive power of map-based strategies.

This book describes the use of qualified types to provide a general framework for the combination of polymorphism and overloading. For example, qualified types can be viewed as a generalization of type classes in the functional language Haskell and the theorem prover Isabelle. These in turn are extensions of equality types in Standard ML. Other applications of qualified types include extensible records and subtyping. Using a general formulation of qualified types, the author extends the Damas/Milner type inference algorithm to support qualified types, which in turn specifies the set of all possible types for any term. In addition, he describes a new technique for establishing suitable coherence conditions that guarantee the same semantics for all possible translations of a given term. Practical issues that arise in concrete implementations are also discussed, concentrating in particular on the implementation of overloading in Haskell and Gofer, a small functional programming system developed by the author.

This book was originally published in 1995. At the time of publication, distributed file systems were monolithic and only supported single file abstractions. Network storage devices needed to be able to accommodate emerging information media such as digital audio and video, with data radically different in characteristics to traditional text and binary that file systems were optimised for. By combining emerging and traditional media, information could be recorded and presented in the most suitable way, and the value of a piece of information could be further enhanced by linking together related pieces. However composite data and cross-reference between data items raised a number of system issues that had not been addressed properly before. In this book Dr Lo defined a multi-service storage architecture that could meet the needs of existing and emerging applications and support multiple file abstractions. He also explored a number of related design issues.

Axiomatic categorical domain theory is crucial for understanding the meaning of programs and reasoning about them. This book is the first systematic account of the subject and studies mathematical structures suitable for modelling functional programming languages in an axiomatic (i.e. abstract) setting. In particular, the author develops theories of partiality and recursive types and applies them to the study of the metalanguage FPC; for example, enriched categorical models of the FPC are defined. Furthermore, FPC is considered as a programming language with a call-by-value operational semantics and a denotational semantics defined on top of a categorical model. To conclude, for an axiomatisation of absolute non-trivial domain-theoretic models of FPC, operational and denotational semantics are related by means of computational soundness and adequacy results. To make the book reasonably self-contained, the author includes an introduction to enriched category theory.

Dr Andrews here provides a homogeneous treatment of the semantics (operational and logical) of both theoretical and practical logic programming languages. He shows how the rift between theory and practice in logic programming can be bridged. This is achieved by precisely characterizing the way in which 'depth-first' search for solutions to a logical formula - the usual strategy in most practical languages - is incomplete. Languages that perform 'breadth-first' searches reflect more closely the theory underlying logic programming languages. Researchers interested in logic programming or semantics, as well as artificial intelligence search strategies, will want to consult this book as the only source for some essential and new ideas in the area.

We are surrounded by noise; we must be able to separate the signals we want to hear from those we do not. To overcome this 'cocktail party effect' we have developed various strategies; endowing computers with similar abilities would enable the development of devices such as intelligent hearing aids and robust speech recognition systems. This book describes a system which attempts to separate multiple, simultaneous acoustic sources using strategies based on those used by humans. It is both a review of recent work on the modelling of auditory processes, and a presentation of a new model in which acoustic signals are decomposed into elements. These structures are then re-assembled in accordance with rules of auditory organisation which operate to bind together elements that are likely to have arisen from the same source. The model is evaluated by measuring its ability to separate speech from a wide variety of other sounds, including music, phones and other speech.

This is the first book presenting a stochastic extension of process algebra, PEPA; this is shown to be suitable for specifying a Markov process, which can then be applied to performance modelling. The method, which is illustrated with case studies taken from the area of communication systems, can readily be used to construct a variety of models that can be analysed using standard numerical techniques. One of the major advantages of PEPA over the standard methods for specifying stochastic performance models is the inherent apparatus for reasoning about the structure and behaviour of models. In the later chapters this apparatus is exploited to define four equivalence relations over PEPA components. Each of these notions of equivalence has intrinsic interest from a process algebra perspective. However, they are also demonstrated to be useful in a performance modelling context. To conclude the book, a section has been added surveying recent results in the area and discussing open questions.