South African Computer Journal 1993(9)
Permanent URI for this collection
Browse
Recent Submissions
Item Introduction to computability theory(South African Computer Society (SAICSIT), 1993) Zucker, J; Pretorius, LThese are notes for a short introductory course on Computability Theory (or recursive function theory). The basic notion of computability is defined in terms of a simple imperative programming language.Item A working relational model: The derivation of the Dijkstra-Scholten predicate transformer semantics from Tarski's axioms for the Peirce-Schroder calculus of relations(South African Computer Society (SAICSIT), 1993) Maddux, RDThe definitions for Dijkstra's predicate transformer semantics can be justified by considering the meaning of a program as a binary relation on states (which holds between two states if there is a terminating computation connecting them) together with a set of states (those which initiate eternal computations). In fact, all of the definitions can be proved as theorems, using Tarski's ten equational postulates for the calculus of relations. These postulates define relation algebras, so we take the meaning of a program to be a pair of elements of a complete relation algebra, one corresponding to the binary relation determined by the terminating computations, the other corresponding to the set of states initiating eternal computations. The predicate transformers for a program are defined from these two elements. In this abstract setting we derive all the significant definitions and theorems of Dijkstra and Scholten's "Predicate Calculus and Program Semantics''.Item Denotational semantics and domain theory(South African Computer Society (SAICSIT), 1993) Goslett, J.; Hulley, H; Melton, AThis tutorial is an introduction to denotational semantics and domain theory. For this reason the presentation is not entirely rigorous, with some proofs being omitted and certain simplifying assumptions being made. Instead, the emphasis here has been on satisfying the computational intuition of the reader - dwelling too long on the mathematical aspects of semantic domains is not always satisfying to somebody attempting to ascertain why these structures are relevant to computer science in the first place. Thus, we have started right at the beginning by discussing the concepts of syntax and semantics, and we have attempted to build the mathematical theory of domains upon this computational foundation in a fluid, intuitive and informal manner. In Section 1 and Section 2 we begin with brief descriptions of the syntax and semantics of computer languages, the roles these notions play in computer science, and how they interact in the quest for a formal methodology for computer programming. Section 3 provides an introduction to denotational semantics in particular - this being illustrated by a very simple example. In Section 4 we get down to the business of defining a language which can be recognised as something approximating a real computer language. Here we also endow this language (which can be found in [8]) with a denotational description. We have attempted to explain why the semantics presented for our toy language should seem natural to the reader. In Sections 5-7 we begin to explore the mathematical complexities of domain theory. Our motivation for introducing all this new theory is the search for a denotational description of the 'while'-loop in our example programming language. We conclude in Section 8 with a discussion of parallelism, non-determinism, and the new demands which these complications make of the theory developed up to then. For more advanced presentations of denotational semantics and domain theory, we recommend [3, 4, 6, 7, 10].Item Deduction systems based on resolution(South African Computer Society (SAICSIT), 1993) Eisinger, N; Ohlbach, HJA general theory of deduction systems is presented The theory is illustrated with deduction systems based on the resolution calculus, in particular with clause graphs. This theory distinguishes four constituents of a deduction system: • the logic, which establishes a notion of semantic entailment; • the calculus, whose rules of inference provide the syntactic counterpart of entailment; • the logical state transition system, which determines the representation of formulae or sets of formulae together with their interrelationships, and also may allow additional operations reducing the search space; • the control, which comprises the criteria used to choose the most promising from among all applicable inference steps. Much of the standard material on resolution is presented in this framework. For the last two levels many alternatives are discussed. Appropriately adjusted notions of soundness, completeness, confluence, and Noetherianness are introduced in order to characterize the properties of particular deduction systems. For more complex deduction systems, where logical and topological phenomena interleave, such properties can be far from obvious.