Computational Aspects of Lattice Theory
Abstract
The use of computers to produce a user-friendly safe environment is an important area of research in computer science. This dissertation investigates how computers can be used to create an interactive environment for lattice theory. The dissertation is divided into three parts. Chapters two and three discuss mathematical aspects of lattice theory, chapter four describes methods of representing and displaying distributive lattices and chapters five, six and seven describe a definitive based environment for lattice theory.
Chapter two investigates lattice congruences and pre-orders and demonstrates that any lattice congruence or pre-order can be determined by sets of join-irreducibles. By this correspondence it is shown that lattice operations in a quotient lattice can be calculated by set operations on the join-irreducibles that determine the congruence. This alternative characterisation is used in chapter three to obtain closed forms for all replacements of the form "h can replace g when computing an element f ", and hence extend the results of Beynon and Dunne into general lattices. Chapter four investigates methods of representing and displaying distributive lattices. Techniques for generating Hasse diagrams of distributive lattices are discussed and two methods for performing calculations on free distributive lattices and their respective advantages are given. Chapters five and six compare procedural and functional based notations with computer environments based on definitive notations for creating an interactive environment for studying set theory. Chapter seven introduces a definitive based language called Pecan for creating an interactive environment for lattice theory. The results of chapters two and three are applied so that quotients, congruences and homomorphic images of lattices can be calculated efficiently.