We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.

A modeloid, a certain set of partial bijections, emerges from the idea to abstract from a structure to the set of its partial automorphisms. It comes with an operation, called the derivative, which is inspired by Ehrenfeucht-Fraïssé games. In this paper we develop a generalization of a modeloid first to an inverse semigroup and then to an inverse category using an axiomatic approach to category theory. We then show that this formulation enables a purely algebraic view on Ehrenfeucht-Fraïssé games.

A shallow semantical embedding of free logic in classical higher-order logic is presented, which enables the off-the-shelf application of higher-order interactive and automated theorem provers for the formalisation and verification of free logic theories. Subsequently, this approach is applied to a selected domain of mathematics: starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. As a side-effect of this work some (minor) issues in a prominent category theory textbook have been revealed. The purpose of this article is not to claim any novel results in category theory, but to demonstrate an elegant way to “implement” and utilize interactive and automated reasoning in free logic, and to present illustrative experiments.

The ordinary untyped λ-calculus has a λ-theoretic model proposed in two related forms by Scott and Plotkin in the 1970s. Recently Scott showed how to introduce probability by extending these models with random variables. However, to reason about correctness and to add further features, it is useful to reinterpret the construction in a higher-order Boolean-valued model involving a measure algebra. We develop the semantics of an extended stochastic λ-calculus suitable for modeling a simple higher-order probabilistic programming language. We exhibit a number of key equations satisfied by the terms of our language. The terms are interpreted using a continuation-style semantics with an additional argument, an infinite sequence of coin tosses, which serves as a source of randomness. We also introduce a fixpoint operator as a new syntactic construct, as β-reduction turns out not to be sound for unrestricted terms. Finally, we develop a new notion of equality between terms interpreted in a measure algebra, allowing one to reason about terms that may not be equal almost everywhere. This provides a new framework and reasoning principles for probabilistic programs and their higher-order properties.

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting framework is intended as a setting for the logical and categorical study of relative computability.

Partial equivalence relations (and categories of these) are a standard tool in semantics of type theories and programming languages, since they often provide a cartesian closed category with extended definability. Using the theory of exact categories, we give a category-theoretic explanation of why the construction of a category of partial equivalence relations often produces a cartesian closed category. We show how several familiar examples of categories of partial equivalence relations fit into the general framework.

A class of Partial Equivalence Relations (PERs) is described such that the resulting full subcategory of the realizability universe has the expected properties of a good category of CPOs; that is, it is a Cartesian closed category and every endomorphism has a canonical fixed point. Moreover, the reflection functor into the subcategory of strict maps (usually called the “lifting operation”) yields a good notion of “partial map,” a necessary condition if one wishes to maintain a connection between strict maps and partial maps. It is shown that all functors that arise in practice have canonical invariant objects; hence a host of domain equations are guaranteed to have solutions.

A search is conducted for a class of PERs (partial equivalence relations on the natural numbers) such that the resulting full subcategory has the expected properties of any good category of CPOs: it should be a CCC (Cartesian closed category) and every endomorphism should have a canonical fixed point. Moreover the reflection functor (usually called the lifting operation) should yield a good notion of partial map. The following topics are discussed: conventions, partial-map classifiers, ExPERS, ExPERS as domains, reflectivity of strict maps, multicorreflectivity of strict maps, the extensional natural numbers, domain equations, and intrinsic descriptions.>

The author's discovery of domains and domain-theoretic models for the lambda -calculus in 1969 is discussed, along with the research of others working in the area at that time.>

The meaning of many kinds of expressions in programming languages can be taken as elements of certain spaces of “partial” objects. In this report these spaces are modeled in one universal domain ${\bf P} \omega $, the set of all subsets of the integers. This domain renders the connection of this semantic theory with the ordinary theory of number theoretic (especially general recursive) functions clear and straightforward.

In attempting to reconstruct Rose's proof of Lemma 3.2 of [1], the present authors found what is apparently a different and simpler method, which moreover leads to a far stronger conclusion. We are operating in the Heyting prepositional calculus as formulated on p. 3 of [1] or on pp. 82 and 101 of [2], and shall make use of relevant theorems on pp. 90, 113–119 of [2]. We shall use a, b, c, w, x, y, z as propositional variables. We say that a conjunction is simple if each factor has one of the forms: (i) a, (ii) ¬a, (iii) a⊃b, (iv) a⊃(b∨c), (v) (a&b)⊃c, (vi) (a⊃b)⊃c.

It is a scientific platitude that there can be neither precise control nor prediction of phenomena without measurement. Disciplines are diverse as cosmology and social psychology provide evidence that it is nearly useless to have an exactly formulated quantitative theory if empirically feasible methods of measurement cannot be developed for a substantial portion of the quantitative concepts of the theory. Given a physical concept like that of mass or a psychological concept like that of habit strength, the point of a theory of measurement is to lay bare the structure of a collection of empirical relations which may be used to measure the characteristic of empirical phenomena corresponding to the concept. Why a collection of relations? From an abstract standpoint a set of empirical data consists of a collection of relations between specified objects. For example, data on the relative weights of a set of physical objects are easily represented by an ordering relation on the set; additional data, and a fortiori an additional relation, are needed to yield a satisfactory quantitative measurement of the masses of the objects. The major source of difficulty in providing an adequate theory of measurement is to construct relations which have an exact and reasonable numerical interpretation and yet also have a technically practical empirical interpretation. The classical analyses of the measurement of mass, for instance, have the embarrassing consequence that the basic set of objects measured must be infinite. Here the relations postulated have acceptable numerical interpretations, but are utterly unsuitable empirically. Conversely, as we shall see in the last section of this paper, the structure of relations which have a sound empirical meaning often cannot be succinctly characterized so as to guarantee a desired numerical interpretation.