Mechanical Analysis of Finite Idempotent Relations

Article type: Research Article

Authors: Kammüller, Florian

Affiliations: Institut für Softwaretechnik und Theoretische Informatik, Technische Universität Berlin, and Middlesex University, The Borroughs, NW4 4BT, London UK. flokam@cs.tu-berlin.de

Note: [] Research for this paper has been partly performed in collaboration with J.W. Sanders, University of Oxford and has been supported by grant ARC D/03/20258 of the German Academic Exchange Service (DAAD). Address for correspondence: Middlesex University, The Borroughs, NW4 4BT, London UK

Abstract: We use the technique of interactive theorem proving to develop the theory and an enumeration technique for finite idempotent relations. Starting from a short mathematical characterization of finite idempotents defined and proved in Isabelle/HOL, we derive first an iterative procedure to generate all instances of idempotents over a finite set. From there, we develop a more precise theoretical characterization giving rise to an efficient predicate that can be executed in the programming language ML. Idempotent relations represent a very basic, general mathematical concept but the steps taken to develop their theory with the help of Isabelle/HOL are representative for developing algorithms from a mathematical specification.

Keywords: Formal Specification of Computer Systems, Idempotent Relations, Interactive Theorem Proving, Higher Order Logic

DOI: 10.3233/FI-2011-392

Journal: Fundamenta Informaticae, vol. 107, no. 1, pp. 43-65, 2011