Search

Finite automata are considered in this paper as instruments for classifying finite tapes. Each one-tape automaton defines a set of tapes, a two-tape automaton defines a set of pairs of tapes, et cetera. The structure of the defined sets is studied. Various generalizations of the notion of an automaton are introduced and their relation to the classical automata is determined. Some decision problems concerning automata are shown to be solvable by effective algorithms; others turn out to be unsolvable by algorithms.

The general mathematical criterion for the solvability of finite systems of linear inequalities is applied to some specific situations from measurement theory. Three examples are treated in detail, and in each case the necessary and sufficent conditions for existence of a suitable real-valued (utility) function on a finite structure are obtained.

LEMMA 1. There is a 0-dimensional Hausdorff space OC such that (i) the class of open sets of SC is closed under the formation of 13-termed intersections for every 13

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.

It is well known that one can build models of full higher-order dependent-type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra. But the idea of categories of PERs and ERs (total equivalence relations) can be applied to other structures as well. In particular, we can easily define the category of ERs and equivalence-preserving continuous mappings over the standard category Top0 of topological T0-spaces; we call these spaces (a topological space together with an ER) equilogical spaces and the resulting category Equ. We show that this category—in contradistinction to Top0—is a cartesian closed category. The direct proof outlined here uses the equivalence of the category Equ to the category PEqu of PERs over algebraic lattices (a full subcategory of Top0 that is well known to be cartesian closed from domain theory). In another paper with Carboni and Rosolini (cited herein), a more abstract categorical generalization shows why many such categories are cartesian closed. The category Equ obviously contains Top0 as a full subcategory, and it naturally contains many other well known subcategories. In particular, we show why, as a consequence of work of Ershov, Berger, and others, the Kleene–Kreisel hierarchy of countable functionals of finite types can be naturally constructed in Equ from the natural numbers object N by repeated use in Equ of exponentiation and binary products. We also develop for Equ notions of modest sets (a category equivalent to Equ) and assemblies to explain why a model of dependent type theory is obtained. We make some comparisons of this model to other, known models.

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.

The first topologies defined on a lattice directly from the lattice ordering (that is, Birkhoffs order topology and Frink’s interval topology) involved “symmetrical” definitions—the topologies assigned to L and to Lop were identical. The guiding example was always the unit interval of real numbers in its natural order, which is of course a highly symmetrical lattice. The initial interest was in such questions as which lattices became compact and/or Hausdorff in these topologies. The Scott topology stands in strong contrast to such an approach. Indeed it is a “one-way” topology, since, for example, all the open sets are always upper sets; thus, for nontrivial lattices, the T0-separation axiom is the strongest it satisfies. Nevertheless, we saw in Chapter II that the Scott topology provides many links between continuous lattices and general topology in such classical areas as the theory of semicontinuous functions and in the study of lattices of closed (compact, convex) sets (ideals) in many familiar structures.

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.

Opectral theory plays an important and well-known role in such areas as the theory of commutative rings, lattices, and of C*-algebras, for example. The general idea is to define a notion of “prime element” (more often: ideal element) and then to endow the set of these primes with a topology. This topological space is called the “spectrum” of the structure. One then seeks to find how algebraic properties of the original structure are reflected in the topological properties of the spectrum; in addition, it is often possible to obtain a representation of the given structure in a concrete and natural fashion from the spectrum.

Sad to report, my own facility in music is only amateurish, but my interest in classical music has been with me nearly all my life. I was lucky to have had several interesting music teachers, and they opened my ears and made a serious level of appreciation possible. One of my high-school teachers, whom I admired very much, gave me a book on acoustics to read, and it was there I first found the name of Helmholtz. The year was about 1946, and the location was in the wilds of California, a far-away land of strange savages. A couple of years later I was actually able to find a copy of Helmholtz’s treatise in English translation in the State Library in Sacramento. I was completely fascinated by the relationships between music and mathematics that Helmholtz was able to show—many of them I realize are still controversial today—and the effort of understanding the mathematics was directly responsible for my later concentration on that subject at the university. All of this reading on acoustics was quite outside the standard school curriculum, please understand, and helps confirm my belief that lives are more determined by accident than by design.

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.

The purpose of the theory of domains is to give models for spaces on which to define computable functions. The kinds of spaces needed for denotational sematics involve not only spaces of higher type (e.g. function spaces) but also spaces defined recursively (e.g. reflexive domains). Also required are many special domain constructs (or functors) in order to create the desired structures. There are several choices of a suitable category of domains, but the basic one which has the simplest properties is the one sometimes called consistently complete algebraic cpo's. This category of domains is studied in this paper from a new, and it is to be hoped, simpler point of view incorporating the approaches of many authors into a unified presentation. Briefly, the domains of elements are represented set theoretically with the aid of structures called information systems. These systems are very familiar from mathematical logic, and their use seems to accord well with intuition. Many things that were done previously axiomatically can now be proved in a straightfoward way as theorems. The present paper discusses many examples in an informal way that should serve as an introduction to the subject.

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 The convention adopted in this chapter is that usual geometrical notions do not involve infinite sets or infinite sequences of points. In specific, a standard Euclidean space can be a vector space over the field of real numbers having any finite or infinite linear dimension. Geometrical properties of spaces are formulated in terms of geometrically meaningful notions. The elementary geometrical properties are identified with the properties of a space expressible in sentences of the first-order predicate logic in terms of the geometrical relations over the space. The chapter presents specific geometric results and a general theorem in the theory of models of the first-order logic. This general result is then applied to geometry and it is shown that there are no elementary geometrical properties distinguishing any two infinite dimensional Euclidean spaces.

Publisher Summary This chapter focusses on extending the topological interpretation to intuitionistic analysis. The universally quantified three-variable consequences of the axioms of order have been discussed. A universal sentence is a consequence in Heyting's predicate calculus (HPC) of a given universal axiom if its matrix is a propositional consequence of a finite number of substitution instances of the axiom using the variables. The chapter discusses the general metamathematical implications for the theory of the topological model of intuitionistic analysis. The chapter discusses the important step that is taken for enlarging the model to encompass arbitrary (extensional) real functions. The main result is the verification in the model of Brouwer's theorem on continuity: all functions are uniformly continuous on closed intervals.

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.

Publisher Summary Probability concepts nowadays are presented in the standard framework of the Kolmogorov axioms. A sample space is given together with an σ-field of subsets, the events, and an σ-additive probability measure defined on this σ-field. It is more natural in many situations to assign probabilities to statements rather than sets. It may be mathematically useful to translate everything into a set-theoretical formulation, but the step is not always necessary or even helpful. The main task is to carry over the standard concepts from ordinary logic to what might be called “probability logic.” Indeed ordinary logic is a special case: the assignment of truth values to formulas can be viewed as assigning probabilities that are either 0 (for false) or 1 (for true). In a sense, the symmetric probability systems are opposite to ordinary relational systems.

Publisher Summary This chapter discusses models of various type free calculi. The range of arguments or range of values of a function should consist wholly or partly of functions. The derivative, as this notion appears in the elementary differential calculus, is a familiar mathematical example of a function for which both ranges consist of functions. Formal logic provides other examples; thus the existential quantifier, according to the present account, is a function for which the range of arguments consists of propositional functions, and the range of values consists of truth values. A function could be a “scheme” for a type of process, which would become definite when presented with an argument. The value would be extracted as an end result of the process. Two functions that are extensionally the same might compute, however, by quite different processes.

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 focuses on the Quine's individuals. Professor Quine has suggested that in relation to the theories of membership, it can be possible to allow for the existence of nonclasses or individuals by interpreting the formula “x Є y” as synonymous with “x = y”—in the case that y is an individual. The fact that the situation did not arise in the course of one particular development is not a conclusive argument. However, it seems clear that Professor Quine does not imagine such a deduction is possible nor would anyone else believe this. Nothing supports belief like proof, and it will be the purpose of this chapter to demonstrate that if Quine's axioms are consistent. For these purposes, the chapter imagines NF formulated in first-order logic with identity and with the descriptive operator. The proof given in the chapter for NF is finitary and in no doubt a similar argument can be applied to ML.

Titanium nitride (TiN) is a candidate material for hard and wear resistant coatings on metallic substrates such as titanium (Ti), stainless steel and aluminum. Coating processes include chemical vapor deposition, ion implantation, plasma and thermal nitriding under vacuum and controlled environments. The motivation for the present research is to develop a laser plasma process for high rate formation of TiN coatings on Ti substrates at near-atmospheric pressures. Laser induced plasma generated by a pulsed CO2 laser was used to excite a Ti substrate. The species in the vapor plume were characterized by optical emission spectroscopy. Spatially and temporally resolved spectral characterization was performed as a function of laser power, position of the substrate relative to the focal plane, pulse parameters, and shielding gases. These experiments are a first step in understanding laser assisted plasma deposition of nitride/oxy-nitride coatings on titanium metal under atmospheric conditions. Results indicate a window of optimal process parameters for developing titanium nitride coatings.