arXiv subjects

M. H. van Emden

Publications and source records attributed to M. H. van Emden.

At least 19 recordsLinked to original sources

arXiv2020

Egyptian multiplication and some of its ramifications

Multiplication and exponentiation can be defined by equations in which one of the operands is written as the sum of powers of two. When these powers are non-negative integers, the operand is integer; without this restriction it is a fraction. The defining equation can be used in evaluation mode or in solving mode. In the former case we obtain "Egyptian" multiplication, dating from the 17th century BC. In solving mode we obtain an efficient algorithm for division by repeated subtraction, dating from the 20th century AD. In the exponentiation case we also distinguish between evaluation mode and solving mode. Evaluation mode yields a possibly new algorithm for raising to a fractional power. Solving mode yields the algorithm for logarithms invented by Briggs in the 17th century AD.

math.NA↗

arXiv2018

Correct by construction

Matrix code allows one to discover algorithms and to render them in code that is both compilable and is correct by construction. In this way the difficulty of verifying existing code is avoided. The method is especially important for logically dense code and when precision programming is called for. The paper explains both these concepts. Logically dense code is explained by means of the partition stage of the Quicksort algorithm. Precision programming is explained by means of fast exponentiation.

cs.PL↗

arXiv2018

Beyond Structured Programming

The correctness of a structured program is, at best, plausible. Though this is a step forward compared to what came before, it falls short of verified correctness. To verify a structured program according to Hoare's method one is faced with the problem of finding assertions to fit existing code. In 1971 this mode of verification was declared by Dijkstra as too hard to be of practical use---he advised that proof and code were to grow together. A method for doing this was independently published by Reynolds in 1978 and by van Emden in 1979. The latter was further developed to attain the form of matrix code. This form of code not only obviates the need of fitting assertions to existing code, but helps in discovering an algorithm that reaches a given postcondition from a fixed precondition. In this paper a keyboard-editable version of matrix code is presented that uses E.W. Dijkstra's guarded commands as starting point. The result is reached by using Floyd's method rather than Hoare's as starting point.

cs.PL↗

arXiv2015

Contributions to the compositional semantics of first-order predicate logic

Henkin, Monk and Tarski gave a compositional semantics for first-order predicate logic. We extend this work by including function symbols in the language and by giving the denotation of the atomic formula as a composition of the denotations of its predicate symbol and of its tuple of arguments. In addition we give the denotation of a term as a composition of the denotations of its function symbol and of its tuple of arguments.

cs.LO↗

arXiv2015

Logic programming beyond Prolog

A logic program is an executable specification. For example, merge sort in pure Prolog is a logical formula, yet shows creditable performance on long linked lists. But such executable specifications are a compromise: the logic is distorted by algorithmic considerations, yet only indirectly executable via an abstract machine. This paper introduces relational programming, a method that solves the difficulty with logic programming by a separation of concerns. It requires three texts: (1) the axioms, a logical formula that specifies the problem and is not compromised by algorithmic considerations, (2) the theorem, a logical formula that expresses the idea of the algorithm and follows from the axioms, and (3) the code, a transcription of the theorem to a procedural language. Correctness of the code relies on the logical relationship of the theorem with the axioms and relies on an accurate transcription of the theorem to the procedural language. Sorting is an example where relational programming has the advantage of a higher degree of abstractness: the data to be sorted can be any data type in C++ (the procedural language we use in our examples) that satisfies the axioms of linear order, while the pure-Prolog version is limited to data structures in the form of linked cells. We show another advantage of relational programs: they have a model-theoretic and fixpoint semantics equivalent to each other and analogous to those of pure Prolog programs.

cs.PL↗

arXiv2015

The lambda mechanism in lambda calculus and in other calculi

A comparison of Landin's form of lambda calculus with Church's shows that, independently of the lambda calculus, there exists a mechanism for converting functions with arguments indexed by variables to the usual kind of function where the arguments are indexed numerically. We call this the "lambda mechanism" and show how it can be used in other calculi. In first-order predicate logic it can be used to define new functions and new predicates in terms of existing ones. In a purely imperative programming language it can be used to provide an Algol-like procedure facility.

cs.PL↗

arXiv2014

Programming in logic without Prolog

Logic can be made useful for programming and for databases independently of logic programming. To be useful in this way, logic has to provide a mechanism for the definition of new functions and new relations on the basis of those given in the interpretation of a logical theory. We provide this mechanism by creating a compositional semantics on top of the classical semantics. In this approach verification of computational results relies on a correspondence between logic interpretations and a class definition in languages like Java or C++. The advantage of this approach is the combination of an expressive medium for the programmer with, in the case of C++, optimal use of computer resources.

cs.LO↗

arXiv2013

Matrix Code

Matrix Code gives imperative programming a mathematical semantics and heuristic power comparable in quality to functional and logic programming. A program in Matrix Code is developed incrementally from a specification in pre/post-condition form. The computations of a code matrix are characterized by powers of the matrix when it is interpreted as a transformation in a space of vectors of logical conditions. Correctness of a code matrix is expressed in terms of a fixpoint of the transformation. The abstract machine for Matrix Code is the dual-state machine, which we present as a variant of the classical finite-state machine.

cs.PL↗

arXiv2013

Constraint Propagation as Information Maximization

This paper draws on diverse areas of computer science to develop a unified view of computation: (1) Optimization in operations research, where a numerical objective function is maximized under constraints, is generalized from the numerical total order to a non-numerical partial order that can be interpreted in terms of information. (2) Relations are generalized so that there are relations of which the constituent tuples have numerical indexes, whereas in other relations these indexes are variables. The distinction is essential in our definition of constraint satisfaction problems. (3) Constraint satisfaction problems are formulated in terms of semantics of conjunctions of atomic formulas of predicate logic. (4) Approximation structures, which are available for several important domains, are applied to solutions of constraint satisfaction problems. As application we treat constraint satisfaction problems over reals. These cover a large part of numerical analysis, most significantly nonlinear equations and inequalities. The chaotic algorithm analyzed in the paper combines the efficiency of floating-point computation with the correctness guarantees of arising from our logico-mathematical model of constraint-satisfaction problems.

cs.AI↗

arXiv2012

Discovering Algorithms with Matrix Code

In first-year programming courses it is often difficult to show students how an algorithm can be discovered. In this paper we present a program format that supports the development from specification to code in small and obvious steps; that is, a discovery process. The format, called Matrix Code, can be interpreted as a proof according to the Floyd-Hoare program verification method. The process consists of expressing the specification of a function body as an initial code matrix and then growing the matrix by adding rows and columns until the completed matrix is translated in a routine fashion to compilable code. As worked example we develop a Java program that generates the table of the first N prime numbers.

cs.PL↗

arXiv2012

Relational Semantics for Databases and Predicate Calculus

The relational data model requires a theory of relations in which tuples are not only many-sorted, but can also have indexes that are not necessarily numerical. In this paper we develop such a theory and define operations on relations that are adequate for database use. The operations are similar to those of Codd's relational algebra, but differ in being based on a mathematically adequate theory of relations. The semantics of predicate calculus, being oriented toward the concept of satisfiability, is not suitable for relational databases. We develop an alternative semantics that assigns relations as meaning to formulas with free variables. This semantics makes the classical predicate calculus suitable as a query language for relational databases.

cs.DB↗

arXiv2010

Integrating Interval Constraints into Logic Programming

The CLP scheme uses Horn clauses and SLD resolution to generate multiple constraint satisfaction problems (CSPs). The possible CSPs include rational trees (giving Prolog) and numerical algorithms for solving linear equations and linear programs (giving CLP(R)). In this paper we develop a form of CSP for interval constraints. In this way one obtains a logic semantics for the efficient floating-point hardware that is available on most computers. The need for the method arises because in the practice of scheduling and engineering design it is not enough to solve a single CSP. Ideally one should be able to consider thousands of CSPs and efficiently solve them or show them to be unsolvable. This is what CLP/NCSP, the new subscheme of CLP described in this paper is designed to do.

cs.PL↗

arXiv2009

The Fundamental Theorems of Interval Analysis

Expressions are not functions. Confusing the two concepts or failing to define the function that is computed by an expression weakens the rigour of interval arithmetic. We give such a definition and continue with the required re-statements and proofs of the fundamental theorems of interval arithmetic and interval analysis. Revision Feb. 10, 2009: added reference to and acknowledgement of P. Taylor.

math.NA↗

arXiv2008

Interval Semantics for Standard Floating-Point Arithmetic

If the non-zero finite floating-point numbers are interpreted as point intervals, then the effect of rounding can be interpreted as computing one of the bounds of the result according to interval arithmetic. We give an interval interpretation for the signed zeros and infinities, so that the undefined operations 0*inf, inf - inf, inf/inf, and 0/0 become defined. In this way no operation remains that gives rise to an error condition. Mathematically questionable features of the floating-point standard become well-defined sets of reals. Interval semantics provides a basis for the verification of numerical algorithms. We derive the results of the newly defined operations and consider the implications for hardware implementation.

math.NA↗

arXiv2007

Functions to Support Input and Output of Intervals

Interval arithmetic is hardly feasible without directed rounding as provided, for example, by the IEEE floating-point standard. Equally essential for interval methods is directed rounding for conversion between the external decimal and internal binary numerals. This is not provided by the standard I/O libraries. Conversion algorithms exist that guarantee identity upon conversion followed by its inverse. Although it may be possible to adapt these algorithms for use in decimal interval I/O, we argue that outward rounding in radix conversion is computationally a simpler problem than guaranteeing identity. Hence it is preferable to develop decimal interval I/O ab initio, which is what we do in this paper.

math.NA↗

arXiv2006

Object-Oriented Modeling of Programming Paradigms

For the right application, the use of programming paradigms such as functional or logic programming can enormously increase productivity in software development. But these powerful paradigms are tied to exotic programming languages, while the management of software development dictates standardization on a single language. This dilemma can be resolved by using object-oriented programming in a new way. It is conventional to analyze an application by object-oriented modeling. In the new approach, the analysis identifies the paradigm that is ideal for the application; development starts with object-oriented modeling of the paradigm. In this paper we illustrate the new approach by giving examples of object-oriented modeling of dataflow and constraint programming. These examples suggest that it is no longer necessary to embody a programming paradigm in a language dedicated to it.

cs.SE↗

arXiv2006

Set-Theoretic Preliminaries for Computer Scientists

The basics of set theory are usually copied, directly or indirectly, by computer scientists from introductions to mathematical texts. Often mathematicians are content with special cases when the general case is of no mathematical interest. But sometimes what is of no mathematical interest is of great practical interest in computer science. For example, non-binary relations in mathematics tend to have numerical indexes and tend to be unsorted. In the theory and practice of relational databases both these simplifications are unwarranted. In response to this situation we present here an alternative to the ``set-theoretic preliminaries'' usually found in computer science texts. This paper separates binary relations from the kind of relations that are needed in relational databases. Its treatment of functions supports both computer science in general and the kind of relations needed in databases. As a sample application this paper shows how the mathematical theory of relations naturally leads to the relational data model and how the operations on relations are by themselves already a powerful vehicle for queries.

cs.DM↗

arXiv2006

Computational Euclid

We analyse the axioms of Euclidean geometry according to standard object-oriented software development methodology. We find a perfect match: the main undefined concepts of the axioms translate to object classes. The result is a suite of C++ classes that efficiently supports the construction of complex geometric configurations. Although all computations are performed in floating-point arithmetic, they correctly implement as semi-decision algorithms the tests for equality of points, a point being on a line or in a plane, a line being in a plane, parallelness of lines, of a line and a plane, and of planes. That is, in accordance to the fundamental limitations to computability requiring that only negative outcomes are given with certainty, while positive outcomes only imply possibility of these conditions being true.

cs.CG↗