We introduce the general notions of an index and a core of a relation. We postulate a limited form of the axiom of choice -- specifically that all partial equivalence relations have an index -- and explore the consequences of adding the axiom to standard axiom systems for point-free reasoning. Examples of the theorems we prove are that a core/index of a difunction is a bijection, and that the so-called ``all or nothing'' axiom used to facilitate pointwise reasoning is derivable from our axiom of choice. Fundamenta Informaticae, Volume 195, Issue 1-4, Article 2, 2025

Abstract An equivalence relation can be constructed from a given (homogeneous, binary) relation in two steps: first, construct the smallest reflexive and transitive relation containing the given relation (the “star” of the relation) and, second, construct the largest symmetric relation that is included in the result of the first step. The fact that the final result is also reflexive and transitive (as well as symmetric), and thus an equivalence relation, is not immediately obvious, although straightforward to prove. Rather than prove that the defining properties of reflexivity and transitivity are satisfied, we establish reflexivity and transitivity constructively by exhibiting a starth root—in a way that emphasises the creative process in its construction. The resulting construction is fundamental to algorithms that determine the strongly connected components of a graph as well as the decomposition of a graph into its strongly connected components together with an acyclic graph connecting such components.

The notion of a difunction was introduced by Jacques Riguet in 1948. Since then it has played a prominent role in database theory, type theory, program specification and process theory. The theory of difunctions is, however, less known in computing than it perhaps should be. The main purpose of the current paper is to give an account of difunction theory in relation algebra, with the aim of making the topic more mainstream. As is common with many important concepts, there are several different but equivalent characterisations of difunctionality, each with its own strength and practical significance. This paper compares different proofs of the equivalence of the characterisations. A well-known property is that a difunction is a set of completely disjoint rectangles. This property suggests the introduction of the (general) notion of the “core” of a relation; we use this notion to give a novel and, we believe, illuminating characterisation of difunctionality as a bijection between the classes of certain partial equivalence relations.

Central to algorithmic graph theory are the concepts of acyclicity and strongly connected components of a graph, and the related search algorithms. This article is about combining mathematical precision and concision in the presentation of these concepts. Concise formulations are given for, for example, the reflexive-transitive reduction of an acyclic graph, reachability properties of acyclic graphs and their relation to the fundamental concept of “definiteness”, and the decomposition of paths in a graph via the identification of its strongly connected components and a pathwise homomorphic acyclic subgraph. The relevant properties are established by precise algebraic calculation. The combination of concision and precision is achieved by the use of point-free relation algebra capturing the algebraic properties of paths in graphs, as opposed to the use of pointwise reasoning about paths between nodes in graphs.

One-person solitaire-like games are explored with a view to using them in teaching algorithmic problem solving. The key to understanding solutions to such games is the identification of invariant properties of polynomial arithmetic. We demonstrate this via three case studies: solitaire itself, tiling problems and a novel class of one-person games. The known classification of states of the game of (peg) solitaire into 16 equivalence classes is used to introduce the relevance of polynomial arithmetic. Then we give a novel algebraic formulation of the solution to a class of tiling problems. Finally, we introduce an infinite class of challenging one-person games, which we call “replacement-set games”, inspired by earlier work by Chen and Backhouse on the relation between cyclotomic polynomials and generalisations of the seven-trees-in-one type isomorphism. We present an algorithm to solve arbitrary instances of replacement-set games and we show various ways of constructing infinite (solvable) classes of replacement-set games.

This paper tackles the problem of constructing a compact, point-free proof of the associativity of demonic composition of binary relations and its distributivity through demonic choice. In order to achieve this goal, a definition of demonic composition is proposed in which angelic composition is restricted by means of a so-called ‘monotype factor’. Monotype factors are characterised by a Galois connection similar to the Galois connection between composition and factorisation of binary relations. The identification of such a connection is argued to be highly conducive to the desired compactness of calculation.

Abstract This paper provides a tutorial introduction to a constructive theory of types based on, but incorporating some extensions to, that originally developed by Per Martin-Löf. The emphasis is on the relevance of the theory to the construction of computer programs and, in particular, on the formal relationship between program and data structure. Topics discussed include the principle of propositions as types, free types, congruence types, types with information loss and mutually recursive types. Several examples of program development within the theory are also discussed in detail.

The use of invariant properties and bound functions is a sound and well-documented methodology for this design of loop structures. We show how to formulate the methodology as a proposition in the intuitionistic theory of types developed by Per Martin-Löf. By proving the validity of this proposition we effectively obtain a method of writing while-statements in Type Theory. Two simple and well-known examples are given to illustrate the method.

Locally least-cost error recovery is a technique for recovering from syntax errors by editing the input string at the point of error detection.A scheme for its implementation in recursive descent parsers, which in principle embodies a process of passing a parameter to each procedure in the parser for each terminal symbol in the grammar, has been suggested.For this scheme to be practical it is vital that as much parameterization as possible is eliminated from the recursive descent parser.This oPtimization problem and how it may be split into three separate global data flow analysis problems-classifying terminal symbols and the so-called min and max follow cost problems--are discussed.The max follow cost problem is a particularly difficult one to solve.The application of Gaussian elimination to its solution is shown by expressing it as a continuous data flow problem, and it is also related to an "idiosyncratic" data flow problem arising in the optimization of very high level languages.Classifying terminal symbols is also difficult since the problem is unsolvable in general.However, for the class of LL(1) grammars, the problem is shown to be expressible as a distributive data flow problem and so may be solved using, say, Gauss-Seidel iteration.

Locally least-cost error recovery is a technique for recovering from syntax errors by editing the input string at the point of error detection. An informal description of a parser generator which implements the technique is given. The generator takes as input an extended BNF description of a language together with a set of primitive edit costs and outputs a recursive descent syntax analyser including error recovery. Criteria for assessment of the technique are offered. Using these criteria the technique is assessed with respect to a database of over 100 example programs, and compared with an alternative local error recovery technique, that of follow set error recovery. The conclusion is that locally least-cost error recovery is more effective than follow set error recovery but much less economical in its use of storage space. The least-cost parser also runs between 15 and 20% slower than the follow set parser.

~While-least-cost~ error correction is fundamentally important to context-free language processing, it is inefficient w'Qhemdone globally.A locally least-cost repair method has been devised to model error recovery in conventional-~o-mpile]ts.The principles of this recovery technique have inspired a practical LL(1) method and should be of value m ~ntmg-error~rJel~a~lr m other parsing algorithms.-At each point in the syntax analysis, a locally optimal repair of't~e-next-sy-mBffl is defined to be a string w such that w can be parsed without error and such that editing the symbol following w can be achieved at least cost, costs being defined by the Wagner-Fischer model of string-to-string correction.In this paper we describe how error recovery can be achieved in Earley's algorithm by simulating locally optimal repairs.The main result is to show that the complexity of Earley's algorithm is not affected by this process; that is, for any input string of length n, the work involved is O(n) if the given grammar is deterministic, O(n 2) if the grammar is unambiguous, and O(n 3) in the worst case.Key Words and Phrases: error repair,