Developing logic programs from specifications using stepwise refinement

In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.

Mathematical methods for spatially cohesive reserve design

The problem of designing spatially cohesive nature reserve systems that meet biodiversity objectives is formulated as a nonlinear integer programming problem. The multiobjective function minimises a combination of boundary length, area and failed representation of the biological attributes we are trying to conserve. The task is to reserve a subset of sites that best meet this objective. We use data on the distribution of habitats in the Northern Territory, Australia, to show how simulated annealing and a greedy heuristic algorithm can be used to generate good solutions to such large reserve design problems, and to compare the effectiveness of these methods.

A refinement calculus for logic programs

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.

Empirical evidence for ultrametric structure in multi-layer perceptron error surfaces

Combinatorial optimization problems share an interesting property with spin glass systems in that their state spaces can exhibit ultrametric structure. We use sampling methods to analyse the error surfaces of feedforward multi-layer perceptron neural networks learning encoder problems. The third order statistics of these points of attraction are examined and found to be arranged in a highly ultrametric way. This is a unique result for a finite, continuous parameter space. The implications of this result are discussed.

Nondeterministic gates for photonic single-rail quantum logic

We discuss techniques for producing, manipulating, and measuring qubits encoded optically as vacuum- and single-photon states. We show that a universal set of nondeterministic gates can be constructed using linear optics and photon counting. We investigate the efficacy of a test gate given realistic detector efficiencies.