Neil D. Jones

TCS Journal 2007 Journal Article

Flow analysis of lazy higher-order functional programs

• Neil D. Jones
• Nils Andersen

In recent years much interest has been shown in a class of functional languages including HASKELL, lazy ML, SASL/KRC/MIRANDA, ALFL, ORWELL, and PONDER. It has been seen that their expressive power is great, programs are compact, and program manipulation and transformation is much easier than with imperative languages or more traditional applicative ones. Common characteristics: they are purely applicative, manipulate trees as data objects, use pattern matching both to determine control flow and to decompose compound data structures, and use a “lazy” evaluation strategy. In this paper we describe a technique for data flow analysis of programs in this class by safely approximating the behavior of a certain class of term rewriting systems. In particular we obtain “safe” descriptions of program inputs, outputs and intermediate results by regular sets of trees. Potential applications include optimization, strictness analysis and partial evaluation. The technique improves earlier work because of its applicability to programs with higher-order functions, and with either eager or lazy evaluation. The technique addresses the call-by-name aspect of laziness, but not memoization.

TCS Journal 1999 Journal Article

LOGSPACE and PTIME characterized by programming languages

• Neil D. Jones

A programming approach to computability and complexity theory yields more natural definitions and proofs of central results than the classical approach. Further, some new results can be obtained using this viewpoint. This paper contains new intrinsic characterizations of the well-known complexity classes PTIME and LOGSPACE, with no externally imposed resource bounds on time or space. LOGSPACE is proven identical with the decision problems solvable by read-only imperative programs on Lisp-like lists; and PTIME is proven identical with the problems solvable by recursive read-only programs.

STOC Conference 1993 Conference Paper

Constant time factors do matter

• Neil D. Jones

TCS Journal 1991 Journal Article

Static semantics, types, and binding time analysis

• Neil D. Jones

Part 1 of this paper is an analysis of problems concerning type systems and static semantics relevant to designing and implementing new programming languages. Part 2 proposes and exemplifies a way to derive a static semantics from a language's dynamic semantics, using a technique known as binding time analysis known from partial evaluation (Ershov's “mixed computation”) [20, 21]. The goal is to analyze the language's type structure during the design process without the need for hand construction of a type system. Ideally, one might automate the construction of a type checker, given only the dynamic semantics as input. In particular, binding time analysis of the interpreter program can be used to distinguish statically detectable errors from dynamic ones, and a static semantics is seen as a mechanism for deciding whether the program to be interpreted can give rise to any of the static errors. Our basic viewpoint is operational: to see how and where in the interpreter immediately observable type errors manifest themselves; to classify them as static or dynamic; and to design the static semantics to detect all static errors in a given program.

FOCS Conference 1980 Conference Paper

Complexity of Flow Analysis, Inductive Assertion Synthesis and a Language Due to Dijkstra

• Neil D. Jones
• Steven S. Muchnick

Two different methods of flow analysis are discussed, one a significant generalization of the other. It is shown that the two methods have significantly different intrinsic computational complexities. As an outgrowth of our observations it is shown that a feature of the programming language used by Dijkstra in A Discipline of Programming makes it unsuitable for compile-time type checking, thus suggesting that flow analysis is applicable to the design of programming languages, as well as to their implementation. It is also shown that program verification by the method of inductive assertions is very likely to lead to assertions whose lengths and proofs are not polynomially bounded in the size of the program being verified, even for very simple programs. This last observation casts further doubt on the practicality and relevance of mechanized verification of arbitrary programs.

TCS Journal 1977 Journal Article

Complexity of some problems in Petri nets

• Neil D. Jones
• Lawrence H. Landweber
• Y. Edmund Lien

We consider the complexity of several standard problems for various classes of Petri nets. In particular, the reachability problem, the liveness problem and the k-boundedness problems are analyzed. Some polynomial time and polynomial space complete problems for Petri nets are given. We then show that the problem of deciding whether a Petri net is persistent is reducible to reachability, partially answering a question of Keller. Reachability and boundedness are proved to be undecidable for the Time Petri net introduced by Merlin. Also presented is the concept of controllability, i. e. , the capability of a set of transitions to disable a given transition. We show that the controllability problem requires exponential space, even for 1-bounded nets.

TCS Journal 1976 Journal Article

Complete problems for deterministic polynomial time

• Neil D. Jones
• William T. Laaser

Log space reducibility allows a meaningful study of complexity and completeness for the class P of problems solvable in polynomial time (as a function of problem size). If any one complete problem for P is recognizable in log k (n) space (for a fixed k), or requires at least n c space (where c depends upon the program), then all complete problems in P have the same property. A variety of familiar problems are shown complete for P, including context-free emptiness, infiniteness and membership, establishing inconsistency of propositional formulas by unit resolution, deciding whether a player in a two-person game has a winning strategy, and determining whether an element is generated from a set by a binary operation.

STOC Conference 1974 Conference Paper

Complete Problems for Deterministic Polynomial Time

• Neil D. Jones
• William T. Laaser

The results of Cook and Karp ([K], [C]) aroused considerable interest for at least two reasons. First, the answer to a long-standing open question which had seemed peculiar to automata theory—whether deterministic and nondeterministic polynomial-time-bounded Turing machines are equivalent in power—was seen to be exactly equivalent to determining whether any of several familiar combinatorial problems can be solved by polynomial-time algorithms. Second, the existence of complete problems for NP 1 made it possible to replace an entire class of questions by a question about a single representative.Thus all of these combinatorial and automata-theoretic problems were essentially restatements of a single problem, such as: can satisfiability of a propositional formula be decided in polynomial time.

STOC Conference 1972 Conference Paper

Turing Machines and the Spectra of First-Order Formulas with Equality

• Neil D. Jones
• Alan L. Selman

In this paper we show that these similarities are not accidental - that spectra and context sensitive languages are closely related, and that their open questions are merely special cases of a family of open questions which relate to the difference (if any) between deterministic and non-deterministic time-or space-bounded Turing machines.