perm filename THEORY[206,LSP] blob sn#242203 filedate 1976-10-16 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00003 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 .require"lispub.pub[206,LSP]"source C00005 00003 .ss Structural Induction C00006 ENDMK C⊗; .require"lispub.pub[206,LSP]"source .SECTION←4 .PAGE←74 .SEC PROVING LISP PROGRAMS CORRECT In this chapter we will introduce techniques for proving LISP programs correct. In general, they will be limited to clean LISP programs. The necessary basic facts can be divided into four categories: algebraic facts about lists and S-expressions, general facts about composition, facts about first order logic including conditional expressions, facts about the inductive structure of lists and S-expressions, and general facts about functions defined by recursion. Ideally, we would use a general theory of recursive definition to prove theorems about LISP functions. However, the general theory is not well enough developed, so we have had to introduce some methods limited to LISP functions defined by particular kinds of recursion schemes. .ss Algebraic facts about S-expressions and lists. The algebraic facts about S-expressions are expressed by the following sentences of first order logic: %3∀x.(issexp x ⊃ %4at%3 x ∨ (issexp %4a%3 x ∧ issexp %4d%3 x ∧ x = (%4a%3 x . %4d%3 x)))%1 and %3∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬%4at%3(x.y) ∧ x = %4a%3(x.y) ∧ y = %4d%3(x.y))%1. These axioms treat S-expressions among other objects. If we can assume that all objects are S-expressions or can declare certain variables as ranging only over S-expressions, we can simplify the axioms to %3∀x.[%4at%3 x ∨ x = [%4a%3 x . %4d%3 x]]%1 and %3∀x y.[¬%4at%3[x.y] ∧ x = %4a%3[x.y] ∧ y = %4d%3[x.y]]%1. The algebraic facts about lists are expressed by the following sentences of first order logic: %3∀x. islist x ⊃ x = %5NIL%3 ∨ islist %4d %3x%1, %3∀x y. islist y ⊃ islist[x . y]%1, %3∀x y. islist y ⊃ %4a%3[x . y] = x ∧ %4d%3[x.y] = y%1, .ss Structural Induction