1,720,959 research outputs found
A Cartesian Closed Category for Random Variables
Full text linkWe present a novel, yet rather simple construction within the traditional framework of Scott domains to provide semantics to probabilistic programming, thus obtaining a solution to a long-standing open problem in this area. We work with the Scott domain of random variables from a standard and fixed probability space - -the unit interval or the Cantor space - -to any given Scott domain. The map taking any such random variable to its corresponding probability distribution provides a Scott continuous surjection onto the probabilistic power domain of the underlying Scott domain, which preserving canonical basis elements, establishing a new basic result in classical domain theory. If the underlying Scott domain is effectively given, then this map is also computable. We obtain a Cartesian closed category by enriching the category of Scott domains by a partial equivalence relation to capture the equivalence of random variables on these domains. The constructor of the domain of random variables on this category, with the two standard probability spaces, leads to four basic strong commutative monads, suitable for defining the semantics of probabilistic programming
Composable Partial Multiparty Session Types
No full textWe introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its components without knowing any suitable global type nor the types of missing parts. Incompatible types, due to e.g. miscommunications or deadlocks, are detected at the merging phase. We apply these types to a process calculus, for which we prove subject reduction and progress, so that well-typed systems never violate the prescribed constraints. Therefore, partial session types support the development of systems by incremental assembling of components
Lazy algorithms for exact real arithmetic
Full text linkIn this article we propose a new representation for the real numbers. This representation can be conveniently used to implement exact real number computation with a lazy programming languages. In fact the new representation permits the exploitation of hardware implementation of arithmetic functions without generating the granularity problem. Moreover we present a variation of the Karatsuba algorithm for multiplication of integers. The new algorithm performs exact real number multiplication in a lazy way and has a lower complexity than the standard algorithm. © 2004 Elsevier B.V. All rights reserved
A definitional implementation of the LAX logical framework LLFP in CoQ, for supporting fast and loose reasoning
Full text linkThe Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to
provide a conceptual framework for integrating different proof development tools, thus allowing for
external evidence and for postponing, delegating, or factoring-out side conditions. In particular,
LLFP allows for reducing the number of times a proof-irrelevant check is performed. In this paper
we give a shallow, actually definitional, implementation of LLFP in Coq, i.e. we use Coq both as
host framework and oracle for LLFP. This illuminates the principles underpinning the mechanism
of Lock-types and also suggests how to possibly extend Coq with the features of LLFP. The derived
proof editor is then put to use for developing case-studies on an emerging paradigm, both at logical
and implementation level, which we call fast and loose reasoning following Danielsson et alii [6].
This paradigm trades off efficiency for correctness and amounts to postponing, or running in parallel,
tedious or computationally demanding checks, until we are really sure that the intended goal can be
achieved. Typical examples are branch-prediction in CPUs and optimistic concurrency control
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
LF+ in Coq for fast-and-loose reasoning
Full text linkWe develop the metatheory and the implementation, in Coq, of the novel logical framework LF+ and discuss several of its applications. LF+ generalises research work, carried out by the authors over more than a decade, on Logical Frameworks conservatively extending LF and featuring lock-type constructors L-P(N:sigma)[center dot]. Lock-types capture monadically the concept of inhabitability up-to. They were originally introduced for factoring-out, postponing, or delegating to external tools the verification of time-consuming judgments, which are morally proof-irrelevant, thus allowing for integrating different sources of epistemic evidence in a unique Logical Framework. Besides introducing LF+ and its "shallow" implementation in Coq, the main novelty of the paper is to show that lock-types are also a very flexible tool for expressing in Type Theory several diverse cognitive attitudes and mental strategies used in ordinary reasoning, which essentially amount to reasoning up-to, as in e.g. Typical Ambiguity provisos or co-inductive Coq proofs. In particular we address the encoding of the emerging paradigm of fast-and-loose reasoning, which trades off efficiency for correctness. This paradigm, implicitly used normally in naive Set Theory, is producing considerable impact also in computer architecture and distributed systems, when branch prediction and optimistic concurrency control are implemented
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
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
lambda!-calculus, Intersection Types, and Involutions
Full text linkAbramsky’s affine combinatory algebras are models of affine combinatory logic, which refines standard combinatory logic in the direction of Linear Logic. Abramsky introduced various universal models of computation based on affine combinatory algebras, consisting of partial involutions over a suitable formal language {of moves}, in order to discuss reversible computation in a Geometry of Interaction setting. We investigate partial involutions from the point of view of the model theory of lambda!-calculus. The latter is a refinement of the standard lambda-calculus, corresponding to affine combinatory logic. We introduce intersection type systems for the lambda!-calculus, by extending standard intersection types with a !_u-operator. These induce affine combinatory algebras, and, via suitable quotients, models of the lambda!-calculus. In particular, we introduce an intersection type system for assigning principal types to lambda!-terms, and we state a correspondence between the partial involution interpreting a combinator and the principal type of the corresponding lambda!-term. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction
- …
