1,721,087 research outputs found
Probabilistic Non-Determinism
No full textMuch of theoretical computer science is based on use of inductive complete partially ordered sets (or ipos). The aim of this thesis is to extend this successful theory to make it applicable to probabilistic computations. The method is to construct a "probabilistic powerdomain" on any ipo to represent the outcome of a probabilistic program which has outputs in the original ipo. In this thesis it is shown that evaluations (functions which assign a probability to open sets with various conditions) form such a powerdomain. Further, the powerdomain is a monadic functor on the categoy Ipo.
For restricted classes of ipos a powerdomain of probability distributions, or measures which only take values less than one, has been constructed (by Saheb-Djahromi). In the thesis we show that this powerdomain may be constructed for continuous ipos where it is isomorphic to that of evaluations.
The powerdomain of evaluations is shown to have a simple Stone type duality between it and sets of upper continuous functions. This is then used to give a Hoare style logic for an imperative probabilistic language, which is the dual of the probabilistic semantics.
Finally the powerdomain is used to give a denotational semantics of a probabilistic metalanguage which is an extension of Moggi's lambda-c-calculus for the powerdomain monad. This semantics is then shown to be equivalent to an operational semantics
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
The Proof Theory and Semantics of Intuitionistic Modal Logic
No full textPossible world semantics underlies many of the applications of modal logic in computer science and philosophy. The standard theory arises from interpreting the semantic definitions in the ordinary meta-theory of informal classical mathematics. If, however, the same semantic definitions are interpreted in an intuitionistic meta-theory then the induced modal logics no longer satisfy certain intuitionistically invalid principles. This thesis investigates the intuitionistic modal logics that arise in this way.
Natural deduction systems for various intuitionistic modal logics are presented. From one point of view, these systems are self-justifying in that a possible world interpretation of the modalities can be read off directly from the inference rules. A technical justification is given by the faithfulness of translations into intuitionistic first-order logic. It is also established that, in many cases, the natural deduction systems induce well-known intuitionistic modal logics, previously given by Hilbert-style axiomatizations.
The main benefit of the natural deduction systems over axiomatizations is their susceptibility to proof-theoretic techniques. Strong normalization (and confluence) results are proved for all of the systems. Normalization is then used to establish the completeness of cut-free sequent calculi for all of the systems, and decidability for some of the systems.
Lastly, techniques developed throughout the thesis are used to establish that those intuitionistic modal logics proved decidable also satisfy the finite model property. For the logics considered, decidability and the finite model property presented open problems
Configuration Structures
Full text linkIn this paper the correspondence between safe Petri nets
and event structures, due to Nielsen, Plotkin and Winskel,
is extended to arbitrary nets without self-loops, under the
collective token interpretation. To this end we propose a
more general form of event structure, matching the expressive power of such nets. These new event structures and
nets are connected by relating both notions with configuration structures, which can be regarded as representations of
either event structures or nets that capture their behaviour
in terms of action occurrences and the causal relationships
between them, but abstract from any auxiliary structure.
A configuration structure can also be considered logically, as a class of propositional models, or—equivalently—as a propositional theory in disjunctive normal from. Converting this theory to conjunctive normal form is the key
idea in the translation of such a structure into a net.
For a variety of classes of event structures we characterise the associated classes of configuration structures in
terms of their closure properties, as well as in terms of the
axiomatisability of the associated propositional theories by
formulae of simple prescribed forms
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Ordinals and Interactive Programs
No full textThe work reported in this thesis arises from the old idea, going back to the origins of constructive logic, that a proof is fundamentally a kind of program.
If proofs can be considered as programs, then one might expect that proof theory should have much to contribute to the theory of programming. This has indeed turned out to be the case. Various technologies developed in proof theory are now widely used in computer science for formulating and investigating programming languages and logics connected with them.
Yet there is a vigorous and venerable part of proof theory which has so far had little impact in computer science, namely ordinal-theoretic proof theory. This focuses on proofs of wellfoundedness, usually expressed in the form of a schema of transfinite induction with respect to a representation of an initial segment of the countable ordinals. Proof theory of this kind is connected with what it is that limits the capacity of a proof system to 'see into the transfinite.
If proofs can be considered as programs, what kind of program is a proof of wellfoundedness? My hypothesis is that the limitations of a formal system for writing proofs of wellfoundedness reflect its limitations as a system in which to program strategies for defeating ones opponent in a certain kind of game. In recent computer science, games have proved invaluable as models for describing patterns of interaction between a system and its environment.
I cannot claim to have substantiated this hypothesis, but only to have taken a few steps in that direction. The work reported in the thesis lies in three areas.
First, I present a framework for dependently typed programming in the style advocated by Martin-Löf. The novelties here are connected with bringing the type-theoretic approach to programming that comes from the Curry-Howard correspondence closer to the calculational approach in the categorical tradition that comes from Lambek and Lawvere. A particular challenge is to find a smooth and practical way of encoding inductive and coinductive definitions.
Second, I have investigated a number of ways of modeling interactive systems and transition systems in a constructive context. The focus here is on models with a direct computational interpretation, that can actually be used in programming. The approach is inspired by a construction due to Petersson and Synek. It is shown how one may represent game-theoretic strategies of various kinds using these models.
Finally, I give a construction of provable ordinals within a Martin-Löf style type theory that has a type of natural numbers, and an external sequence of universes closed under generalised Cartesian products. The locus of the ideas for this construction lie more in conventional proof theory, and were the basis for a conjecture made by me almost thirty years ago in work that I then abandoned. What is new here is the concept of a 'lens'. This is a predicate transformer that has been implicit in the construction of proofs of wellfoundedness since Gentzen. I hope this concept may be of some use in an algebraic, systematic approach to setting lower bounds on the proof-theoretic strength of more extensive type theories
Appropriate Similarity Measures for Author Cocitation Analysis
Full text linkWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
A computational model of learning
Full text linkThe program described learns to improve its performance in
the playing of a game, from experience. The main objectives
of the project are that the system should observe the
following principles:
1) The program should not rely on any special evaluation
functions, which would embody domain-specific information.
2) Initial knowledge of the domain should be minimal,
and further knowledge gained should be assimilated in
terms of prior knowledge 3) The system of representation employed should as far
as possible be independent of the domain, again
avoiding the incorporation of domain-specific information.
In customary Artificial Intelligence terms, the program is
referred to as existing in a domain or environment. The
model has a goal within this domain and has available
certain actions which it may take in order to achieve its
goal. The goal is represented as a Structure. This term
will be used throughout to denote a set of objects from
the domain, constrained by various domain-pertinent relationships. The actions, goals and objects are the
initial known facts of the environment. The program has
an innate ability to plan simple sequences of actions to
achieve its goals. Inevitably, these plans do not take
into account enough of the nature of the domain and prove
inadequate. In such events the descriptive abilities of
the program are invoked to correct the deficiency, and the
program's model of its environment is enriched
On a thermodynamic approach to biomolecular interaction networks
Full text linkWe explore the direct and inverse problem of thermodynamics in the context of
rule-based modelling. The direct problem can be concisely stated as obtaining
a set of rewriting rules and their rates from the description of the energy
landscape such that their asymptotic behaviour when t → ∞ coincide. To
tackle this problem, we describe an energy function as a finite set of connected
patterns P and an energy cost function e which associates real values to each of
these energy patterns.We use a finite set of reversible graph rewriting rules G to
define the qualitative dynamics by showing which transformations are possible.
Given G and P, we construct a finite set of rules Gp which i) has the same
qualitative transition system as G and ii) when equipped with rates according
to e, defines a continuous-time Markov chain that has detailed balance with
respect to the invariant probability distribution determined by the energy
function. The construction relies on a technique for rule refinement described
in earlier work and allows us to represent thermodynamically consistent
models of biochemical interaction networks in a concise manner.
The inverse problem, on the other hand, is to i) check whether a rule-based
model has an energy function that describes its asymptotic behaviour and
if so ii) obtain the energy function from the graph rewriting rules and their
rates. Although this problem is known to be undecidable in the general case,
we find two suitable subsets of Kappa, our rule-based modelling framework
of choice, were this question can be answer positively and the form of their
energy functions described analytically
- …
