Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation

We prove the correctness of an algorithm for normalizing untyped combinator terms by evaluation. The algorithm is written in the functional programming language Haskell, and we prove that it lazily computes the combinatory Böhm tree of the term. The notion of combinatory Böhm tree is analogous to the usual notion of Böhm tree for the untyped lambda calculus. It is defined operationally by repeated head reduction of terms to head normal forms. We use formal neighbourhoods to characterize finite, partial information about data, and define a Böhm tree as a filter of such formal neighbourhoods. We also define formal topology style denotational semantics of a fragment of Haskell following Martin-Löf, and let each closed program denote a filter of formal neighbourhoods. We prove that the denotation of the output of our algorithm is the Böhm tree of the input term. The key construction in the proof is a “glueing” relation between terms and semantic neighbourhoods which is defined by induction on the latter. This relation is related to the glueing relation which was earlier used for proving the correctness of normalization by evaluation algorithm for typed combinatory logic.     

Unifications,deunifications, and their complexity

The execution of a Prolog program can be viewed as a sequence of unifications and backtracks over unifications. We study the time requirement of executing a sequence of such operations (the unify-deunify problem). It is shown that the well-known set union problem is reducible to this problem, even in the case when no function symbols are allowed (the Datalog unify-deunify problem). As the set union problem requires nonlinear time on a large class of algorithms, the same holds for the unify-deunify problem. Thus the linearity of single unifications does not give a complete picture of the time complexity of Prolog primitives. We discuss the methods for executing sequences of Datalog unifications used in Prolog interpreters and show that some of them require even quadratic time in the worst case. Complementing these results, we show that if the number of variables occurring in one clause is bounded by a constant, then the Datalog unify-deunify problem can be solved in linear time.A preliminary version of this paper appeared in the Third International Conference on Logic Programming, London, July 1986. This work was supported by the Academy of Finland and by TEKES.     

On specifications,subset types and interpretation of proposition in type theory

In this paper we discuss some practical aspects of using type theory as a programming and specification language, where the viewpoint is to use it not only as a basis for program synthesis but also as a programming language with a programming logic allowing us to do ordinary verification.The subset type has been added to type theory in order to avoid irrelevant information in programs. We give an example of a proof which illustrates the problems that may occur if the subset type is used in specifications when we have the standard interpretation of propositions as types. Harrop-formulas and Squash are then discussed as solutions to these problems. It is argued that they are not acceptable from a practical point of view.An extension of the theory to include the two new judgment forms:A is a proposition, andA is true, is then given and explained in terms of the old theory. The logical constants are no longer identified with the corresponding type theoretical constants, but propositions are interpreted as Gödel formulas, which allow us to introduce and justify logical rules similar to rules for classical logic. The interpretation is extended to include predicates defined by using reflections of the ordinary definition of Gödel formulas in a type of small propositions.The programming example is then revisited and stronger elimination rules are discussed.     

Terminating general recursion

In Martin-Löf's type theory, general recursion is not available. The only iterating constructs are primitive recursion over natural numbers and other inductive sets. The paper describes a way to allow a general recursion operator in type theory (extended with propositions). A proof rule for the new operator is presented. The addition of the new operator will not destroy the property that all well-typed programs terminate. An advantage of the new program construct is that it is possible to separate the termination proof of the program from the proof of other properties.Dedicated to Peter Naur on the occasion of his 60:th birthday.     

The paradox of trees in type theory

We show how to represent a paradox similar to Russell's paradox in Type Theory withW-types and a type of all types, and how to use this in order to represent a fixed-point operator in such a theory. It is still open whether such a construction is possible without theW-type.This research was partly supported by ESPIRIT Basic Research Action Logical Frameworks.     

Amortized analysis of some disk scheduling algorithms: SSTF,SCAN, andN-StepSCAN

The amortized analysis is a useful tool for analyzing the time-complexity of performing a sequence of operations. The disk scheduling problem involves a sequence of requests in general. In this paper, the performances of representative disk scheduling algorithms,SSTF, SCAN, andN-StepSCAN, are analyzed in the amortized sense. A lower bound of the amortized complexity for the disk scheduling problem is also derived. According to our analysis,SCAN is not only better thanSSTF andN-StepSCAN, but also an optimal algorithm. Various authors have studied the disk scheduling problem based on some probability models and concluded that the most acceptable performance is obtained fromSCAN. Our result therefore supports their conclusion.This research was supported by the National Science Council, Taiwan R. O. C. under contract: NSC80-0408-E009-11.     

An axiomatic treatment ofSIMD assignment

The aims of this article are to provide (i) an abstract characterisation of SIMD computation and (ii) a simple proof theory for SIMD programs. A soundness result is stated and the consequences of the result are analysed. The use of the axiomatic theory is illustrated by a proof of a parallel implementation of Euclid's GCD algorithm.     

Partial inductive definitions as type-systems for λ-terms

To every partial inductive definitionD, a natural deduction calculusND(D) is associated. Not every such system will have the normalization property; specifically, there are definitionsD for whichND(D) permits non-normalizable deductions. A lambda calculus is formulated where the terms are used as objects realizing deductions inND(D), and is shown to have the Church-Rosser property. SinceND(D) permits non-normalizable deductions, there will be typed terms which are non-normalizable. It will, for example, be possible to obtain a typed fixed-point operator.     

Partial correctness of exits from concurrent structures

A rudimentary exit-mechanism from the parallel command of the language fragment CSP is introduced. A method for embedding invariants in a standard partial correctness system with pre-and postconditions is presented. Proof rules for exits from concurrent systems are introduced, and a simple data flow system is verified.     

An axiomatic semantics for nested concurrency

We give transformation rules for the concurrent parts of Hoare's language CSP, transforming concurrent CSP programs into nondeterministic, sequential programs.On the basis of these transformations we define an axiomatic semantics for CSP with nested concurrency.This axiomatic system includes a rule for binary, associative process composition, enabling modular verification dealing with parts of concurrent systems as well as full programs.The proof system is fully abstract, in the sense that the internal structure of processes is irrelevant in the specification inasmuch it is not externally observable.An outline of a verification of a recursive, concurrent sorter is given as an example.     

The equational part of proofs by structural induction

We study proofs by structural induction and the equational subproofs that emerge from inductive proofs. Due to the role these subproofs play in the proof process, existing theorem provers tend to use ad hoc methods rather than existing semi-decision methods for equational proofs. We present a formalized version of these ad hoc methods, and prove some results on its completeness. Finally we present some examples on the formalized method used in fully automatized proofs by structural induction.This research was partly supported by The Research Council of Norway, division NAVF.     

On the design of reactive systems

The notion of joint actions provides a framework in which the granularity of atomic actions can be refined in the design of concurrent systems. An example of a telephone exchange is elaborated to demonstrate the feasibility of this approach for reactive systems and to illustrate transformations that are justifiable in such a process. Particular problems arise when a refinement would allow new interleavings of semantically relevant events. The meaning of a reactive computation is specified in a way that makes this possible.Dedicated to Peter Naur on the occasion of his 60th birthday     

Minimizing the number of transitions with respect to observation equivalence

Labeled transition systems (lts) provide an operational semantics for many specification languages. In order to abstract unrelevant details of lts's, manybehavioural equivalences have been defined; here observation equivalence is considered. We are interested in the following problem:Given a finite lts, which is the minimal observation equivalent lts corresponding to it? It is well known that the number of states of an lts can be minimized by applying arelational coarsest partition algorithm. However, the obtained lts is not unique (up to the renaming of the states): for an lts there may exist several observation equivalent lts's which have the minimal number of states but varying number of transitions. In this paper we show how the number of transitions can be minimized, obtaining a unique lts.     

Remarks on Martin-Löf's partial type theory

In this paper we discuss Martin-Löf's partial type theory, that is type theory with general recursion, and in particular the consequences of the presence of a fixed point operator. We model Martin-Löf's logical framework domain-theoretically in the category of conditional upper semi lattices and parametrizations thereof. An interpretation of a type of sets in the logical framework, which defines partial type theory with one universe, is finally described.During the preparation of this paper, the first author was supported by the Swedish Natural Science Research Council as a PhD-student in mathematical logic.     

Generating a random cyclic permutation

We prove correct an algorithm that, givenn>0, stores in arrayb[0..n–1] a random cyclic permutation of the integers in 0..n–1, with each cyclic permutation having equal probability of being stored inb. The algorithm was developed by Sattolo; our contribution is to present a more convincing proof using standard program-proving methods.Dedicated to Peter Naur on the occasion of his 60th birthdayThis research was supported by the NSF under grant DCR-8320274.Visiting Cornell from the Computer Science Department, Jiangxi Normal University, Nanchang, People's Republic of China.     

Disk allocation methods for binary Cartesian product files

Since a file is usually stored on a disk, the response time to a query is dominated by the disk access time. In order to reduce the disk access time, a file can be stored on several independently accessible disks. In this paper, we discuss the problem of allocating buckets in a file among disks such that the maximum disk accessing concurrency can be achieved. We are particularly concerned with the disk allocation problem for binary Cartesian product files. A new allocation method is first proposed for the cases when the number (m) of available disks is a power of 2. Then it is extended to fit the cases wherem is not a power of 2. The proposed algorithm has a near strict optimal performance for a partial match query in which the number of unspecified attributes is greater than a small number (5 or 6).This work was supported in part by NSF Grant DCR-8405498.     

Time considered irrelevant for real-time systems

Various manifestations of the time-as-a-proxy phenomenon in specification of computing problems are considered. It is argued that unless the time-related considerations constitute an essential part of natural (physical) problems, safer specifications are obtained from avoiding short-cuts offered by introduction of time-related notions. This methodological principle is illustrated by examples from several fields: digital control and simulation, design of operator's interface and communication protocols.Dedicated to Peter Naur on the occasion of his 60th birthday     

An adaptation of a root finding method to searching ordered disk files revisited

In the present report, Interpolation search, Fast search and Pegasus method are compared with respect to their performance in searching ordered disk files for several key distributions. The aim is to study the effect of the page capacity on searching performance. Cost metric is the number of page accesses and not key comparisons. Numerical results are illustrated and a new approximate formula is derived giving an estimate of the number of page accesses for the case of the Interpolation algorithm under uniform distributions.     

Theo: An interactive proof development system

This paper presents an interactive, tactic-driven, proof development system, a Theorem Prover calledTheo. Both the meta and the object levels of our theorem prover are logics presented in Typol. Typol is the programming language that implements Natural Semantics, a semantics developed at Inria and pioneered by G. Plotkin under the name Structural Operational Semantics. So Theo is written in Typol and helps the user to build proofs in an object logic also written in Typol. Tactics and tacticals are written in Typol. Other important features of Theo are the form chosen for representing proofs, and the way proofs are performed. The internal form of the proofs is very compact, expressed with combinators, that can be related to the -calculus used in Automath and its descendants. Meanwhile, Theo performs proofs by a pure calculus on proofs, using a resolution rule. Proofs may be incomplete and may contain logical variables. Theo is developed under the Centaur system, as well as Typol. This system provides a modern graphic man-machine interface that Theo uses, for the user's advantage.     

Analysis of recursive batched interpolation search

For an ordered file of records with uniformly distributed key values, we examine an existing batched searching algorithm based on recursive use of interpolation searches. The algorithm, called Recursive Batched Interpolation Search (RBIS) in this paper, uses a divide-and-conquer technique for batched searching. The expected-case complexity of the algorithm is shown to beO(m loglog (2n/m) +m), wheren is the size of the file andm is the size of the query batch. Simulations are performed to demonstrate the savings of batched searching using RBIS. Also, simulations are performed to compare alternative batched searching algorithms which are based on either interpolation search or binary search. When the file's key values are uniformly distributed, the simulation results confirm that interpolation-search based algorithms are superior to binary-search based algorithms. However, when the file's key values are not uniformly distributed, a straight-forward batched interpolation search deteriorates quickly as the batch size increases, but algorithm RBIS still outperforms binary-search based algorithms when the batch size passes a threshold value.