Search

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.

To the memory of Prof. Grigori Mints, Stanford UniversityBorn: June 7, 1939, St. Petersburg, RussiaDied: May 29, 2014, Palo Alto, California

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-Fraisse 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-Fraisse games.

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.

We present an interactive and automated theorem prover for free higher-order logic. Our implementation on top of the Isabelle/HOL framework utilizes a semantic embedding of free logic in classical higher-order logic. The capabilities of our tool are demonstrated with first experiments in category theory.

The paper presents in an informal way several conflicting viewpoints concerning concepts, theories, models, and applications of λ-calculus and the combinators.

Domain theory for denotational semantics is over thirty years old. There are many variations on the idea and many interesting constructs that have been proposed by many people for realizing a wide variety of types as domains. Generally, the effort has been to create categories of domains that are cartesian closed (that is, have products and function spaces interpreting typed lambda-calculus) and permit solutions to domain equations (that is, interpret recursive domain definitions and perhaps untyped lambda-calculus).

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.

Since 1989, the author has tried to show that it is possible to put a complete semester-long course in machine-held form. Several examples have been carried out (in Mathematica), and the paper reports on the experience, on the problems encountered, and on some suggestions for future developments.

Our basic premise is that the ability to construct and modify programs will not improve without a new and comprehensive look at the entire programming process. Past theoretical research, say, in the logics of programs, has tended to focus on methods for reasoning about individual programs; little has been done, it seems to us, to develop a sound understanding of the process of programming — the process by which programs evolve in concept and in practice. At present, we lack the means to describe the techniques of program construction and improvement in ways that properly link verification, documentation and adaptability.

Logic has been long interested in whether answers to certain questions are computable in principle, since the outcome puts bounds on the possibilities of formalization. More recently, precise comparisons in the efficiency of decision methods have become available through the developments in complexity theory. These, however, are applications to logic, and a big question is whether methods of logic have significance in the other direction for the more applied parts of computability theory. Programming languages offer an obvious opportunity as their syntactic formalization is well advanced; however, the semantical theory can hardly be said to be complete. Though we have many examples, we have still to give wide-ranging mathematical answers to these queries: What is a machine? What is a computable process? How (or how well) does a machine simulate a process? Programs naturally enter in giving descriptions of processes. The definition of the precise meaning of a program then requires us to explain what are the objects of computation (in a way, the statics of the problem) and how they are to be transformed (the dynamics). So far the theories of automata and of nets, though most interesting for dynamics, have formalized only a portion of the field, and there has been perhaps too much concentration on the finite-state and algebraic aspects. It would seem that the understanding of higher-level program features involves us with infinite objects and forces us to pass through several levels of explanation to go from the conceptual ideas to the final simulation on a real machine. These levels can be made mathematically exact if we can find the right abstractions to represent the necessary structures. The experience of many independent workers with the method of data types as lattices (or partial orderings) under an information content ordering, and with their continuous mappings, has demonstrated the flexibility of this approach in providing definitions and proofs, which are clean and without undue dependence on implementations. Nevertheless much remains to be done in showing how abstract conceptualizations can (or cannot) be actualized before we can say we have a unified theory.

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.

Here we enter into the discussion of our principal topic. Continuous lattices, as the authors have learned in recent years, exhibit a variety of different aspects, some are lattice theoretical, some are topological, some belong to topological algebra and some to category theory—and indeed there are others. We shall contemplate these aspects one at a time, and this chapter is devoted entirely to the lattice theory surrounding our topic.

Publisher Summary This chapter discusses that the connection with recursive functions is not at all like that of the combinatory arithmetic, because the integers are taken as primitive rather than as defined. This is hardly a defect, because the aim is to construct a model out of known objects. Further, what is taken as primitive in the corresponding formal language is a very brief selection of arithmetic notions—just the ones that would naturally present themselves—and the combinators are then used to define everything else. Because no combinator is excluded, the iterators previously used to introduce integers can be studied as well in the present context. Thus, nothing has been lost, but much has been gained, because now the possibility of a real cooperation can be seen between arithmetic (and later set-theoretic) notions and those of the λ-calculus. Because the original program of relative combinatory logic could never be carried out, these connections were never clear before.

In Chapter I we encountered the rich lattice-theoretic structure of continuous lattices. Perhaps even more typical for these lattices is their wealth of topological structure. The aim or the present chapter is to introduce topology into the study—a program to be continued in Chapter III.

Denotational Semantics is a framework for the formal description of programming language semantics. The main idea of Denotational Semantics is that each phrase of the described language is given a denotation: a mathematical object that represents the contribution of the phrase to the meaning of any program in which it occurs. Moreover, the denotation of each phrase is determined just by the denotations of its subphrases.This report consists of two chapters. The first, Semantic Domains, was written by Gunter and Scott. It is concerned with the theory of domains of denotations. The second, Denotational Semantics, was written by Mosses. It explains the formal notation used in denotational descriptions, and illustrates the major standard technigues for finding denotations of programming constructs.Both chapters are to appear in the forthcoming Handbook of Theoretical Computer Science (North-Holland).

With the exception of certain developments in Chapter II, notably Sections 2 and 4, we largely refrained from using category-theoretic language (even when we used its tools in the context of Galois connections). Inevitably, we have to consider various types of functions between continuous lattices, and this is a natural point in our study to use the framework of category theory.

Strictly speaking the structures to be used are not lattices since as posets they will lack the top (or unit) element, but the adjunction of a top will make them complete lattices. The closure properties as posets, then, are closure underinf of any non-empty subset and sup of directed subsets. A family of subsets of a set closed underintersections of non-empty subfamilies and unions of directed subfamilies is a special type of poset with the closure properties where additionally every element is the directed sup (union) of the finite (“compact”) elements it contains. We call such posets finitary domains. (With a top they are just the well known algebraic lattices.) The continuous domains can be defined as the continuous retracts of finitary domains. A mapping between domains is continuous if it preserves direct sups. A map of a domain into itself is aretraction if it is idempotent. Starting with a finitary domain, the range (= fixed-point set) of a continuous retraction — as a poset — is a continuous domain. Numberless characterizations of continuous domains, both topological and order-theoretic, can be found in [2]. For the most part in the lectures we shall concentrate on the finitary domains, but the continuous domains find an interest as a generalization of interval analysis and by the connection with spaces of upper-semicontinuous functions.

This note should perhaps be called just a ‘footnote’, since my concern here is in a reformulation of the definition. In a long sequence of papers Hintikka and his coworkers (see the bibliography, which I hope is reasonably complete) have introduced, developed, and applied the idea of this normal form and its constituents which are the main ingredient. Usually the description is quite syntactical — since after all these are normal forms of formulae written out in first-order predicate calculus. In the reformulation here the definition will be purely set theoretical: the constituents will correspond to certain sets of finite rank (‘types’ of finite depth) that could be considered quite apart from the usual formal language. However, the translation back to first-order logic is very quick, so not all that much is gained. The exercise of seeing the connection might nevertheless help the reader understand what exactly is being expressed in these normal forms.

It is one of our fundamental theses that major improvements in software engineering practice will come about only through the development and use of software development tools. This thesis is based on our belief that formal methods will ultimately have a far more profound effect on software engineering productivity than management based methods, programming language design, or fast hardware. But we also believe that formal methods, by their nature, are suitable for practical use only in mechanized systems. This is not to say that everything is to be automated; the point is that the actual formal steps must be automated even if most of the guidance for their use is to come from the user. This is the same kind of observation that prompted the developers of LCF to introduce the ML type structure to protect the notion of “theorem,” together with formal deductive structure that defines it, from the surrounding heuristic apparatus. It must be expected that heuristics will be under continual development, but a deductive system is fragile and will change only infrequently.

Publisher Summary The chapter presents an exposition of why the λ-calculus has models. The A-calculus was one of the first areas of research of Professor Kleene, in which the experience gained by him was surely beneficial in his later development of the recursive function theory. The chapter discusses a very short historical summary, and it is found that there is considerable overlap with CURRY. There is a review of the theory of functions and relations as sets leading up to the important notion of a continuous set mapping. The problem of the self-application of a function to itself as an argument is discussed in the chapter from a new angle. The model (essentially due to PLOTKIN) of the basic laws of λ -calculus thus results. The chapter describes self-application to recursion by the proof of David Park's theorem to the effect that the least fixed-point operator and the paradoxical combinator are the same in a wide class of well-behaved models. The connection thus engendered to recursion theory (r. e. sets) is outlined, and some remarks on recent results about ill-behaved models and on induction principles are discussed. The theme of type theory and a construction of an (η)-model with fewer -type distinctions is presented. There is a brief discussion of how to introduce more type distinctions into models via equivalence relations. The chapter also presents various points of philosophical disagreement with Professor Curry.

These notes were originally written for lectures on the semantics of programming languages delivered at Oxford during Michaelmas Term 1980. The purpose of the course was to provide the foundations needed for the method of denotational semantics; in particular I wanted to make the connections with recursive function theory more definite and to show how to obtain explicit, effectively given solutions to domain equations. Roughly, these chapters cover the first half of the book by Stoy, and he was able to continue the lectures the next term discussing semantical concepts following his text.

This introductory chapter serves as a convenient source of reference for certain basic aspects of complete lattices needed in the sequel. The experienced reader may wish to skip directly to Chapter I and the beginning of the discussion of the main topic of this book: continuous lattices, a special class of complete lattices.

It is very easy to confuse rules with axioms or even theorems. Consider for example this equation from arithmetic: 4·11=44. We may regard this as a truth about integers; or we may consider it a suggestion for an even more general rule about how easy it is to multiply a one-digit number by 11. From the first point of view we are concerned with content; while from the second, form>. In the case of arithmetic the confusion is not particularly troublesome, but in logic such mixups have wasted considerable time. The endless discussions of modal logic from a prime example. In [3] the author tried to argue that there was a point that had been generally overlooked about C.I. Lewis’ introduction of strict implication which turned on the distinction between rules of inference and tautologies. The conclusion reached there was that the Lewis System S4 was more interesting than it might seem even with the benifit of modern semantics. The crux of the argument was a formal metatheorem relating derived rules to derived theorems (Cf. [3], p. 803), but lack of space and time resulted in the exclusion of the proof of the result. The purpose of the present paper is to supply the details along with some general definitions about rules and derivations.

Publisher Summary This chapter discusses the background of formalization. The mathematical approach to logic, which means the study of formalized languages and their interpretations, has enjoyed considerable success—particularly in the past few years. In difficult areas such as practical logic, the trained philosopher who could perhaps identify some claims as knowledge and reject others commonly supposed to have that status are rarely to be found, preferring to build their own ivory towers. The word “logic,” fortunately or unfortunately, rings with varied overtones, not all of which are in harmony. One ear may be deaf to what excites another, and great care must be taken in claiming that the logic of a subject has been found or revised. Formal methods should only be applied when the subject is ready for them, when conceptual clarification is sufficiently advanced. In a way, the axiomatic method has been too successful. Propositional calculus, first-order logic, elementary geometry are all completely axiomatized. Incompleteness creeps into number theory, second-order logic, and set theory, but few people seem to worry.

Everyone knows how much more pleasant it is to give advice than to take it. Everyone knows how little heed is taken of all the good advice he has to offer. Nevertheless, this knowledge seldom restrains anyone, least of all the present author. He has been noting the confusions, misdirections of emphasis, and duplications of effort current in studies of modal logic and is, by now, anxious to disseminate all kinds of valuable advice on the subject. Thus he is very happy that the Irving meeting has provided such a suitable and timely forum and hopes that all this advice can provoke some useful discussion — at least in self-defense. The time really seems to be ripe for a fruitful development of modal logic, if only we take care to purify and simplify the foundations. A quite flexible framework is indeed possible: the old puzzles can be brushed aside, and one can begin to provide meaningful applications.

In mathematics after some centuries of development the semantical situation is very clean. This may not be surprising, as the subject attracts people who enjoy clarity, generality, and neatness. On the one hand we have our concepts of mathematical objects (numbers, relations, functions, sets), and on the other we have various formal means of expression. The mathematical expressions are generated for the most part in a very regular manner, and every effort is made to supply all expressions with denotations. (This is not always so easy to do. The theory of distributions, for example, provided a non-obvious construction of denotations for expressions of an operational calculus. The derivative operator was well serviced, but one still cannot multiply two distributions.)

Publisher Summary This chapter discusses the background of formalization. The mathematical approach to logic, which means the study of formalized languages and their interpretations, has enjoyed considerable success—particularly in the past few years. In difficult areas such as practical logic, the trained philosopher who could perhaps identify some claims as knowledge and reject others commonly supposed to have that status are rarely to be found, preferring to build their own ivory towers. The word “logic,” fortunately or unfortunately, rings with varied overtones, not all of which are in harmony. One ear may be deaf to what excites another, and great care must be taken in claiming that the logic of a subject has been found or revised. Formal methods should only be applied when the subject is ready for them, when conceptual clarification is sufficiently advanced. In a way, the axiomatic method has been too successful. Propositional calculus, first-order logic, elementary geometry are all completely axiomatized. Incompleteness creeps into number theory, second-order logic, and set theory, but few people seem to worry.