An exponential lower bound on the circuit complexity of deciding the weak monadic second-order theory of one successor (WS1S) is proved. Circuits are built from binary operations, or 2-input gates, which compute arbitrary Boolean functions. In particular, to decide the truth of logical formulas of length at most 610 in this second-order language requires a circuit containing at least 10 125 gates. So even if each gate were the size of a proton, the circuit would not fit in the known universe. This result and its proof, due to both authors, originally appeared in 1974 in the Ph.D. thesis of the first author. In this article, the proof is given, the result is put in historical perspective, and the result is extended to probabilistic circuits.*

It is impossible to add a combinator to PCF to achieve full abstraction for models such as Berry’s stable domains in a way analogous to the addition of the “parallel-or” combinator that achieves full abstraction for the familiar complete partial order (cpo) model. In particular, we define a general notion of rewriting system of the kind used for evaluating simply typed $\lambda $-terms in Scott’s PCF. Any simply typed $\lambda $-calculus with such a “PCF-like” rewriting semantics is shown necessarily to satisfy Miler’s Context Lemma. A simple argument demonstrates that any denotational semantics that is adequate for PCF, and in which certain simple Boolean functionals exist, cannot be fully abstract for any extension of PCF satisfying the Context Lemma. An immediate corollary is that stable domains cannot be fully abstract for any extension of PCF definable by PCF-like rules.

This is a complete exposition of a tight version of a fundamental theorem of computational complexity due to Levin: The inherent space complexity of any partial function is very accurately specifiable in a Π1 way, and every such specification that is even Σ2 does characterize the complexity of some partial function, even one that assumes only the values 0 and 1.

In the concurrent language CCS, two programs are considered the same if they are bisimilar . Several years and many researchers have demonstrated that the theory of bisimulation is mathematically appealing and useful in practice. However, bisimulation makes too many distinctions between programs. We consider the problem of adding operations to CCS to make bisimulation fully abstract. We define the class of GSOS operations, generalizing the style and technical advantages of CCS operations. We characterize GSOS congruence in as a bisimulation-like relation called ready-simulation . Bisimulation is strictly finer than ready simulation, and hence not a congruence for any GSOS language.

Introduces a unary "self-synchronization" operation on concurrent processes that synchronizes concurrent transitions within a process. Standard parallel synchronization and communicating action refinement operations can be reduced to simple combinations of self-synchronization and unsynchronized noncommunicating operations. Modifying familiar fully abstract process semantics, so that actions are replaced by action multisets (steps), typically yields semantics that are fully abstract for processes with self-synchronization.>

Distinctions between concurrent processes based on observable outcomes of computational experiments are examined. The equivalence determined by a general class of experiments involving duplication of processes can be characterized by a notion of ready simulation resembling, but strictly coarser than, Milner's bisimulation equivalence.

Familiar beta eta -equational reasoning on lambda -terms is unsound for proving observational congruences when termination of the standard lazy interpreter is taken into account. A complete logic, based on sequents, for proving termination-observational congruences between simply-typed terms without constants is developed. It is shown that the theory, like that of beta eta -reasoning in the ordinary types lambda -calculus, is decidable. The authors examined the termination behavior of the functional language PCF under the standard interpreters.>

To help understand the reason for continuity in denotational semantics, the author offers some global comments on goodness-to-fit criteria between semantic domains and symbolic evaluators. The appendices provide the key parts of a proof that Scott domains give a computationally adequate and fully abstract semantics for lambda calculus with simple recursive types.>

Bisimulation is the primitive notion of equivalence between concurrent processes in Milner's Calculus of Communicating Systems (CCS); there is a nontrivial game-like protocol for distinguishing nonbisimular processes. In contrast, process distinguishability in Hoare's theory of Communicating Sequential Processes (CSP) is determined solely on the basis of traces of visible actions. We examine what additional operations are needed to explain bisimulation similarly—specifically in the case of finitely branching processes without silent moves. We formulate a general notion of Structured Operational Semantics for processes with Guarded recursion (GSOS), and demonstrate that bisimulation does not agree with trace congruence with respect to any set of GSOS-definable contexts. In justifying the generality and significance of GSOS's, we work out some of the basic proof theoretic facts which justify the SOS discipline.

The Store Model of Halpern-Meyer-Trakhtenbrot is shown—after suitable repair—to be a fully abstract model for a limited fragment of ALGOL in which procedures do not take procedure parameters. A simple counter-example involving a parameter of program type shows that the model is not fully abstract in general. Previous proof systems for reasoning about procedures are typically sound for the HMT store model, so it follows that theorems about the counter-example are independent of such proof systems. Based on a generalization of standard cpo based models to structures called locally complete partial orders (lcpo's), improved models and stronger proof rules are developed to handle such examples.

The model theory of simply typed and polymorphic (second-order) lambda calculus changes when types are allowed to be empty. For example, the “polymorphic Boolean” type really has exactly two elements in a polymorphic model only if the “absurd” type ∀t.t is empty. The standard β-ε axioms and equational inference rules which are complete when all types are nonempty are not complete for models with empty types. Without a little care about variable elimination, the standard rules are not even sound for empty types. We extend the standard system to obtain a complete proof system for models with empty types. The completeness proof is complicated by the fact that equational “term models” are not so easily obtained: in contrast to the nonempty case, not every theory with empty types is the theory of a single model.

In programming languages of universal power, the computational integers must be distinguished from the classical integers because of the “divergent” integer. Even the equational theory corresponding to evaluation of integer expressions is distinct from the theory of classical integers, and classical reasoning about computational integers yields inconsistencies. We show that there exist “programming languages”, actually extensions of the polymorphic lambda calculus, that have tremendous computing power and yet whose computational integers, or any other algebraically specified abstract data type, coincide with their classical counterpart. In particular, the equational theory of the programming language is a conservative extension of the theory of the underlying base types as given by algebraic data type specifications.

A function has a dependent type when the type of its result depends upon the value of its argument. Dependent types originated in the type theory of intuitionistic mathematics and have reappeared independently in programming languages such as CLU, Pebble, and Russell. Some of these languages make the assumption that there exists a type-of-all-types which is its own type as well as the type of all other types. Girard proved that this approach is inconsistent from the perspective of intuitionistic logic. We apply Girard's techniques to establish that the type-of-all-types assumption creates serious pathologies from a programming perspective: a system using this assumption is inherently not normalizing, term equality is undecidable, and the resulting theory fails to be a conservative extension of the theory of the underlying base types. The failure of conservative extension means that classical reasoning about programs in such a system is not sound.

Regular terms with the Kleene operations $ \cup $, ; and $ * $ can be thought of as operators on languages, generating other languages. An equation $\tau _1 = \tau _2 $ between two such terms is said to be satisfiable just in case languages exist which make this equation true. We show that the satisfiability problem even for $ * $-free regular terms is undecidable. Similar techniques are used to show that a very natural extension of the Process Logic of Harel, Kozen and Parikh is undecidable.

Denotational semantics for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing) is given by translating programs into an appropriately typed l-calculus. Procedures are entirely explained at a purely functional level - independent of the interpretation of program constructs - by continuous models for l-calculus. However, the usual (cpo) models are not adequate to model local storage allocation for blocks because storage overflow presents an apparent discontinuity. New domains of store models are offered to solve this problem.

The termination assertion pq means that whenever the formula p is true, there is an execution of the possibly nondeterministic program S which terminates in a state in which q is true. Termination assertions are more tractable technically than the partial correctness assertions usually treated in the literature. Termination assertions are studied for a programming language which includes local variable declarations, calls to undeclared global procedures, and nondeterministic recursive procedures with call-by-address and call-by-value parameters. By allowing formulas p and q to place conditions on global procedures, we provide a method for reasoning about programs with calls to global procedures based on hypotheses about procedure input-output behavior. The set of first-order termination assertions valid over all interpretations is completely axiomatizable without reference to the theory of any interpretation. Although uninterpreted assertions have limited expressive power, the set of valid termination assertions defines the semantics of recursive programs in the sense of Meyer and Halpern [10]. Thus the axiomatization constitutes an axiomatic definition of the semantics of recursive programs.

A precise defmttion is given of how partial correctness or termination assertions serve to define the semantics of program schemes Assertions involving only formulas of f'trst-order predicate calculus are proved capable of defining program scheme semanUcs, and effective ax,om systems for deriving such assertions are described.Such axiomatic definitions are possible despite the limited expressive power of predicate calculus.

A property of Boolean functions of n variables is described and shown to imply lower bounds as large as $\Omega (n\log n)$ on the number of literals in any Boolean formula for any function with the property. Formulas over the full basis of binary operations $( \wedge , \oplus ,{\text{ etc.}})$ are considered. The lower bounds apply to all but a vanishing fraction of symmetric functions, in particular, to all threshold functions with sufficiently large threshold and to the “congruent to zero modulo k” function for $k > 2$. In the case $k = 4$, the bound is optimal.

Sufficient conditions are given for partial correctness assertions to determine the input-output semantics of quite general classes of programming languages. This determination cannot be unique unless states which are indistinguishable by predicates in the assertions are identified. Even when indistinguishable states are identified, partial correctness assertions may not suffice to determine program semantics.

Regular terms with the Kleene operations ∪,;, and * can be thought of as operators on languages, generating other languages. An equation r1 = r2 between two such terms is said to be satisfiable just in case languages exist which make this equation true. We show that the satisfiability problem even for *-free regular terms is undecidable. Similar techniques are used to show that a very natural extension of the Process Logic of Harel, Kozen and Parikh is undecidable.

If the reachability set of a Petri net or vector addmon system is fimte, it can be effectively constructed.Furthermore, this finiteness is decidable The complexity of dectsion procedures for the containment and equality problem of f'lmte reachabihty sets rs investigated, and it is shown by reducing a bounded version of Hilbert's Tenth Problem to the finite containment problem that these two problems are extremely hard--that, in fact, the complexity of each decision procedure exceeds any primitive recursive functmn mfimtely often The funte containment and equality problems are thus the first uncontrived decidable problems which are not primitive recursive KEY WORDS AND PHRASES.incluston problem, reachabihty set, Petn net, pdmmve recurs~ve complexity

We consider three kinds of mathematical objects which can be designated as the "meaning" or "semantics" of programs: binary relations between initial and final states, binary relations on predicates (partial-correctness semantics), and functionals from predicates to predicates (predicate transformers).We exhibit various formal specification mechanisms: induction on program syntax, axioms, and deductive systems.We show that each kind of semantics can be specified by several different mechanisms.As long as arbitrary predicates on states are permitted, each kind of semantics uniquely determines the others, with the sole exception of the weakest precondition semantics for nondeterministic programs.

A precise definition is given of how partial correctness or termination assertions serve to specify the semantics of classes of program schemes. Assertions involving only formulas of first order predicate calculus are proved capable of specifying program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic specifications are possible despite the limited expressive power of predicate calculus.

We study the expressive power of various versions of Dynamic Logic and compare them with each other as well as with standard languages in the logical literature. One version of Dynamic Logic is equivalent to the infinitary logic LCKω1ω, but regular Dynamic Logic is strictly less expressive. In particular, the ordinals ωω and ω ω.2 are indistinguishable by formulas of regular Dynamic Logic.

Hoare and Lauer [1974] have advocated using a variety of styles of programming language definitions to fit the variety of users from implementers to program verifiers. They consider the question of whether different definitions and specifications determine the same language by showing that the definitions are what they call "consistent". However, their treatment skirts the question of whether their definitions can each be taken to specify the language adequately. Although, as we will show, any one of the kinds of semantics they discuss -- operational, relational, deductive -- can be used to specify meaning uniquely, Hoare and Lauer do not make the case in their paper. In fact, both their relational and deductive definitions are satisfied by several different semantics, only one of which is desired.Thus, the main point of this paper is to clarify the characteristics of a proper specification of language semantics and to formulate alternative specifications each of which is equally good as the language definition. We basically agree with Hoare and Lauer that several specifications can and should be given, but are disturbed by confusions about such specifications, some of which are illustrated in their paper. In particular we refer to confusions between the mathematical object which is designated to be the meaning of a program and methods for specifying that object; the similar confusion between predicate and expression; between consistency and equivalence of two definitions; between completeness of a theory and its having a unique model. While these issues are familiar in mathematical logic, we take this opportunity to survey them in the context of programming language semantics.This paper can be read without prior familiarity with Hoare and Lauer's paper. The authors plan another paper extending this work which will include a more comprehensive bibliography.

We show that “looping” of while-programs can be expressed in Regular First-Order Dynamic Logic, disproving a conjecture made in [Harel-Pratt 1978]. In addition we show that the expressive power of quantifier-free Dynamic Logic increases when nondeterminism is introduced in the programs that are part of formulae of Dynamic Logic. Allowing assignments of random values to variables increases the expressive power even further.

A new lower bound on the computational complexity of the theory of real addition and several related theories is established: any decision procedure for these theories requires either space 2εn or nondeterministic time 2εn2 for some constant ε > O and infinitely many n.

We consider the problem of identifying an unknown value xε{1,2,...,n} using only comparisons of x to constants when as many as E of 'the comparisons may receive erroneous answers. For a continuous analogue of this problem we show that there is a unique strategy that is optimal in the worst case. This strategy for the continuous problem is then shown to yield a strategy for the original discrete problem that uses log2n+E.log2log2n+O(E.log2E) comparisons in the worst case. This number is shown to be optimal even if arbitrary “Yes-No” questions are allowed.

AaSTancr.A recurslve padding technique is used to obtain conditions sufficient for separation of nondetermlmsttc multltape Turlng machine time complexity classes If T2 is a running time and Tl(n + 1) grows more slowly than T~(n), then there is a language which can be accepted nondetermmlstlcally within time bound T~ but which cannot be accepted nondetermlnlStlcally within time bound T1.If even T~(n + f(n)) grows more slowly than Tz(n), where f is the very slowly growing "rounded reverse" of some real-time countable function, then there is such a language over a single-letter alphabet.The strongest known dmgonalization results for both deterministic and nondetermlmstlc time complexity classes are reviewed and orgamzed for comparison with the results of the new padding technique KEY WOADS ^NO PHaASrS: Turlng machine, complexity class, complexity hierarchy, time complexity, nondetermmism, padding, recursmn theorem, dmgonahzatmn, single-letter alphabet CR CAa~ORIES 5 23, 5.25, 5.26, 5 27 This paper represents a portion of the first author's Ph D d~ssertatlon [25] written at M.

Dynamic logic is a generalization of first order logic in which quantifiers of the form “for all χ...” are replaced by phrases of the form “after executing program α...”. This logic subsumes most existing first-order logics of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness, yet is more closely related to classical first-order logic than any other proposed logic of programs. We consider two issues: how hard is the validity problem for the formulae of dynamic logic, and how might one axiomatize dynamic logic? We give bounds on the validity problem for some special cases, including a Π02-completeness result for the partial correctness theories of uninterpreted flowchart programs. We also demonstrate the completeness of an axiomatization of dynamic logic relative to arithmetic.

The uniform word problem for commutative semigroups (UWCS) is the problem of determining from any given finite set of defining relations and any pair of words, whether the words describe the same element in the commutative semigroup defined by the relations. The effective decidability of this classical algebraic problem was first explicitly noted by Malcev [1958] and Emilichev [1958], though in retrospect this result can be seen to be contained in the earlier work of König [1903] and Hermann [1926] on polynomial ideals.

Let C(n)k be the Boolean function of n variables that equals one iff the number of arguments equal to one is a multiple of k. It is shown that every Boolean expression for C(n)k, allowing all of the 16 binary connectives, has size exceeding εn log n/log log n, ε> 0. This result follows from a general criterion relating the minimum size expression for a Boolean function to the kinds of subfunctions obtainable through restriction. Lower bounds on formula size for several other functions are obtained. In some cases, the lower bounds are nearly achievable by known constructions.

Let be the set of recursive functions computable by machines using at most t(x) computation steps on argument x, for all but finitely many inputs x. We call t a name for the complexity class . Suppose we allow our machines to run longer, say h(x, t(x)) steps on argument x, where h is some fixed recursive function. One might expect that, for large enough h, permitting our machines to run longer by an amount h will always allow us to compute new functions, i.e., is a proper subset of . This turns out not to be the case: The “gap theorem” ([2], [3]) implies that for every recursive h there exists a recursive t such that . However, if we restrict our attention to names from a certain subclass of the recursive functions, then we can indeed uniformly increase the size of our -classes. Informally, we call a recursive function t “honest” if some machine computes t(x) in roughly t(x) steps for each argument x. (A precise definition is given in Definition 1 below.) Then according to the “compression theorem” [1], there exists a single recursive function h such that, for every honest t, is a proper subset of . Thus the phenomenon of the gap theorem is avoided by restricting attention to honest functions. It is a surprising consequence of the “honesty theorem” of McCreight and Meyer ([4], [5]) that there is no loss of generality in this restriction. Namely, for any recursive function t there is an honest recursive function t′ such that .

This paper contains several results yielding pairs of problems which don't help each other's solution, and therefore which may be said to be complex for “different reasons.” Statements are formalized and results proved within Blum complexity theory, generalized to relative algorithms. The approach is fairly intuitive; all details appear in [1] and [2].

The equivalence problem for Kleene's regular expressions has several effective solutions, all of which are computationally inefficient. In [1], we showed that this inefficiency is an inherent property of the problem by showing that the problem of membership in any arbitrary context-sensitive language was easily reducible to the equivalence problem for regular expressions. We also showed that with a squaring abbreviation ( writing (E)2 for E×E) the equivalence problem for expressions required computing space exponential in the size of the expressions.

Restricted programming languages, for example primitive recursive definition schemes, are very often not nearly as succinct in describing primitive recursive functions as a general programming language [1]. We show that as one increases the power of programming languages, one can obtain economies in program size by any recursive amount for even very simple functions. This parallels a situation in the arithmetic hierarchy, where it is possible to get a recursively enumerable set whose smallest recursively enumerable index is much larger than the smallest index for the same set considered, say, as a set recursively enumerable in ø'.

The main result of this paper is that, given a Turing machine with several readwrite heads per tape, one can effectively construct an equivalent multitape Turing machine with a single read-write head per tape, which runs at precisely the same speed.This result implies that serial storage may be used to handle files requiring several points of immediate two-way read-write access without interruptions for rewinds, etc.It also yields simplified proofs of several results in the literature of computational complexity.

The complexity of a computable function can be measured by considering the time or space required to compute its values. Particular notions of time and space arising from variants of Turing machines have been investigated by R. W. Ritchie [14], Hartmanis and Stearns [8], and Arbib and Blum [1], among others. General properties of such complexity measures have been characterized axiomatically by Rabin [12], Blum [2], Young [16], [17], and McCreight and Meyer [10]. In this paper the speed-up and super-speed-up theorems of Blum [2] are generalized to speed-up by arbitrary total effective operators. The significance of such theorems is that one cannot equate the complexity of a computable function with the running time of its fastest program, for the simple reason that there are computable functions which in a very strong sense have no fastest programs. Let φi be the ith partial recursive function of one variable in a standard Gödel numbering of partial recursive functions. A family Φ0, Φ1, … of functions of one variable is called a Blum measure on computation providing (1) domain (φi) = domain (Φi), and (2) the predicate [Φi(x) = m] is recursive in i, x and m. Typical interpretations of Φi(x) are the number of steps required by the ith Turing machine (in a standard enumeration of Turing machines) to converge on input x, the space or number of tape squares required by the ith Turing machine to converge on input x (with the convention that Φi(x) is undefined even if the machine fails to halt in a finite loop), and the length of the shortest derivation of the value of φi(x) from the ith set of recursive equations.

The structure of the functions computable in time or space bounded by t is investigated for recursive functions t. The t-computable classes are shown to be closed under increasing recursively enumerable unions; as a corollary the primitive recursive functions are shown to equal the t-computable functions for a certain recursive t. Any countable partial order can be isomorphically embedded in the family of t-computable classes partially ordered by set inclusion. For any recursive t, there is a recursive t' which is (approximately) equal to an actual running time such that the t-computable functions equal the t'-computable functions.

It is shown that a short proof of the equivalence of star-free and group-free regular events is possible if one is willing to appeal to the Krohn-Rhodes machine decomposition theorem.

The problem of solving sequential Boolean equations is shown to be equivalent to the problem of finding whether there exists a path on a labeled graph for every sequence of labels. Algorithms are given for testing whether a solution exists, and if a solution with a finite delay exists. In case of existence of solutions the algorithms provide them.

In this paper a relationship among distinct Pn+1, cycles, distinct stable maximum transient feedback shift registers of order n+1, and stable feedback shift registers of order n will be presented. In the course of the discussion, two algorithms will be introduced. The first will provide a one-to-one mapping between distinct stable feedback shift registers of order n and distinct stable maximum-transient feedback shift registers of order n+1. The second will provide a one-to-one mapping between distinct maximum transient feed-back shift registers of order n+1 and distinct Pn+1, cycles. As a corollary to these relationships, an enumeration of the stable feed-back shift registers is obtained.