On Proving Laws of the Algebra of FP-Systems in Edinburgh LCF

Jacek Leszczylowski

J.Backus, in CACM 21/8, defined a class of applicative programming systems called FP /functional programming/ systems in which a user has: 1.objects built recursively from atoms, UU /an undefined element/ and objects by a strict /i.e. a UU-preserving/ "list" operator, 2. elementary functions over objects, 3. tools for building functions out of already defined functions. One can think of a machine support while working with FP systems and proving facts about FP systems as well as facts concerning the functions being defined. The choice of EDINBURGH LCF is rather natural because it is an interactive ccmputer system /implemented in LISP/ for reasoning about functions /see [6]/. It consists of two parts. The first part is a family of calculi each of which is characterized by four factors: 1. type operators /representing domains in the sense of Scott’s theory; see [11]/, 2. constants /representing continuous functions/, 3. axioms, 4. inference rules. One of them, PPLAMBDA, is given as the "initial" calculus, and other calculi may be built by users as extensions of existing calculi. The second part is a high level programming language ML which is fully higher order and is strongly typed. Its polymorphic types make it as convenient as typeless languages. This paper is a short report on the application of EDINBURGH LCF to proving the laws of the algebra of FP systems listed by Backus in [1]. Actualiy, we generalized FP-systems and the laws are formulated in stronger form than it was done by Backus. We briefly describe /sec.II/ the style of proving with the system, then /sec.III/ comment the strategies used in the proofs giving only their specifications. The summing up remarks will be given in sec.IV. More detailed report on the project is given in [9].


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.