There has recently been considerable interest in the development of 'logical frameworks' which can represent many of the logics arising in computer science in a uniform way. Within the Edinburgh LF project, this concept is split into two components; the first being a general proof theoretic encoding of logics, and the second a uniform treatment of their model theory. This thesis forms a case study for the work on model theory. The models of many first and higher order logics can be represented as <i>fibred</i> or <i>indexed</i> categories with certain extra structure, and this has been suggested as a general paradigm. The aim of the thesis is to test the strength and flexibility of this paradigm by studying the specific case of Girard's linear logic. It should be noted that the exact form of this logic in the first order case is not entirely certain, and the system treated here is significantly different to that considered by Girard. To secure a good class of models, we develop a carefully restricted form of first order intuitionistic linear logic, called cal L<SUB>FOLL</SUB>, in which the linearity of the logic is also reflected at the level of types. That is, the terms of the logic are given by a <i>linear type theory</i> LTT corresponding to the algebraic idea of a symmetric monoidal closed category. The study of logic in such categories is motivated by two examples which are derived as linear analogues of presheaf topoi and Heyting valued sets respectively. We introduce the concept of a <i>monoidal factorisation system</i> over such categories to provide a basis for a theory of linear predicates. A monoidal factorisation system then gives rise to a structure preserving fibration between symmetric monoidal closed categories, which we term a <i>linear doctrine</i>. We provide a sequent calculus formulation of cal L<SUB>FOLL</SUB> and show that it is both sound and complete with respect to a linear doctrine semantics.

The thesis addresses the most fundamental architectural characteristic of the brain: the fact that it is divided into two halves, with resulting functional asymmetries. The goal is to explore the characteristic behaviours, and the advantages if any, of processing in a split architecture. The explorations are concerned with the fundamental issue of how information is handled and distributed between different parts of a whole system. Specifically, the thesis is concerned with the intersection of visual processing in humans, marked by the separation of the visual cortices, and the resource allocation properties of split neural networks. This study involvesthe representational differentiation and associated behaviours that result from the interaction of several factors, and particularly: the developing architecture; the way in which stimuli are presented to the processor; and the nature of the stimuli themselves. I present results from connectionist modelling experiments with split architectures. The principal issues addressed in the thesis revolve around what the advantages might be for bi-hemispheric processing of visual information, and how real-time high-density information management---such as that employed in the human visual system---copes with the fact that processing of the same stimulus is done in two halves, in two different places. Despite the brain's clear division into two cerebral hemispheres, there has to date been relatively little computational modelling of this aspect of gross brain morphology. However, certain recent models employing split neural networks have demonstrated that such architectures are not only effective for processing visual information, but that certain emergent processing strategies are particular to these split architectures. This thesis reports further studies of the complex relationship that comes into play between particular architectural features and general processing strategies, as well as distinct variations in the nature of the stimuli involved. The particular feature of the visual system addressed in this thesis is the recently acknowledged vertical splitting of the human retina, including the fovea, resulting in each visual hemifield initially being precisely projected to the contralateral hemisphere. As an example of the emergent effects that models of such a system produce, this thesis examines the nature of symmetrical forms, asking in what ways the perception of symmetry can be treated as a special case in cognition. This thesis makes a contribution to our understanding of processing in a divided architecture such as the human brain, and to unpacking the causes that lie behind functional lateralisation, by examining split processing in its most general form.

The role of interactive technology in live performance has increased substantially in recent years. Practices and experiences of existing forms of live performance have been transformed and new genres of technology-­‐mediated live performance have emerged in response to novel technological opportunities. Consequently, designing for live performance is set to become an increasingly important concern for interaction design researchers and practitioners. However, designing interactive technology for live performance is a challenging activity, as the experiences of both performers and their audiences are shaped and influenced by a number of delicate and interconnected issues, which relate to different forms and individual practices of live performance in varied and often conflicting ways. The research presented in this thesis explores how interaction designers might be better supported in engaging with this intricate and multifaceted design space. This is achieved using a practice-­‐led methodology, which involves the researcher’s participation in both the investigation of, and design response to, issues of live performance as they are embodied in the lived and felt experiences of individual live performers’ practices during three interaction design case studies. This research contributes to the field of interaction design for live performance in three core areas. Understandings of the relationships between key issues of live performance and individual performers’ lived and felt experiences are developed, approaches to support interaction designers in engaging individual live performers’ lived and felt experiences in design are proposed and innovative interfaces and interaction techniques for live performance are designed. It is anticipated that these research outcomes will prove directly applicable or inspiring to the practices of interaction designers wishing to address live performance and will contribute to the ongoing academic discourse around the experience of, and design for, live performance.

This thesis investigates the application of Distributed Cognition (DCog) to understand patients’ situated interactions with Home Haemodialysis Technology (HHT). With the anticipated increase in home healthcare, there is a need to understand how Home Medical Devices (HMDs) should be designed so that they are patient-friendly and can be safely used in the home. This implies studying situated interactions with current HMDs and identifying the issues that patients face. Taking HHT as an example of a HMD, this thesis focuses on understanding the contexts in which renal patients interact with HHT, and their interaction strategies and issues, from a DCog perspective. DCog has been a useful theoretical framework for understanding work in clinical settings, but has not previously been applied to the study of interactions with HMDs. Data was gathered during visits to 19 patients through ethnographic observations and semi-structured interviews. 3 renal nurses, 3 renal technicians, and 1 nephrologist were also interviewed. Data was analysed by constructing the representational models of the Distributed Cognition for Teamwork framework (DiCoT) to understand the context of interactions, focusing on system activities, information flows, physical layouts, artefacts, social structures, and system evolution, and by applying the principles associated with these models to identify patients’ interaction strategies and issues. This thesis brings five contributions to the study of situated interactions with HHT. Firstly, it provides an account of patients’ experiences of interacting with HHT. Secondly, it demonstrates the utility of DCog as a theoretical framework for understanding interactions with a HMD such as HHT. Thirdly, it develops new theoretical principles that help to understand how people distribute cognitive processes through time. Fourthly, it develops a Contextual Factors Analysis that facilitates the analysis of complex interaction strategies. Finally, it develops an overarching approach that augments DCog analysis from considering a system of representations to considering systems of activity-centric interactions.

In the text entry domain, the task of number entry is often overlooked despite the prevalence of number entry tasks in the real world. Number entry often occurs in safety critical contexts, such as the medical domain, where errors can lead to patient death. In order to prevent errors from happening, it is important to design devices that help the user in their number entry task, and guard against error. To do this effectively, more needs to be known about the task of number transcription so that appropriate design interventions can be created. Current research commonly uses randomly generated numbers in the evaluation of number entry interfaces. However, it is not clear that random numbers are appropriate in this context. The first half of the thesis builds on research that shows that the familiarity of a number can affect how it is read, and investigates how this finding impacts upon transcription of familiar numbers. This is investigated by replicating seminal transcription typing studies using both words and numbers. The results of these experiments suggest that familiar numbers are represented more strongly than non-familiar numbers in memory, and as a result familiar numbers are significantly faster to transcribe. This novel finding then motivates a series of studies that aim to reduce errors in a medical number entry task. First, a log analysis of hospital devices shows that there are clear patterns in the numbers used, providing evidence that medical workers are likely to be more familiar with some numbers rather than others. The knowledge of these frequently used numbers is then utilised in three novel approaches to number entry interface design. First, knowledge of the landscape of frequent numbers in this context is used to create a set of heuristics for the design of number entry interfaces. Second, an experiment shows that adapting the interface specifically for frequent number entry can speed up interaction. Finally an experiment explores how an understanding of the numbers used to program devices can be used to check for and prevent number transcription errors. This thesis highlights the importance of understanding the frequency and familiarity of num- bers used in specific contexts. It explores how this knowledge can improve both evaluation and design of number entry interfaces.

This project proves universal computation in the Game of Life cellular automaton by using a Turing machine construction. Existing proofs of universality in the Game of Life rely on a counter machine. These machines require complex encoding and decoding of the input and output and the proof of universality for these machines by the Church Turing thesis is that they can perform the equivalent of a Turing machine. A proof based directly on a Turing machine is much more accessible. The computational power available today allows powerful algorithms such as HashLife to calculate the evolution of cellular automata patterns sufficiently fast that an efficient universal Turing machine can be demonstrated in a conveniently short period of time. Such a universal Turing machine is presented here. It is a direct simulation of a Turing machine and the input and output are easily interpreted. In order to achieve full universal behaviour an infinite storage media is required. The storage media used to represent the Turing machine tape is a pair of stacks. One stack representing the Turing tape to the left of the read/write head and one for the Turing tape to the right. Collision based construction techniques have been used to add stack cells to the ends of the stacks continuously. The continuous construction of the stacks is equivalent to the formatting of blank media. This project demonstrates that large areas of a cellular automata can be formatted in real time to perform complex functions.

The main aim of this thesis was to identify, complement and refine the factors that contribute to users’ intention to purchase, satisfaction and attitude toward using a particular B2C online environment, as well as the causal relationships between these factors. A systematic literature review on Information System (IS), Market Research, and User Experience (UX), which has informed the design and development of a pilot study, has been conducted. Results have led to the conception of an online shopping decision-making (OSDM) model called ‘Episodic UX Model on Decision-Making’ (EUX-DM). It has been developed by integrating the established Technology Acceptance Model (TAM) as well as Information System Success Model (ISSM), and emerging UX models, and Expectation-Confirmation Theory (ECT). Results from analysing 305 responses to the web-based questionnaire aimed to evaluate EUX-DM verified its validity. In addition, after investigating the users’ preferences for the possible modifications related to the use of visual avatar in a particular B2C e-Commerce website for information presentation, another research focus has been placed on identifying the real conversational functions and their related communicational behaviour in designing male and female visual avatars’ facial expressions and body gestures. Following this, four different types of information presentations have been developed to be used in a contrived B2C online shopping environment, namely: (i) 2D static graphical and textual information, (ii) non-expressive avatars, (iii) avatars with facial expressions, (iv) and avatars with facial expressions and body gestures information presentations. Consequently, these information presentations were empirically investigated through two experimental studies. The outcomes of these studies indicated that the gender of the avatar and participants were found to be insignificant factors for any of the measured qualities, and the use of visual avatars with animated facial expressions and body gestures positively influenced customers’ usage attitude, intention to purchase and satisfaction.

The number of online citizen science projects has increased significantly over the past decade, yet some aspects of participation are poorly understood as is the motivation behind the involvement of the scientists who set up these projects, and the citizen scientists who take part. This thesis explores three different online citizen science projects (Foldit, Folding@home and Planet Hunters) using a case study approach and data collected through online surveys, interviews and participant observation. It explores the motivations that initiate and sustain participation, and it examines the various ways individuals can contribute to these projects. It also investigates how participants (both professional scientists and citizen scientists) interact online. A number of theoretical models of motivation and participation are considered. While many individuals register to take part in these projects, only a small proportion become active participants. These active citizen scientist volunteers are motivated to participate because they want to make a contribution to science or have a background interest in science. Scientists set up these projects in order to get help analysing large volumes of data, particularly those that require human pattern recognition or problem-solving skills. The complexity of the project task and the presence of certain technological features can affect how participants interact with each other, and how they contribute. Tasks that are complex are more likely to present opportunities for cooperation and collaboration, and may foster the development of online communities of practice. The findings of this research suggest that online citizen science projects have been important in making scientific research more open for a number of distributed volunteers. These individuals have responded to the challenges presented by these projects, increasing their scientific and technical understanding, and self-organising into various roles and teams in order to produce new knowledge.

Interaction design for domains that involve complex abstractions can present significant challenges. This problem is particularly acute in domains where users lack effective means to conceptualise and articulate relevant abstractions. In this thesis, we investigate the use of domain-specific conceptual metaphors to address the challenge of presenting complex abstractions, using tonal harmony as an extended case study. This thesis presents a methodology for applying domain-specific conceptual metaphors to interactions designs for music. This domain involves complex abstractions where users with any degree of domain knowledge may have difficulty in articulating concepts. The methodology comprises several parts. Firstly, the thesis explores methods for systematically guiding conversation between musicians to elicit speech that describes music using conceptual metaphors. Recommendations for the most suitable methods are made. Secondly, the thesis presents a methodology for identifying image schemas and conceptual metaphors from transcriptions of conversations between musicians. The methodology covers rules for identifying source image schemas and extrapolating conceptual metaphors. Thirdly, the thesis presents a methodology for evaluating existing music interaction designs using domain-specific conceptual metaphors. We demonstrate that this approach can be used to identify potential areas for improvement as well as tensions in the design between certain tasks or abstractions. Fourthly, the thesis presents a case study for the development of a conceptual metaphor-influenced design process. In the case study, a set of materials are developed to be used by participants in the design process to facilitate the mapping of conceptual metaphors to elements of an interaction design without requiring knowledge of Conceptual Metaphor Theory. Finally, a pilot study is presented integrating the results of the conceptual metaphor-influenced design process into a consistent and useful prototype system. Compromises and refinements to the design proposals made during the design process are discussed and the resulting system design is detailed.

No description available.