perm filename FOLISP[206,LSP] blob sn#372861 filedate 1978-08-05 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00015 PAGES C REC PAGE DESCRIPTION C00001 00001 C00003 00002 .if false then begin "revision outline" C00006 00003 .s(FOLISP,PROVING LISP PROGRAMS CORRECT) C00011 00004 .ss Introductory Example. C00018 00005 .ss First Order Logic with Conditional Forms and Lambda-expressions. C00036 00006 .ss Conditional Expressions. C00041 00007 .ss Lambda-expressions. C00044 00008 .ss First Order Axioms for LISP. C00050 00009 .ss Axiom Schemas of Induction. C00054 00010 .ss A Simple Example. C00062 00011 .ss Pseudo-logic. C00072 00012 .ss An Extended Example. C00093 00013 .ss Functionals and Least Fixedpoints. C00106 00014 .ss The Minimization Schema. C00114 00015 .cb Exercises. C00121 ENDMK C⊗; .if false then begin "revision outline" intro: motivation, automatic proving and checking, why develop f-o-theory informal example: properties of append by list induction (theory.new) compare to numinduction? informal discussion of what it means to formalize such an argument mention notions of language, semantics (intended model), formal notion of proof, theory, notion of fn defined by rec defn, exists unique least defined partial fn on domain that satisfies fnl eqn "totality", "bottom" formalization: language semantics rules for manipulating sentences mentions some standard dedn rules rules for cond rules for λ axioms for theory of LISP (include cvi (istail and issexp) from the beginning mention not all independent, but are useful for making more natural proofs really recursive functions definitions that are "total" on form add to axioms fnl eqn and fact that ⊗islist() or ⊗issexp() or ⊗isnatnum mention reasonable list of forms and do formal example :length(fringe(x))=size(x) proving that a rec defn is really recursive eg that result is in desired domain another example :flatten=fringe? recursively defined predicates lose(x)←lose(x) representing fn arriving at desired equiv when rf is "total" (eg has only T and NIL as values) occur example istail upto commontail relations? substantial example samefringe correctness of partions of a list into n pieces. show each part is a part show every part occurs balancing algorithm how to handle definitions of partial fns motivation, example of kinds of interesting problems min schema example of use add selection of exercises to prove facts about the programs written as solutions to the exercises in Ch 2. fix unification problem to be programming and proving problem .end "revision outline" .s(FOLISP,PROVING LISP PROGRAMS CORRECT) .if NOTASSEMBLING then start .IMPURE: NEXT SECTION!; .SEARCH: NEXT SECTION!; .EXTEND: NEXT SECTION!; .ABSNTX: NEXT SECTION!; .COMPIL: NEXT SECTION!; .COMPUT: NEXT SECTION!; .FOL←"A" .end The theory of computation may be divided into two parts. The first is the general theory of computability including topics like universal functions, the existence of uncomputable functions, lambda calculus, call-by-name and call-by-value, and the relation of conditional expression recursion to other formalisms for describing computable functions. The second part, which we will discuss in this chapter emphasizes techniques for proving particular facts about particular computable functions. We emphasize the use of the techniques more than their mathematical background. Much of the material in this chapter is based on [Cartwright 1977] and the rest on [McCarthy 1977]. We begin with proving ⊗extensional ⊗properties of ⊗clean, ⊗pure LISP programs. An ⊗extensional ⊗property is one that depends only on the function computed by the program. Thus it includes the fact that two sort programs compute the same function or that ⊗append is associative but does not include the fact that one sort program does ⊗⊗n%52%*⊗ comparisons and another ⊗⊗n_log_n⊗ comparisons. ⊗Clean LISP programs have no side effects (our methods require the freedom to replace a subexpression by an equal expression), and equality refers to the S-expressions and not to the list structures. ⊗Pure LISP involves only recursive function definitions and doesn't use assignment statements. It wouldn't be difficult to give corresponding methods that would be valid for non-functional programs, because this topic is well developed. In spite of all these limitations, the techniques are useful and point the way to further progress. The main idea is to represent the programs formally using first order logic. Higher order functionals and predicates are used informally. Formal proofs of properties of programs can easily be checked using an automatic proof checker such as FOL [Weyhrauch 1977]. Examples are given in Appendix {SECTION FOL}. We begin with an informal sample proof, commenting about the information and concepts needed to make the proof work. We then proceed to formalize these ideas. The necessary basic facts can be divided into several categories: first order logic including conditional forms and first order lambda-expressions, algebraic facts about lists and S-expressions, facts about the inductive structure of lists and S-expressions, and general facts about functions defined by recursion. .ss Introductory Example. Consider the function ⊗append ( * ) defined by ⊗⊗⊗u * v ← if qn u qthen v qelse qa u . [qd u * v]⊗ and the predicate ⊗member ( ε ) defined by ⊗⊗⊗x ε u ← ¬qn u ∧ [x = qa u ∨ x ε qd u] ⊗ where ⊗x is any S-expression and ⊗u and ⊗v are lists (whose elements are S-expresssions). (Note that our precedence conventions imply that ⊗⊗qd u_*_v_=_[qd u]_*_v⊗.) It is probably intuitively clear that if ⊗x is a member of one of the lists ⊗u or ⊗v then ⊗x is a member of the list ⊗⊗u_*_v⊗. We will give an informal proof of this property. The proof will be based on the principle of ⊗list_induction which is analogous to natural induction (for functions on the natural numbers). This principle states that if some property, qP(qNIL), holds for the list qNIL and if, by assuming qP(⊗⊗u⊗) holds for ⊗⊗qd u⊗, we can prove that it holds for the list ⊗u then qP(⊗⊗u⊗) holds for all lists ⊗u. In our case qP(⊗⊗u⊗) is the property: ⊗⊗⊗[x ε u ∨ x ε v] ⊃ x ε [u * v] . ⊗ The induction will be with respect to the list ⊗u, eg. the first argument to ⊗append. The variables ⊗x and ⊗v are just carried along. The proof consists of two parts. First we assume qn ⊗u. Then by the definition of ⊗member, ⊗⊗x_ε_u⊗ is false and by the definition of ⊗append, ⊗⊗u_*_v_=_v⊗. Thus qP(⊗⊗u⊗) becomes ⊗⊗⊗x ε v ⊃ x ε v ⊗ which is true. Next we assume ¬qn ⊗u and that ⊗⊗qP(qd u)⊗ is true. Thus ⊗⊗⊗[x ε qd u ∨ x ε v] ⊃ x ε [qd u * v]⊗ By definition of ⊗append, ⊗⊗u_*_v⊗ reduces to ⊗⊗qa u . [qd u * v]⊗. Thus ⊗⊗u_*_v_≠_qNIL⊗, ⊗⊗qa [u_*_v]_=_qa u⊗ and ⊗⊗qd [u_*_v]_=_qd u_*_v⊗. By definition of ⊗member, ⊗⊗x_ε_u⊗ reduces to ⊗⊗x_=_qa u_∨_x_ε_qd u⊗. So we consider two cases: ⊗⊗x_=_qa u⊗ and ⊗⊗x_ε_qd u_∨_x_ε_v⊗. In the first case we have ⊗⊗x_=_qa [u_*_v]⊗ and so, by definition of ⊗member, ⊗⊗x_ε_[u_*_v]⊗ and qP(⊗⊗u⊗) is true. In the second case we have by the induction hypothesis that ⊗⊗x_ε_[qd u_*_v]⊗ and again, by definition of ⊗member, qP(⊗⊗u⊗) holds. Thus we have done the required proofs and by list induction the property qP(⊗⊗u⊗) holds for any list ⊗u. .if lines < 7 then next page In carrying out the proof we have used properties of lists such as .NOFILL ⊗⊗[x . u]⊗ is a list ⊗⊗qa [x . u] = x]⊗ ⊗⊗qd [x . u] = u]⊗ ⊗⊗¬qn [x . u]⊗ .FILL for any S-expression ⊗x and any list ⊗u. We have also used these properties with ⊗u replaced by ⊗⊗u_*_v⊗ or ⊗⊗qd u_*_v⊗. To do this we need to know that ⊗⊗u_*_v⊗ is a list or that ⊗⊗qd u_*_v⊗ is a list. This is essentially the same as saying that the computation defined by ⊗append terminates in a finite number of steps or that ⊗append is a total function. Saying that ⊗⊗u * v⊗ reduces to ⊗⊗qa u . [qd u * v]⊗ is based on the rule for computing recursively defined functions. It too, is only meaningful when ⊗⊗qd u_*_v⊗ is a list, eg. when ⊗append is total. Note that in using the recursive function definition and the rule for comptation we are essentially substituting equals for equals in the problem. The two cases can be combined giving the ⊗functional_equation for ⊗append ⊗⊗⊗u * v = qif qn u qthen v qelse qa u . [qd u * v].⊗ Again, being able to use the functional equation here depends on knowing ⊗append is total. Similiarly several of the statements made about ⊗member depend on the fact that it is total. Thus to complete the proof it is necessary to know that ⊗append and ⊗member are total. This should be intuitively clear, since the recursive calls in the definitions depend on the ⊗cdr of the test variable and, since our lists are finite, this will eventually be qNIL and the computation will terminate. We will see later how to state and prove such facts. The validity of the list induction principle is due to the fact that we require our lists to be finite. This just is one of many forms of induction. We will see examples of other forms as well as other applications of list induction. Looking at induction in another way, if one starts with a set of properties that must be satisfied by a domain and some basic functions on that domain, then requiring that some induction principle be valid is a way of giving further information about the domain. .ss First Order Logic with Conditional Forms and Lambda-expressions. The logic we shall use is a sorted first order logic with equality, extended by admitting conditional forms as terms and first order lambda-expressions as function symbols. These extensions do not change the logical strength of the theory, because, as we shall see, every formula that includes conditional forms or first order lambdas can be transformed into an equivalent formula without them. However, the extensions are practically important, because they permit us to use recursive definitions directly as formulas of the logic. The adjective sorted refers to the fact that we may restrict a variable to range over some type of object (a sort) rather than over all objects. We can then restrict the domain of a function to some fixed sort. This means that in proving properties of that function attention can be focused on the domain of interest without worrying about what happens for arguments for which the function is not intended to be defined. For example, we shall often use the variables ⊗u and ⊗v to denote lists, and the sorting will permit us to write statements that are true for lists but not for general S-expressions without putting the fact that their validity is restricted to lists into the statement itself. The language for our logic contains terms, formulas, function expressions and predicate expressions which are built from constants, variables, predicate symbols, and function symbols using function application, conditional terms, boolean terms, lambda expressions, and quantifiers. %3Constants%1: We will use S-expresssions as constants standing for themselves and also lower case letters from the first part of the alphabet to represent constants in other domains than S-expressions. In particular we will have the atom qNIL. Other atoms will be introduced as needed. Among the non-S-expression constants we will have qw (read "bottom"). %3Variables%1: We will use the letters ⊗XX through ⊗ZZ as general variables. The variables ⊗u through ⊗w will range over lists, while ⊗x through ⊗z will range over S-expressions and ⊗X through ⊗Z range over extended S-expressions (the set consisting of S-expressions togther with the constant qw). ⊗k through ⊗n are integer variables. Variables ranging over other sorts will be introduced later, when it is meaningful. The variables may appear with or without subscripts. %3Function symbols%1: As function constant symbols we will use the LISP function names qqa, qqd and . (as an infix). Other function symbols including function parameter symbols will be introduced as needed. We suppose that each function symbol takes the same definite number of arguments every time it is used. Thus if the same letter is used with differing numbers of arguments, it stands for different function symbols. Thus we can use ⊗⊗<x%41%*, ... ,x%4n%*>⊗ to represent the list forming functions, but we shall have to axiomatize it separately for each length we actually use. We will often use one argument functions symbols as prefixes, i.e. without brackets, just as qqa and qqd have been used up to now. %3Predicate symbols%1: As predicate constant symbols we will use the logical equality symbol =, and the LISP predicate names qqat, qqn and qeq. We will use qP as a predicate parameter symbol. Certain unary predicate symbols will be designated as sorts. In particular ⊗isesexp, ⊗issexp and ⊗islist are sorts. Other predicate symbols and sorts will be introduced when needed. We suppose that each predicate symbol takes the same definite number of arguments each time it is used. Again a letter may be used with differing numbers of arguments to represent different predicates. Infix and prefix notation will also be used where this is customary. Next we define terms, formulas, function expressions and predicate expressions inductively. A term is an expression whose value will be an object like an S-expression or a number while a formula has value qtrue or qfalse. We will use the symbols T and F for the formulas always having the values qtrue and qfalse respectively. Terms are used in making formulas, and formulas occur in terms so that the definitions are ⊗mutually ⊗recursive where this use of the word ⊗recursive should be distinguished from its use in recursive definitions of functions. Function and predicate expressions are also involved in the mutual recursion. %3Terms%1: Constants are terms, and variables are terms. If ⊗f is a function expression taking ⊗n arguments, and ⊗⊗t%41%*,_..._,t%4n%*⊗ are terms, then ⊗⊗f[t%41%*,_..._,t%4n%*]⊗ is a term. If ⊗s is a formula and ⊗⊗t%41%*⊗ and ⊗⊗t%42%*⊗ are terms, then ⊗⊗qif_s_qthen_t%41%*_qelse_t%42%*⊗ is a term. We soften the notation by allowing infix symbols where this is customary. %3Formulas%1: T and F are formulas. If ⊗⊗t%41%*⊗ and ⊗⊗t%42%*⊗ are terms then ⊗⊗t%41%*_=_t%42%*⊗ is a formula. If qp is a predicate expression taking ⊗n arguments and ⊗⊗t%41%*,_..._,t%4n%*⊗ are terms, then ⊗⊗qp[t%41%*,_..._,t%4n%*]⊗ is a formula. If ⊗s is a formula, then ¬⊗s is also a formula. If ⊗⊗s%41%*⊗ and ⊗⊗s%42%*⊗ are formulas, then ⊗⊗s%41%*⊗_∧_⊗⊗s%42%*⊗, ⊗⊗s%41%*⊗_∨_⊗⊗s%42%*⊗, ⊗⊗s%41%*⊗_⊃_⊗⊗s%42%*⊗, and ⊗⊗s%41%*⊗_≡_⊗⊗s%42%*⊗ are formulas. If ⊗⊗s%40%*⊗, ⊗⊗s%41%*⊗ and ⊗⊗s%42%*⊗ are formulas, then ⊗⊗qif_s%40%*_qthen_s%41%*_qelse_s%42%*⊗ is a formula. If ⊗⊗x%41%*,_...,_x%4n%*⊗ are variables, and ⊗s is a formula, then ⊗⊗[∃x%41%*_..._x%4n%*:_s]⊗ and ⊗⊗[∀x%41%*_..._x%4n%*:_s]⊗ are formulas. %3Function expressions%1: A function symbol is a function expression. If ⊗⊗x%41%*,_..._,x%4n%*⊗ are variables and ⊗t is a term, then ⊗⊗[λx%41%*,_..._,x%4n%*:_t]⊗ is a function expression. %3Predicate expressions%1: A predicate symbol is a predicate expression. If ⊗⊗x%41%*,_..._,x%4n%*⊗ are variables and ⊗s is a formula, then ⊗⊗[λx%41%*,_..._,x%4n%*:_s]⊗ is a predicate expression. An occurrence of a variable ⊗x is called ⊗bound if it is in an expression of one of the forms ⊗⊗[λx%41%*_..._x%4n%*:_t]⊗, ⊗⊗[λx%41%*_..._x%4n%*:_s]⊗, ⊗⊗[∀x%41%*_..._x%4n%*:_s]⊗ or ⊗⊗[∃x%41%*_..._x%4n%*:_s]⊗ where ⊗x is one of the numbered ⊗⊗x⊗'s. If not bound an occurrence is called ⊗free. A formula having no free variables is called a ⊗sentence. The ⊗semantics of first order logic consists of the rules that determine whether a formula is qtrue or qfalse. However, the truth or falsity of a formula is relative to the interpretation assigned to the constants, the function and predicate symbols and the free variables of the formula. We proceed as follows: We begin by choosing a domain. In most cases, the domain will include the S-expressions, and any S-expression constants appearing in the formula stand for themselves. We will allow for the possibility that other objects than S-expressions exist, and some constants may designate them. The special constant symbol qw is used for the value of the function defined by a LISP program in case the computation doesn't terminate; its use requires a justification that will be given later. Each function or predicate constant symbol is assigned a function or predicate on the domain We will normally assign to the basic LISP function and predicate symbols the corresponding basic LISP functions and predicates. A predicate that has been designated as a sort is assigned the characteristic predicate of the subdomain consisting of all the elements of that sort. (The characteristic predicate of a set is the predicate that is qtrue exactly on elements of the set). We require that the subdomain corresponding to a sort be non-empty. Thus ⊗isesexp is assigned to the characteristic predicate of the subdomain of extended S-expressions, ⊗issexp is assigned the characteristic predicate of the subdomain of S-expressions, and ⊗islist is assigned the characteristic predicate for the subdomain of lists. Function and predicate parameter symbols do not get assigned any meaning. Their use is mainly in writing axiom schemata from which an axiom can be obtained by substituting an actual function or predicate expression for the parameter. Each variable appearing free in a formula is assigned an element of the domain. A general variable maybe assigned any element of the domain. A sorted variable is assigned an element from the corresponding subdomain. This collection of assignments constitutes an interpretation, and the truth of a formula is relative to the interpretation. The truth of a formula is determined from the values of its constituents by evaluating successively larger subexpressions. The rules for handling functions and predicates, conditional expressions, equality, and Boolean expressions are exactly the same as those we have used in the previous chapters. We need only explain quantifiers and lambdas. ⊗⊗[∀x%41%*_..._x%4n%*:_s]⊗ is qtrue if and only if ⊗s is qtrue for ⊗all allowed assignments of elements of the domain to the ⊗⊗x⊗'s. An assignment is allowed if the variable is general or if it is sorted and the assignment is to an element of the corresponding subdomain. If ⊗s has free variables that are not among the ⊗⊗x⊗'s, then the truth of the formula depends on the values assigned to these remaining free variables. ⊗⊗[∃x%41%*_..._x%4n%*:_s]⊗ is qtrue if and only if ⊗s is qtrue for ⊗some allowed assignment of elements of the domain to the ⊗⊗x⊗'s. Free variables are handled just as before. ⊗⊗[λx%41%*_..._x%4n%*:_e]⊗ is assigned a function or predicate according to whether ⊗e is a term or a formula. The value of ⊗⊗[λx%41%*_..._x%4n%*:_e][t%41%*,...,t%4n%*]⊗ is obtained by evaluating the ⊗⊗t⊗'s and using these values as values of the ⊗⊗x⊗'s in the evaluation of ⊗e. If ⊗e has free variables in addition to the ⊗⊗x⊗'s, the function or predicate assigned will depend on them too. To see how sorts actually work, we will examine some typical sentences. Assume ⊗x is of sort ⊗issexp and ⊗XX is a general variable. Then the sentence ⊗⊗∀x:_[¬qat x_⊃_x_=_qa x_._qd x]⊗ has the same truth value as ⊗⊗∀XX:_[issexp_XX_⊃_[¬qat XX_⊃_XX_=_qa XX_._qd XX]]⊗ and the sentencc ⊗⊗∃x:_¬qat x⊗ has the same truth value as ⊗⊗∃XX:_[issexp_XX_∧_¬qat XX]⊗. This follows from the rules forming interpretations and evaluating quantified expressions. The formula ⊗⊗∃x:_issexp_x⊗ is guaranteed to be qtrue since we have required that the subdomain corresponding to ⊗issexp (or any sort) is non-empty. Those who are familiar with the lambda calculus should note that λ is being used here in a very limited way. Namely, the variables in a lambda-expression take only elements of the domain as values, whereas the essence of the lambda calculus is that they take arbitrary functions as values. We may call these restricted lambda expressions ⊗first ⊗order ⊗lambdas. .ss Conditional Expressions. All the properties we shall use of conditional forms follow from the relation !eqncond1 ⊗⊗⊗[s ⊃ [qif s qthen a qelse b] = a] ∧ [¬s ⊃ [qif s qthen a qelse b] = b] ⊗. It is worthwhile to list separately some properties of conditional terms. First we have the obvious .begin nofill group ⊗⊗⊗[qif T qthen a qelse b] = a ⊗ !eqncond2 ⊗⊗⊗[qif F qthen a qelse b] = b . ⊗ .end Next we have a ⊗distributive ⊗law for functions applied to conditional terms, namely !eqncond4 ⊗⊗⊗f[qif s qthen a qelse b] = qif s qthen f[a] qelse f[b] ⊗. This applies to predicates as well as functions and can also be used when one of the arguments of a function of several arguments is a conditional term. It also applies when one of the terms of a conditional term is itself a conditional term. Thus .begin nofill group !eqncond5 ⊗⊗⊗qif [qif r qthen s%41%* qelse s%42%*] qthen a qelse b = ⊗ ⊗⊗⊗qif r qthen [qif s%41%* qthen a qelse b] qelse [qif s%42%* qthen a qelse b]⊗ and ⊗⊗⊗qif r qthen [qif s qthen a qelse b] qelse c = ⊗ !eqncond6 ⊗⊗⊗qif s qthen [qif r qthen a qelse c] qelse [qif r qthen b qelse c] . ⊗ .end When the expressions following qthen and qelse are sentences, then the conditional term can be replaced by a sentence according to !eqncond7 ⊗⊗⊗[qif r qthen s%41%* qelse s%42%*] ≡ [r ∧ s%41%*] ∨ [¬r ∧ s%42%*] ⊗. These two rules permit eliminating conditional terms from sentences by first using distributivity to move the conditionals to the outside of any functions and then replacing the conditional term by a Boolean expression. Note that the elimination of conditional terms may increase the size of a sentence, because ⊗r occurs twice in the right hand side of the above equivalence. In the most unfavorable case, ⊗r is dominates the size of the expression so that writing it twice almost doubles the size of the expression. Suppose that ⊗a and ⊗b in ⊗⊗qif_s_qthen_a_qelse_b⊗ are expressions that may contain the sentence ⊗s. Occurrences of ⊗s in ⊗a can be replaced by T, and occurrences of ⊗s in ⊗b can be replaced by F. This follows from the fact that ⊗a is only evaluated if ⊗s is true and ⊗b is evaluated only if ⊗s is false. This leads to a strengthened form of the law of replacement of equals by equals. The ordinary form of the law says that if we have ⊗⊗e_=_e'⊗, then we can replace any occurrence of ⊗e in an expression by an occurrence of ⊗e'. However, if we want to replace ⊗e by ⊗e' within ⊗a within ⊗⊗qif_s_qthen_a_qelse_b⊗, then we need only prove ⊗⊗s_⊃_e_=e'⊗, and to make the replacement within ⊗b we need only prove ⊗⊗¬s_⊃_e_=_e'⊗. More facts about conditional terms are given in [McCarthy 1963] including a discussion of canonical forms that parallels the canonical forms of Boolean terms. Any question of equivalence of conditional terms is decidable by truth tables analogously to the decidability of propositional sentences. .ss Lambda-expressions. The only rule required for handling lambda-expressions in first order logic is called ⊗lambda-conversion. Essentially it is ⊗⊗⊗[λx: e][a] =⊗ < the result of substituting ⊗a for ⊗x in ⊗e >. As examples of this rule, we have ⊗⊗⊗[λx: qa x . y][u . v] = [qa [u . v]] . y . ⊗ However, a complication requires modifying the rule. Namely, we can't substitute for a variable ⊗x an expression ⊗e that has a free variable ⊗y into a context in which ⊗y is bound. Thus it would be wrong to substitute ⊗⊗y_+_z⊗ for ⊗x in ⊗⊗∀y:_[x_+_y_=_z]⊗ or into the term ⊗⊗[λy:_x_+_y][u_+_v]⊗. Before doing the substitution, the variable ⊗y would have to be replaced in all its bound occurrences by a fresh variable. Lambda-expressions can always be eliminated from sentences and terms by lambda-conversion, but the expression may increase greatly in length if a lengthy term replaces a variable that occurs more than once in ⊗e. It is easy to make an expression of length proportional to ⊗n whose length is proportional to 2%5n%* after conversion of its ⊗n nested lambda-expressions. For example ⊗⊗⊗λx%41%*: [x%41%*.x%41%*][ ... [λx%4n%*: [x%4n%*.x%4n%*][$$A$]] ... ]⊗ becomes $$(A . A)$, $$((A . A) . (A . A))$, or $$((((A . A) . (A . A)) . ((A . A) . (A . A))) . ((A . A) . (A . A)) . ((A . A) . (A . A))))$ for ⊗n = 1, 2, or 4 respectively. .ss First Order Axioms for LISP. We are interested in the first order theory of LISP. That is, we are interested in determining what formulas involving variables ranging over lists and S-expressions and function and predicate symbols representing LISP functions and predicates are qtrue. In order to describe this theory we represent the algebraic facts about lists, S-expressions and basic LISP functions and predicates by axioms (sentences of the theory which we assume to be qtrue). The axioms are given names either individually or in small groups. To refer to the second axiom in a group named $AXNAME we write $AXNAME2. .turnon "∂" .bb Sorts and variables. Before stating the axioms we list the sorts and give the variables which range over these sorts. The statement ⊗⊗x_ε_issexp⊗ means that the variable ⊗x ranges over the subdomain with characteristic predicate ⊗issexp. .nofill $SORTS: ⊗isesexp, ⊗issexp, ⊗islist $VARIABLES: $GENERAL: ∂(24)⊗⊗XX, YY, ZZ⊗ $SORTED: ∂(24)⊗⊗X, Y, Z⊗ ε ⊗isesexp ∂(24)⊗⊗x, y, z⊗ ε ⊗issexp ∂(24)⊗⊗u, v, w⊗ ε ⊗islist .fill Note that from these declarations we can show such facts as ⊗⊗∀x:_issexp_x⊗. To see this, we observe that this sentence has the same truth value as ⊗⊗∀X:_issexp_X_⊃_issexp_X⊗ which clearly is qtrue. .bb Domain facts. The first group of axioms give facts about the various sorts(subdomains) and their relations. $ESEXP: ∂(16)⊗⊗∀x: isesexp x⊗ ∂(16)⊗⊗isesexp qw⊗ ∂(16)⊗⊗∀X: issexp X ∨ X = qw⊗ $SEXP: ∂(16)⊗⊗∀u: issexp u⊗ ∂(16)⊗⊗¬issexp qw⊗ ∂(16)⊗⊗∀XX: qat XX ⊃ issexp XX⊗ $NIL: ∂(16)⊗⊗islist qNIL⊗ $NULL: ∂(16)⊗⊗∀u: [qn u ≡ u=qNIL]⊗ ∂(16)⊗⊗∀u: [qn u ≡ qat u]⊗ .bb Function ranges. Next are the axioms describing the ranges of the basic LISP functions. $CONS: ∂(16)⊗⊗∀x y: ¬qat [x . y]⊗ ∂(16)⊗⊗∀x y: issexp [x . y]⊗ ∂(16)⊗⊗∀x u: islist [x . u]⊗ $CAR: ∂(16)⊗⊗∀x: [¬qat x ⊃ issexp qa x]⊗ $CDR: ∂(16)⊗⊗∀x: [¬qat x ⊃ issexp qd x]⊗ ∂(16)⊗⊗∀u: [¬qn u ⊃ islist qd u]⊗ .bb Function relations. Finally we have the axioms describing the relations among the basic LISP functions. $CAR-CONS: ∂(16)⊗⊗∀x y: qa [x . y] = x⊗ $CDR-CONS: ∂(16)⊗⊗∀x y: qd [x . y] = y⊗ $CONSTRUCT: ∂(16)⊗⊗∀x: [¬qat x ⊃ [qa x . qd x] = x]⊗ An alternate form of $CONSTRUCT which we will find useful is $EQ-SEXP: ∂(16)⊗⊗∀x y: [[¬qat x ∧ ¬qat y] ⊃ [qa x = qa y ∧ qd x = qd y ≡ x = y]] ⊗. .turnoff These axioms are analogous to the algebraic part of Peano's axioms for the non-negative integers. The analogy can be made clear if we write Peano's axioms using ⊗n' for the successor of ⊗n and ⊗⊗n⊗%5-%* for the predecessor of ⊗n. Peano's algebraic axioms then become ⊗⊗⊗∀n: n' ≠ 0 , ⊗ ⊗⊗⊗∀n: (n')%5-%* = n , ⊗ and ⊗⊗⊗∀n: n ≠ 0 ⊃ (n%5-%*)' = n . ⊗ Lists can model integers if we identify 0 with qNIL and assume that there is only one object (say qNIL again) that can serve as a list element. Then ⊗⊗n'_=_cons[qNIL,n]⊗, and ⊗⊗n%5-%*_=_qd n⊗. .ss Axiom Schemas of Induction. Clearly S-expressions and lists satisfy the axioms given for them, but unfortunately these algebraic axioms are insufficient to characterize them. For example, consider a domain of one element ⊗a satisfying ⊗⊗⊗qa a = qd a = a . a = a . ⊗ It satisfies the algebraic axioms for S-expressions. We can exclude it by an axiom ⊗⊗∀x: [qa x ≠ x]⊗, but this won't exclude other circular list structures that eventually return to the same element by some qqa-qqd chain. Actually we want to exclude all infinite chains, because most LISP programs won't terminate unless every qqa-qqd chain eventually terminates in an atom. This cannot be done by any finite set of axioms. In order to exclude circular and infinite list structures we need axiom schemas of induction analogous to Peano's for the integers. Peano's induction schema is ordinarily written ⊗⊗⊗P(0) ∧ ∀n: (P(n) ⊃ P(n')) ⊃ ∀n: P(n) .⊗ Here ⊗P(n) is an arbitrary predicate of integers, and we get particular instances of the schema by substituting particular predicates. It is called an axiom schema rather than an axiom, because we consider the schema, which is not properly a sentence of first order logic, as standing for the infinite collection of axioms that arise from it by substituting all possible predicates for ⊗P. The S-expression induction schema is $SEXPINDUCTION: ⊗⊗∀x: [qat x ⊃ qP x] ∧ ∀x: [¬qat x ∧ qP qa x ∧ qP qd x ⊃ qP x] ⊃ ∀x: qP x ⊗. The corresponding axiom schema for lists is $LISTINDUCTION: ⊗⊗∀u: [qn u ⊃ qP u] ∧ ∀u: [¬qn u ∧ qP qd u ⊃ qP u] ⊃ ∀u: qP u ⊗. Here qP is a predicate variable. These schemas are called principles of ⊗structural ⊗induction, since the induction is on the structure of the entities involved. Other schemas derived from principles of ⊗structural ⊗induction are possible and the best schema to use depends stongly on the problem at hand. Some examples will be given in a later section. Even the axiom schemas don't assure us that the only domain satisfying the axioms is that of the integers or the S-expressions as the case may be. Any first order theory whose axioms can be given effectively admits the so-called ⊗non-standard_models. However, it seems likely that the non-standard models of S-expressions, like the non-standard models of integers, will agree with the standard model for sentences of practical interest. .ss A Simple Example. In order to complete our description of the first order theory of LISP we need to be able to represent facts about recursively defined LISP functions. Given a recursive function definition we can form the ⊗functional_equation by replacing the "←" in the recursive function definition by "=" and universally quantifying over the argument variables. In the case of ⊗append which is defined by ⊗⊗⊗u * v ← qif qn u qthen v qelse qa u . [qd u * v]⊗ the corresponding functional equation is $APPEND: ⊗⊗∀u v: [u * v = qif qn u qthen v qelse qa u . [qd u * v]] ⊗. Sometimes the functional equation characterizes the function completely. For this to be the case we need to know that a function satisfying the equation exists and that it is unique. This essentially reduces to showing that the function is total. If the function is not total then we need the additional information provided by the ⊗minimiztion_schema. This is justified by the semantics of LISP programs based on the use of functionals and fixedpoints. Before proceeding with a more detailed discussion of these matters an example is in order. For the remainder of this section we will show how to use the axiom $APPEND together with the LISP axioms to prove some properties of ⊗append. In particular we will show $NIL-APPEND: ⊗⊗∀v: qNIL * v = v⊗ $ISTOT-APPEND: ⊗⊗∀u v: islist [u * v]⊗ $CAR-APPEND: ⊗⊗∀u v: [¬qn u ⊃ qa [u * v] = qa u]⊗ $CDR-APPEND: ⊗⊗∀u v: [¬qn u ⊃ qd [u * v] = [qd u] * v]⊗ $NOTNUL-APPEND: ⊗⊗∀u v: [[¬qn u ∨ ¬qn v] ⊃ ¬qn [u * v]]⊗ $AASOC-APPEND: ⊗⊗∀u v w: [u * v] * w = u * [v * w]⊗ First we prove $NIL-APPEND. By $APPEND and the axiom $NIL we have ⊗⊗⊗qNIL * v = qif qn qNIL qthen v qelse qa u . [qd u * v]⊗ and by $NULL this simplifies to ⊗⊗qNIL * v = v⊗ as desired. Next we prove $ISTOT-APPEND, i.e. that ⊗append is total. For this we use $LISTINDUCTION with ⊗⊗⊗qP u ≡ ∀v: islist [u * v] ⊗ obtaining the induction axiom .NOFILL ⊗⊗⊗[∀u: [qn u ⊃ ∀v: islist [u * v]] ∧ ⊗ ⊗⊗⊗∀u: [[¬qn u ∧ ∀v: islist [qd u * v]] ⊃ ∀v: islist [u * v]]]⊗ ⊗⊗⊗⊃ ∀u v: islist [u * v] . ⊗ .FILL The proof then breaks into two steps corresponding to the cases ⊗⊗qn u⊗ and ⊗⊗¬qn u⊗. In the first case we must show ⊗⊗⊗∀u: [qn u ⊃ ∀v: islist [u * v]] ⊗ which follows directly from $APPEND and $SORTED. In the second case we must show ⊗⊗⊗∀u: [[¬qn u ∧ ∀v: islist [qd u * v]] ⊃ ∀v: islist [u * v]] ⊗. To do this we assume ⊗⊗⊗¬qn u ∧ ∀v: islist [qd u * v] . ⊗ Then by $NULL, $CAR we have ⊗⊗issexp qa u⊗ and so by $CONS3 we have ⊗⊗⊗islist [qa u . [qd u * v]] . ⊗ From this and $APPEND, since we are in the case ⊗⊗¬qn u⊗, it follows that ⊗⊗⊗islist [u * v] . ⊗ $ISTOT-APPEND follows immediately from these two steps and the induction axiom. We now prove $CAR-APPEND. From $APPEND we have ⊗⊗⊗¬qn u ⊃ [u * v = qa u . [qd u * v]] .⊗ Now we use $CAR-CONS and obtain ⊗⊗⊗¬qn u ⊃ [qa [u * v] = qa u] ⊗ To justify using $CAR-CONS we need ⊗⊗issexp qa u⊗, ⊗⊗islist qd u⊗ and ⊗⊗islist [qd u * v]⊗ under the assumption that ⊗⊗¬qqn_u⊗. These follow from ($NULL, $CAR), $CDR2; and $ISTOT-APPEND respectively. $CDR-APPEND is proved similiarly with $CDR-CONS in place of $CAR-CONS. To prove $NOTNUL-APPEND we note first that ⊗⊗⊗¬qn u ⊃ ¬qn [u * v] ⊗ follows from $APPEND, $NULL, $CAR, $CDR2, $ISTOT-APPEND, and $CONS1. Second we have ⊗⊗⊗[qn u ∧ ¬qn v] ⊃ ¬qn [u * v] ⊗ by $APPEND. Combining these two we have the desired result. Finally we prove $ASSOC-APPEND. Again we use $LISTINDUCTION, this time with ⊗⊗⊗qP u ≡ ∀v w: [u * v] * w = u * [v * w] ⊗. First we show ⊗⊗⊗∀u: [qn u ⊃ ∀v w: [u * v] * w = u * [v * w]] ⊗. Assuming ⊗⊗qn u⊗ we have by $APPEND that ⊗⊗⊗[u * v] * w = v * w ⊗ and by $APPEND and $ISTOT-APPEND that ⊗⊗⊗u * [v * w] = v * w ⊗ proving the first step. The second step is to show that ⊗⊗⊗∀u: [[¬qn u ∧ ∀v w: [qd u * v] * w = [qd u] * [v * w]] ⊃ ∀v w: [u * v] * w = u * [v * w]] ⊗. We do this by assuming the lefthand side of the implication and proving a chain of equalities which will prove the righthand side of the implication. By $APPEND, $NOTNUL-APPEND and $ISTOT-APPEND we have ⊗⊗⊗[u * v] * w = qa [u * v] . [qd [u * v] * w]⊗ and by $CAR-APPEND and $CDR-APPEND ⊗⊗⊗qa [u * v] . [qd [u * v] * w] = qa u . [[qd u * v] * w] ⊗. By assumption ⊗⊗⊗qa u . [[qd u * v] * w] = qa u . [[qd u] * [v * w]] ⊗. Finally by $APPEND and $ISTOT-APPEND since we are in the case ⊗⊗¬qn u⊗ ⊗⊗⊗qa u . [[qd u] * [v * w]] = u * [v * w] ⊗. Combining these two steps with the induction axiom we have the desired result. In the above proofs we have been particularly careful with details such as showing ⊗⊗islist x⊗ where ⊗x is an expression to be substituted for ⊗u in some sentence. The proofs are in fact fairly close to the formal proofs given in Appendix {SECTION FOL}. In later examples we shall be more brief as the reader will be expected to be able to fill in the details. .ss Pseudo-logic. In this section we give a method for handling recursively defined predicates. Consider the recursive program ⊗⊗⊗occur[x, y] ← [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]⊗. If we were to treat this program in a manner analogous to the functional equation method described in the last section, we would represent the predicate ⊗occur by the sentence ⊗⊗⊗∀x y: [occur[x, y] ≡ [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]]⊗. However, in order to justify this representation we would have to use some kind of logic of partial predicates, because we could not be sure in advance that ⊗occur is total, and honest predicates cannot take the value qw; they can only be true or false. Instead, we introduce a domain TV of truth values consisting of the elements $TT and $FF and having characteristic predicate ⊗istv. The extension, TV%5+%*, of TV we shall call ETV. It consists of the elements $TT, $FF, and qw and has characteristic predicate ⊗isetv. By identifying $TT and $FF with appropriate LISP atoms TV could be considered as a subdomain of SE. For our purposes it makes no difference. We define pseudo-logical operators (⊗nnot, ⊗aand, ⊗oor) to imitate the logical operators (¬, ∧, ∨) and pseudo-predicates (⊗eeq, ⊗aatom) to imitate the basic LISP predicates (=, qqat). Now we can imitate the predicate ⊗occur by the recursive program ⊗⊗⊗occura[x, y] ← [x eeq y] oor [nnot aatom y aand [occura[x, qa y] oor occura[x, qd y]]]⊗ which has the functional equation ⊗⊗⊗∀x y: [occura[x, y] = [x eeq y] oor [nnot aatom y aand [occura[x, qa y] oor occura[x, qd y]]]]⊗. Using this equation and the S-expression induction axiom we can show ⊗⊗⊗∀x y: istv occura[x, y] ⊗ which is the statement that occura is total. If we define ⊗occur by ⊗⊗⊗∀x y: [occur[x, y] ≡ occura[x, y] = $$TT$] ⊗ then we can prove the original sentence proposed for representing ⊗occur. .bb ETV axioms We now give the axioms for extended truths values needed to make the above arguments and similar ones work. First the axioms describing the domains TV and ETV. .begin nofill $TVSORTS: ⊗etv, ⊗tv $VARIABLES: $SORTED: ⊗⊗P, Q ε etv⊗ ⊗⊗p, q ε tv⊗ .end $B2: ⊗⊗∀p: isetv p⊗ $B3: ⊗⊗isetv qw ∧ istv $TT ∧ istv $FF ⊗ $B4: ⊗⊗∀P: [P = $TT ∨ P = $FF ∨ P = qw]⊗ $B5: ⊗⊗∀p: [p = $TT ∨ p = $$FF$]⊗ $B6: ⊗⊗$TT ≠ $FF ∧ $TT ≠ qw ∧ $FF ≠ qw⊗ Next the axioms defining the functions on ETV corresponding to the pseudo-logical operators and pseudo-predicates. $B7: ⊗⊗∀P: [nnot P = qif [P = qw] qthen qw qelse qif [P = $$TT$] qthen $FF qelse $$TT$]⊗ $B8: ⊗⊗∀P Q: [P aand Q = qif [P = qw] qthen qw qelse if [P = $$TT$] qthen Q qelse $$FF$]⊗ $B9: ⊗⊗∀P Q: [P oor Q = qif [P = qw] qthen qw qelse qif [P = $$TT$] qthen $TT qelse Q]⊗ $B10: ⊗⊗∀X Y: [X eeq Y] = qif [¬issexp X ∨ ¬issexp Y] qthen qw qelse qif [X = Y] qthen $TT qelse $$FF$]⊗ $B11: ⊗⊗∀X: [aatom X = qif [¬issexp X] qthen qw qelse qif qat x qthen $TT qelse $$FF$]⊗ Finally a conditional function which takes elements of ETV as its first argument. $B12: ⊗⊗∀P X Y: [iif[P, X, Y] = qif [P = qw] qthen qw qelse qif [P = $$TT$] qthen X qelse Y]⊗ .bb ETV lemmas We now give some lemmas which show that the pseudo- operators and predicates behave as advertised. First we need to know that the functions map into ETV. $ETVNNOT: ⊗⊗∀P: isetv nnot P⊗ $ETVAAND: ⊗⊗∀P Q: isetv [P aand Q]⊗ $ETVOOR: ⊗⊗∀P Q: isetv [P oor Q]⊗ $ETVEEQ: ⊗⊗∀X Y: isetv [X eeq Y]⊗ $ETVAATOM: ⊗⊗∀X: isetv aatom X⊗ These lemmas are all a direct consequence of the function definitions and the axioms $SORTED, $B2 and $B3. Next are some lemmas stating that the functions defined above are total when restricted to the domains TV or SE as appropriate. $TVNNOT: ⊗⊗∀p: istv nnot p⊗ $TVAAND: ⊗⊗∀p q: istv [p aand q]⊗ $TVOOR: ⊗⊗∀p q: istv [p oor q]⊗ $TVEEQ: ⊗⊗∀x y: istv [x eeq y]⊗ $TVAATOM: ⊗⊗∀x: istv atom x⊗ These lemmas follow from the function definitions and the axioms $SORTED, $B3, $B5 and $B6. Next are some lemmas which show that the functions do indeed imitate their logical counterparts. $EQNNOT: ⊗⊗∀p: [nnot p = $TT ≡ ¬[p = $$TT$]]⊗ $EQAAND: ⊗⊗∀p q: [p aand q = $TT ≡ p = $TT ∧ q = $$TT$]⊗ $EQOOR: ⊗⊗∀p q: [p oor q = $TT ≡ p = $TT ∨ q = $$TT$]⊗ $EQEEQ: ⊗⊗∀x y: [x eeq y = $TT ≡ x = y]⊗ $EQAATOM: ⊗⊗∀x: [aatom x = $TT ≡ qat x]⊗ These lemmas can all be proved by simple case analysis. We prove $EQAAND and $EQEEQ as examples. By $SORTED, $B5, $B6, and $B8 we have ⊗⊗⊗p aand q = qif [p=$TT] qthen q qelse $FF ⊗ and $EQAAND follows immediately using $B6. By $SORTED and $B10 ⊗⊗⊗x eeq y = qif [x = y] qthen $TT qelse $FF ⊗ and $EQEEQ follows using $B6. Finally we give some lemmas that will be useful in later examples. $TVNOTATM: ⊗⊗∀x y: istv [nnot aatom x aand nnot aatom y]⊗ $EQNOTATM: ⊗⊗∀x y: [[nnot aatom x aand nnot aatom y] = $TT ≡ [¬qat x ∧ ¬qat y]]⊗ $TVNOTATM follows from $TVNNOT, $TVAATOM, and $TVAAND. $EQNOTATM follows from $EQAAND and ⊗⊗∀x:_nnot_aatom_x_=_$$TT$_≡_¬qat x⊗. The latter follows from $TVAATM, $EQNNOT and $EQAATOM. $POORF: ⊗⊗∀P: [P oor $FF = P]⊗ $FAANDQ: ⊗⊗∀Q: [$FF aand Q = $$FF$]⊗ $POORF follows from $B9 by case analysis using $B4 and $B6. $FAANDQ follows by simplification of $B8 using $B6. A formal proof of many of the above lemmas is included in Appendix {SECTION FOL}. .cb Exercise. Prove the statements made about ⊗occur and ⊗occura. Namely show ⊗⊗⊗∀x y: istv occura[x, y] ⊗ and ⊗⊗⊗∀x y: [occur[x, y] ≡ [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]]⊗. using the definitions ⊗⊗⊗∀x y: [occura[x, y] = [x eeq y] oor [nnot aatom y aand [occura[x, qa y] oor occura[x, qd y]]]]⊗ and ⊗⊗⊗∀x y: [occur[x, y] ≡ occura[x, y] = $$TT$]. ⊗ .ss An Extended Example. As a non trivial application of the techniques described in the previous sections, we will give a proof of correctness of the predicate ⊗samefringe which has been proposed as a solution of the SAMEFRINGE problem. This is the problem of determining whether or not two S-expressions have the same fringe using a minimum of space. (We will be concerned only with the correctness of ⊗samefringe since the efficiency is not an ⊗extensional property). The fringe of an S-expression, ⊗x, is a list of atoms in the order that they occur in ⊗x. Thus the fringe of $A is $(A) and the fringe of $$((A_._B)_._(C_._D))$ is $$(A_B_C_D)$. The LISP program for computing the fringe of an S-expression is !fcnfringe&sf ⊗⊗⊗fringe x ← qif qat x qthen <x> qelse [fringe qa x] * [fringe qd x]⊗ The predicate ⊗samefringe is computed by the LISP program !fcnsamefringe& ⊗⊗⊗samefringe[x, y] ← x = y ∨ [¬qat x ∧ ¬qat y ∧ same[gopher x, gopher y]]⊗ where !fcnsame& ⊗⊗⊗same[x, y] ← qa x = qa y ∧ samefringe[qd x, qd y]⊗ and !fcngopher& ⊗⊗⊗gopher x ← qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗ Using the method of the previous section we define an imitation of ⊗samefringe by .begin nofill ⊗⊗⊗samefringea[x, y] ← [x eeq y] oor [[nnot aatom x aand nnot aatom y]⊗ !fcnsamefringea& ⊗⊗⊗ aand samea[gopher x, gopher y]]⊗ .end where !fcnsamea& ⊗⊗⊗samea[x, y] ← [qa x eeq qa y] aand samefringea[qd x, qd y]⊗ Thus we have the functional equations .begin nofill $FRINGE: ⊗⊗∀x: [fringe x = qif qat x qthen <x> qelse [fringe qa x] * [fringe qd x]]⊗ $SAMEFRINGEA: ⊗⊗∀x y: [samefringea[x, y] = [x eeq y] oor [[nnot aatom x aand nnot aatom y]⊗ ⊗⊗aand samea[gopher x, gopher y]]]⊗ $SAMEA: ⊗⊗∀x y: [samea[x, y] = [qa x eeq qa y] aand samefringea[qd x, qd y]]⊗ $SAMEFRINGE: ⊗⊗∀x y: [samefringe[x, y] ≡ samefringea[x, y] = $$TT$]⊗ $SAME: ⊗⊗∀x y: [same[x, y] ≡ samea[x, y] = $$TT$]⊗ $GOPHER: ⊗⊗∀x: [gopher x = qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]]⊗ .end In order to prove that ⊗samefringea is total we will need the fact that ⊗samea maps into ETV. This is because in the case ⊗x is an atom or ⊗y is an atom we must have ⊗⊗isetv_samea[gopher_x,_gopher_y]⊗ in order to use the definition of ⊗aand even though the actual value is irrelevant. There are several ways to do this. One would be to define ⊗gopher of an atom to be qw, and have an axiom stating that ⊗samea produces qw if either argument is qw. Another is to take as part of the definition of ⊗samea that it maps into ETV, without stating for what arguments it actually produces qw. We have chosen the latter option as it seems cleaner. Thus we add the axiom $ETVSAMEA: ⊗⊗∀X Y isetv samea[X, Y]⊗ The goal is to prove the following three statements: $THM1: ⊗⊗∀x y: istv samefringea[x, y]⊗ $THM2: ⊗⊗∀x y: [samefringe[x, y] ≡ [x = y] ∨ [[¬qat x ∧ ¬qat y] ∧ same[gopher x, gopher y]]⊗ $THM3: ⊗⊗∀x y: [samefringe[x, y] ≡ fringe x = fringe y]⊗ $THM1 says that ⊗samefringea is total, $THM2 says that ⊗samefringe as defined via its imitatiom satisfies the intended equivalence, and $THM3 says that ⊗samefringe is correct. Due to the complicated form of the recursion defining ⊗samefringe, simple S-expression induction is not adequate to prove the above theorems. Therefore if we wish to carry out the proof by structural induction we must find an axiom schema appropriate for the problem. One way is to use induction on the size of the S-expressions involved. The size of an S-expression ⊗x is the number of atoms occuring in ⊗x and is computed by the LISP program !fcnsize& ⊗⊗⊗size x ← qif qat x qthen 1 qelse size qa x + size qd x⊗ ⊗size provides a mapping of S-expressions into the domain of natural numbers and allows us to transform the problem into one of natural number induction. In particular we will take for the axiom schema, the course of values induction schema $NUMBINDUCTION: ⊗⊗∀n: [∀m: [m < n ⊃ qP m] ⊃ qP n] ⊃ ∀n: qP n⊗ with ⊗⊗⊗qP n ≡ ∀x y: [size x + size y = n ⊃ THM[x, y]]⊗ where $THM: ⊗⊗∀x y: [THM[x, y] ≡ THM1[x, y] ∧ THM2[x, y] ∧ THM3[x, y]]⊗. In order to use the $NUMBINDUCTION axiom we will need the functional equation for ⊗size and some properties of the natural numbers. The characteristic predicate of the domain of natural numbers is ⊗natnum and we add to our list of axioms the following: $NUMSORTS: ⊗natnum $VARIABLES: ⊗⊗k, l, m, n ε natnum⊗ $ONE: ⊗⊗natnum 1⊗ $ISTOT-PLUS: ⊗⊗∀m n: natnum [m + n]⊗ $ASSOC: ⊗⊗∀l m n: l + [m + n] = [l + m] + n⊗ $ORDER-PLUS: ⊗⊗∀k l m n: [[k < l ∧ m < n] ⊃ k + m < l + n]⊗ $ORDER: ⊗⊗∀n: n < 1 + n⊗ $SIZE: ⊗⊗∀x: [size x = qif qat x qthen 1 qelse size qa x + size qd x]⊗ Here we have not attempted to axiomatize the natural numbers, but simply have taken as axioms those properties needed for the present problem. Now to proceed with the proof. In addition to the lemmas about ⊗append and the ETV lemmas proved in earlier sections, we will need some lemmas about ⊗gopher, ⊗fringe, ⊗size and combinations thereof. They are $GOOD-GOPHER: ⊗⊗∀x: [¬qat x ⊃ [issexp gopher x ∧ issexp qa gopher x ∧ issexp qd gopher x]]⊗ $GOOD-FRINGE: ⊗⊗∀x: [issexp fringe x ∧ ¬qat fringe x]⊗ $FRINGE-ATM: ⊗⊗∀x y: [[qat x ∨ qat y] ⊃ [fringe x = fringe y ≡ x = y]]⊗ $FRINGE-GOPHER: ⊗⊗∀x: [¬qat x ⊃ [qa fringe x = qa gopher x] ∧ [qd fringe x = fringe qd gopher x]]⊗ $ISTOT-SIZE: ⊗⊗∀x: natnum size x⊗ $SIZE-GOPHER: ⊗⊗∀x y: [[¬qat x ∧ ¬qat y] ⊃ [size qd gopher x +size qd gopher y] < [size x + size y]]⊗ We will give only a brief indication of the proof of these lemmas. Formal proofs are contained in Appendix_{SECTION FOL}. The key idea in proving things about ⊗gopher is to first prove properties of ⊗⊗gopher[x_._y]⊗ as gopher is only defined for non atoms and every non atom can be expressed as ⊗⊗x_._y⊗ for suitable ⊗x and ⊗y. For this purpose we start with some useful facts derived from $GOPHER, $FRINGE, $SIZE and the LISP axioms. $GOPHER-CONS-ATM: ⊗⊗∀x y: [qat x ⊃ gopher[x . y] = [x . y]]⊗ $GOPHER-CONS-NOTATM: ⊗⊗∀x y: [¬qat x ⊃ gopher[x . y] = gopher[qa x. [qd x . y]]]⊗ $FRINGE-CONS: ⊗⊗∀x y: [fringe[x . y] = fringe x * fringe y]⊗ $SIZE-CONS: ⊗⊗∀x y: [size[x . y] = size x + size y]⊗ To prove $GOOD-GOPHER first prove, by a straight forward use of $SEXPINDUCTION, that ⊗⊗∀x y: [issexp gopher[x . y] ∧ ¬qat gopher[x . y]]⊗ The lemma then follows from this and the axioms $CAR, $CDR1 and $CONS1. $GOOD-FRINGE folllows from ⊗⊗∀x: [islist fringe x ∧ ¬qn fringe x]⊗ , $SEXP1, and $NULL. The former is proved using $SEXPINDUCTION. For $FRINGE-ATM we assume ⊗⊗qat x⊗ and show ⊗⊗fringe_x_=_fringe_y_≡_x_=_y⊗. The lemma then follows from the symmetry of the occurrences of ⊗x and ⊗y. From the definition of ⊗fringe we have ⊗⊗fringe_x_=_<x>_=_[x_._qNIL]⊗. If ⊗⊗qqat_y⊗ the result follows using $EQ-SEXP. If ⊗⊗¬qqat_y⊗ then ⊗⊗x_≠_y⊗ and by $EQ-SEXP we need only prove ⊗⊗¬qqn_qqd_fringe_y⊗. But this follows from $CDR-APPEND and $NOTNUL-APPEND. To prove $FRINGE-GOPHER we use the "gopher trick" again and first prove ⊗⊗⊗∀x y: [qa fringe[x . y] = qa gopher[x . y] ∧ qd fringe[x . y] = fringe qd gopher[x . y]]⊗ using $SEPXINDUCTION. By $CAR-APPEND, $CDR-APPEND $GOOD-FRINGE and $FRINGE-CONS we have ⊗⊗⊗qa fringe[x . y] = qa fringe x, ⊗ and ⊗⊗⊗qd fringe[x . y] = [qd fringe x] * fringe y. ⊗ In the case ⊗⊗qat x⊗ the result follows from $NIL-APPEND, $GOPHER-CONS-ATM, and ⊗⊗fringe_x_=_[x_._qNIL]⊗ . In the case ⊗⊗¬qqat x⊗ we show ⊗⊗⊗fringe[x . y] = fringe[qa x . [qd x . y]] ⊗ using properties of ⊗append and $FRINGE-CONS. Then the result follows from the induction hypothesis and $GOPHER-CONS-NOTATM. $FRINGE-GOPHER now follows from the above using $CONSTRUCT. $ISTOT-SIZE is proved by a straight forward application of $SEXPINDUCTION. To prove $SIZE-GOPHER we first show ⊗⊗⊗∀x y: [size qd gopher[x . y] < size[x . y]]⊗ using $SEXPINDUCTION. In the case ⊗⊗qa x⊗ we have ⊗⊗⊗size qd gopher[x . y] = size y⊗ and ⊗⊗size[x . y] = 1 + size y⊗ by $SIZE, $SIZE-CONS and $GOPHER-CONS-ATM and the result follows by $ORDER. In the case ⊗⊗¬qqat_x⊗ we show ⊗⊗⊗size[x . y] = size[qa x . [qd x . y]]⊗ using $SIZE-CONS, $ASSOC and the LISP axioms. The result then follows from the induction hypothesis and $GOPHER-CONS-NOTATM. $SIZE-GOPHER now follows from $CONSTRUCT and $ORDER-PLUS. Now we are ready to prove the SAMEFRINGE theorem. The proof is divided into two cases. In the first case we assume ⊗⊗qat x ∨ qat y⊗. Then by the ETV lemmas ⊗⊗⊗nnot aatom x aand nnot aatom y = $FF ⊗, by $FAANDP and $ETVSAMEA ⊗⊗⊗$FF aand samea[gopher x, gopher y] = $FF ⊗, and by $POORF ⊗⊗⊗[x eeq y] oor $FF = x eeq y ⊗. Thus by $SAMEFRINGEA we have ⊗⊗⊗samefringea[x, y] = x eeq y⊗ and $THM now follows using the ETV lemmas, $FRINGE-ATM and $SAMEFRINGE. In the second case we assume ⊗⊗¬qat x ∧ ¬qat y⊗ and make use of the $NUMBINDCTION axiom and predicate as mentioned above. In particular we have the induction hypothesis ⊗⊗⊗∀m: [m < n ⊃ ∀x%41%* y%41%*: [size x%41%* + size y%41%* = m ⊃ THM[x%41%*, y%41%*]] ⊗. Taking ⊗⊗n = size x + size y⊗, ⊗⊗m = size qd gopher x + size qd gopher y⊗, ⊗⊗x%41%*_=_qqd_gopher_x⊗ and ⊗⊗y%41%*_=_qqd_gopher_y⊗ we have by $SIZE-GOPHER $THMCDRGO: ⊗⊗THM[qd gopher x, qd gopher y]⊗ Assigning these values to ⊗n and ⊗m is allowed since by $ISTOT-PLUS, $ISTOT-SIZE and $GOOD-GOPHER the expressions satisfy ⊗natnum. $THM1 now follows from $THMCDRGO, the ETV lemmas, $GOOD-GOPHER, $SAMEA and $SAMEFRINGEA. $THM2 follows for the above reasons and $SAME. By $SAMEA, $SAMEFRINGE, $GOOD-GOPHER, $THMCDRGO and the ETV lemmas it follows that .NOFILL ⊗⊗⊗samea[gopher x, gopher y] = $TT ≡ ⊗ ⊗⊗⊗[qa gopher x = qa gopher y] ∧ [fringe qd gopher x = fringe qd gopher y]⊗. .FILL Using $FRINGE-GOPHER, $THM2, and $SAME we have ⊗⊗⊗samefringe[x, y] ≡ x = y ∨ [[qa fringe x = qa fringe y] ∧ [qd fringe x = qd fringe y]]⊗. Finally $THM3 follows from $EQ-SEXP and $GOOD-FRINGE. Combining the two cases and applying the induction axiom we conclude ⊗⊗⊗∀n: ∀x y: [[size x + size y] = n ⊃ THM[x, y]]⊗ and by $ISTOT-SIZE and $ISTOT-PLUS it follows that ⊗⊗⊗∀x y: THM[x, y] . ⊗ In the above proof we could have equally well used the predicate ⊗⊗⊗qP n ≡ ∀x y: [size x = n ⊃ THM[x, y]]⊗ since the recursive call to ⊗samefringe always reduces the size of the first argument. Another version of ⊗samefringe without any auxilliary functions is .begin nofill turnon "∂" .n←16 ∂(n)⊗⊗samefringe[x, y] ← ⊗ ∂(n)⊗⊗ x = y ∨ ⊗ ∂(n)⊗⊗ [¬qat x ∧ ¬qat y ∧ ⊗ !fcnsamefringe&1 ∂(n)⊗⊗ [qif qat qa x qthen [qif qat qa y qthen qa x = qa y ∧ samefringe[qd x, qd y] ⊗ ∂(n)⊗⊗ qelse samefringe[x, qaa y. [qda y . qd y]]]⊗ ∂(n)⊗⊗ qelse samefringe[qaa x . [qda x . qd x], y]. ⊗ .end Note that a recursive call to ⊗samefringe does one of the following: 1) decreases ⊗⊗size x + size y⊗ 2) leaves ⊗⊗size x + size y⊗ and ⊗⊗size qa x⊗ invariant and decreases ⊗⊗size qa y⊗ or 3) leaves ⊗⊗sixe x + size y⊗ and ⊗⊗size qa y⊗ invariant and decreases ⊗⊗size qa x ⊗. .TURN ON "↑[]" This can lead to a choice of an induction axiom schema in at least two ways. If in the $NUMBINDUCTION schema we let ⊗n and ⊗m range over all ordinals less than a given one it becomes a schema of transfinite induction. Ordinary induction is obtained as a special case where the bounding ordinal is qW the least transfinite ordinal. If we take the bounding ordinal to be qW↑[qW] then the SAMEFRINGE theorem for the above version of ⊗samefringe can be proved using the predicate .TURN OFF ⊗⊗⊗qP n ≡ ∀x y: [[size x +size y]qW + size qa x + size qa y = n ⊃ THM[x, y]]⊗ (Note that THM2 will need to be modified to account for the new form of ⊗samefringe.) Alternately one could axiomatize the lexicographic ordering of triples of numbers by .NOFILL ⊗⊗⊗∀l%41%* m%41%* n%41%* l m n: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ≡ ⊗ ⊗⊗⊗[l%41%* < l] ∨ [l%41%* = l ∧ m%41%* < m] ∨ [l%41%* = l ∧ m%41%* = m ∧ n%41%* < n]]⊗ .FILL This ordering is well-founded (has no infinite decreasing sequences) and so we have a schema analogous to $NUMBINDUCTION given by .NOFILL ⊗⊗⊗∀l m n: [∀l%41%* m%41%* n%41%*: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ⊃qP(l%41%*, m%41%*, n%41%*)] ⊃ qP(l, m, n)]⊗ ⊗⊗⊗⊃ ∀l m n: qP(l, m, n)⊗ .FILL The SAMEFRINGE theorem can now be proved using this schema with the predicate ⊗⊗⊗qP(l, m, n) ≡ ∀x y: [l = size x +size y ∧ m = size qa y ∧ n = size qa x ⊃ THM[x, y]]⊗ .ss Functionals and Least Fixedpoints. Now we will describe a method for determining the function computed by a recursive program. This will allow us to justify the use of the functional equation to represent a total function. It will also provide a means of justifying the use of the functional equation together with the minimization schema to represent partial functions in general. The latter will be discussed in a later section. We are interested in recursive programs of the form ⊗⊗⊗f x ← qt[f] x ⊗ where qt is a computable functional. A functional is a higher order function which takes functions as arguments as well as ordinary arguments. The result of applying a functional to a function is a function which is then applied to the rest of the arguments. For example the LISP program ⊗mapcar defines a functional. We will consider functiionals constructed using a function variable and a set of base functions and predicates in a manner similar to the formation of λ-expressions (but omitting quantifiers). Functionals constructed in this manner are called ⊗term ⊗functionals. In the case of LISP programs, the non-logical functions and predicates are ⊗car, ⊗cdr, ⊗cons, ⊗atom and ⊗null. For example, for the function ⊗append the functional is ⊗⊗⊗qt = λF: λx y: [qif qn x qthen y qelse qa x . F[qd x,y]]⊗ or, using infix notation, ⊗⊗⊗qt = λOP: λx y: [qif qn x qthen y qelse qa x . [qd x OP y]]⊗. In order to say what function is computed by a recursive program of the form given above we will need to introduce the concepts of ⊗partial ⊗ordering and of ⊗least ⊗fixedpoints. We give here only a brief summary. A more complete discussion can be found in (Manna 1974, Chapter 5). Given a domain D, we form a domain D%5+%* by adjoining the undefined element qw to D. We use upper case letters to range over D%5+%* where the corresponding lower case letters range over D. A partial ordering, q≤ (read "less defined than or equal"), on D%5+%* is defined by ⊗⊗⊗X q≤ Y ≡ X = qw ∨ X = Y ⊗. (Recall that a partial ordering on a set S is a relation on (S $x S) that is transitive, reflexive and antisymmetric.) For example in the domain SE%5+%* we have qw_q≤_qNIL and qNIL_q≤_qNIL, but not qNIL_q≤_(qNIL_._qNIL). This partial ordering (sometimes called the "flat" partial ordering) is indeed trivial. A partial ordering can be represented by a diagram in which all elements less than but not equal to a given element are "below" that element. For our trivial ordering the diagram has only two layers: the bottom layer consisting of the single element qw and a top layer consisting of the rest. Hence the name "flat". Despite the trivial nature of this particular partial ordering, the concept turns out to be very useful. Given domains D1 and D2 and a partial function ⊗f: D1→D2, we extend ⊗f to a function from D1%5+%* to D2%5+%* by defining ⊗⊗f_qw_=_qw⊗ and, if ⊗f is undefined for ⊗x in D1, then ⊗⊗f_x_=_qw⊗. (Note that we use the same symbol to denote the undefined element regardless of domain. We shall also use this symbol to denote a totally undefined function. Context will make it clear what is being denoted by qw.) Other extensions are possible but we will not consider them. We will not distinguish between a function and its extension as we are considering only one extension. We "lift" the partial orderings on D1%5+%* and D2%5+%* to the set of partial functions from D1%5+%* to D2%5+%* by defining ⊗⊗⊗f q≤ g ≡ ∀x in D1: f x q≤ g x ⊗. For example if D1 and D2 are the domain SE, ⊗⊗⊗f%41%* = λx: [qif qat x qthen x qelse qw]⊗ and ⊗⊗⊗f%42%* = λx: [qif qat x qthen x qelse qif qat qa x qthen qa x qelse qw] ⊗. then ⊗⊗f%41%* q≤ f%42%* ⊗. The partial ordering on the function domains is not as trivial as that on the underlying domains but it is still very easy to work with. A useful concept here it that of ⊗lub (least upper bound to be precise). ⊗lub acts on sets of functions and produces the least function in the domain that contains (or is equal to) every function in the set, if such a function exists. A special case where ⊗lub is always defined is the following. Let ⊗⊗f⊗%4i%* be a set of functions satisfying ⊗⊗⊗f%4i%* q≤ f%4i+1%*⊗ for all ⊗i. Such a set is called a ⊗chain. The ⊗lub of a chain always exists. Call the resulting function ⊗f, then we can compute ⊗f as follows. If for some ⊗n ⊗⊗f%4n%*[x]_≠_qw⊗ then ⊗⊗f[x]_=_f%4n%*[x]⊗. If no such ⊗n exists then ⊗⊗f[x]_=_qw⊗. This works because of the simple nature of the partial ordering. .xgenlines ← xgenlines-2; If qt is a functional mapping functons from D1 to D2 to functions of the same type then a function ⊗f satisfying ⊗⊗f_=_qt[f]⊗ is a ⊗fixedpoint of qt. If furthermore for any other function ⊗g we have ⊗⊗g_=_qt[g]_⊃_f_q≤_g⊗ then ⊗f is the ⊗least ⊗fixedpoint of qt. For our restricted class of functionals the least fixedpoint always exists. We denote the least fixedpoint of qt by qY[qt]. The existence of qY[qt] is due to the fact that our functionals have some very special properties. One such property is ⊗monotonicity. A functional, qt that is monotonic preserves the partial ordering of its function domain. In particular, for functions ⊗f and ⊗g, qt must satisfy ⊗⊗⊗f q≤ g ⊃ qt[f] q≤ qt[g] . ⊗ A second propery is ⊗continuity. A continuous functional is monotonic and must preserve ⊗⊗lub⊗'s of chains of functions. In particular if qt is a continuous functional and ⊗⊗f%4i%*⊗ is a chain of functions then the set ⊗⊗qt[f%4i%*]⊗ of functions is also a chain and ⊗⊗⊗qt[lubα{f%4i%*α}] = lubα{qt[f%4i%*]α}⊗. Now we show how to construct qY[qt] for a continuous functional qt. Let ⊗⊗⊗f%40%* = qw⊗ and ⊗⊗f%4i+1%* = qt[f%4i%*] ⊗. Then ⊗⊗⊗qw = f%40%* q≤ f%41%* = qt[f%40%*]⊗ and, since qt is monotonic, ⊗⊗⊗f%4i%* q≤ f%4i+1%*⊗ for all ⊗i. .xgenlines ← xgenlines-1 Thus the functions ⊗⊗f%4i%*⊗ form a chain, ⊗⊗lubα{f%4i%*α}⊗ is defined, and ⊗⊗qY[qt]_=_lubα{f%4i%*α}⊗ . Intuitively one can think of the ⊗⊗f%4i%*⊗'s as forming a sequence of successively better approximations to the function qY[qt]. What is being approximated is the domain of definition. Repeated applications of qt increase the domain of definition (unless, of course, we have for some ⊗i that ⊗⊗f%4i%*⊗_=_qY[qt]). For example if ⊗⊗⊗qt = λf: λx: [qif qat x qthen x qelse f[qa x]] ⊗ then, for ⊗⊗f%41%*⊗ and ⊗⊗f%42%*⊗ as defined above, we have ⊗⊗⊗f%41%* = qt[qw]⊗ and ⊗⊗f%42%* = qt[f%41%*] ⊗. The ⊗n mentioned above in the description of how to compute ⊗lub of a chain of functions is essentially the number of ⊗⊗car⊗'s that must be applied to ⊗x to reach an atom. [A parenthetical remark: the notions of ⊗monotonicity and ⊗continuity defined above are generalizations of those encountered in a calculus or analysis course in mathematics. Such generalizations are common in the study of topology and the above arguments can be formulated in a topological framework.] .xgenlines←xgenlines-3; Now we are ready to define the function computed by a recursive program and to show how this function is characterized by the corresponding functional equation in the case of total functions. If qt is a term_functional then the function, ⊗f, computed by the recursive program, ⊗⊗f_x_←_qt[f]_x⊗ is qY[qt]. Thus ⊗f satisfies the functional equation ⊗⊗⊗∀x: [f x = qt[f] x] . ⊗ If ⊗f is total then ⊗⊗f_x_≠_qw⊗ for any ⊗x in D1. This means that for any function ⊗g ⊗⊗⊗f q≤ g⊗ iff ⊗⊗f = g . ⊗ Thus ⊗f is the unique function satisfying the functional equation. In the case that ⊗f is not total the functional equation is not sufficient. We also need to express the fact that ⊗f is the least function satisfying this equation. The minimization schema will do that. .ss The Minimization Schema. As mentioned before, the functional equation of a program doesn't in general completely characterize it. For example, the program ⊗⊗⊗f1 x ← f1 x ⊗ leads to the sentence ⊗⊗⊗∀x: [f1 x = f1 x] ⊗ which provides no information although the function ⊗f1 is undefined for all ⊗x. This is not always the case, since the program ⊗⊗⊗f2 x ← [f2 x] . qNIL ⊗ has the functional equation ⊗⊗⊗∀x: [f2 x = [f2 x] . qNIL] . ⊗ from which ⊗⊗∀x: [¬issexp f2 x]⊗ can be proved by induction. In order to characterize recursive programs, we need some way of asking for the least defined solution of the functional equation. That is we want the least fixedpoint of the defining functional. Consider the recursive program ⊗⊗⊗f x ← qt[f] x ⊗ which has the functional equation ⊗⊗⊗∀x: [f x = qt[f] x] . ⊗ It can be shown that requiring a fixedpoint ⊗f of a functional qt to be minimal is equivalent to the ⊗minimization_schema ⊗⊗⊗∀x: [qt[F] x q≤ F x] ⊃ ∀x: [f x q≤ F x]⊗ where ⊗F is a function variable. The partial ordering can be removed from the statement of the minimization schema by noting that for functions ⊗f and ⊗g we have ⊗⊗⊗f q≤ g ≡ ∀x: [isD f x ⊃ f x = g x]⊗ where D is the domain containing the range of ⊗f and the predicate ⊗isD states that its argument is in the domain D. Thus ⊗⊗isD_f_x⊗ means that ⊗⊗f_x_≠_qw⊗. The minimization schema then becomes ⊗⊗⊗∀x: [isD qt[F] x ⊃ F x = qt[F] x] ⊃ ∀x: [isD f x ⊃ f x = F x] ⊗. The simplest application of the schema is to show that the program for ⊗f1 given above computes the totally undefined function. The schema becomes ⊗⊗⊗∀x: [F x q≤ F x] ⊃ ∀x: [f1 x q≤ F x] ⊗. The left side of the implication is identically true. Taking F[x] = qw, and remembering that ⊗⊗X_q≤_qw⊗ only if ⊗⊗X_=_qw⊗, the right side tells us that ⊗⊗f1_x_=_qw⊗. The minimization schema provides an alternate method for proving the correctness of ⊗samefringe. To simplify matters we eliminate the auxilliary function ⊗samea from the definition of ⊗samefringea thus eliminating the problem of having to deal with mutually recursive programs. The functional defining ⊗samefringea now becomes .NOFILL ⊗⊗⊗qt = λF: λx y: [[x eeq y] oor [[nnot aatom x aand nnot aatom y] aand ⊗ ⊗⊗⊗ [[qa gopher x eeq qa gopher y] aand F[qd gopher x, qd gopher y]]]] ⊗. .FILL Now we form an axiom schema from the minimization schema by using the qt given above and ⊗samefringea for ⊗f. We instantiate this schema with ⊗⊗⊗F[x, y] = fringe x eeq fringe y . ⊗ The proof then consists of the following steps 1) ⊗⊗∀x y: [istv qt[F] [x, y]]⊗ 2) ⊗⊗∀x y: [F[x, y] = qt[F] [x, y]]⊗ 3) ⊗⊗∀x y: istv samefringea[x, y]⊗ from 1) - 3) and the axiom instantiation we conclude 4) ⊗⊗∀x y: [fringe x eeq fringe y = samefringea[x, y]]⊗ from 3) we know that ⊗samefringea[x,_y] is either $TT or $FF and so by a simple case analysis using the TV-lemmas, the fact that $TT ≠ $FF, the definition of ⊗samefringe and 4) we conclude 5) ⊗⊗∀x y: [samefringe[x, y] ≡ fringe x = fringe y]⊗ as desired. The minimization schema can sometimes be used to show partial correctness. For example, the well known 91-function is defined by the recursive program over the integers ⊗⊗⊗f91 x ← qif x > 100 qthen x - 10 qelse f91 f91 [x + 11] ⊗. The goal is to show that ⊗⊗⊗∀x: [f91 x = qif x > 100 qthen x - 10 qelse 91] . ⊗ We apply the minimization schema with ⊗⊗⊗F x = qif x > 100 qthen x - 10 qelse 91 , ⊗ and it can be shown by an explicit calculation without induction that the premiss of the schema is satisfied, and this shows that ⊗f91, whenever defined has the desired value. The method of ⊗recursion ⊗induction is also an immediate application of the minimization schema. If we show that two functions satisfy the schema of a recursive program, we show that they both equal the function computed by the program whereever the function is defined. The utility of the minimization schema for proving partial correctness or non-termination depends on our ability to name suitable comparison functions. ⊗f1 and ⊗f91 were easily treated, because the necessary comparison functions could be given explicitly without recursion. Any extension of the language that provides new tools for naming comparison functions, e.g. going to higher order logic, will improve our ability to use the schema in proofs. The minimization schema can be regarded as an axiom schema involving a second order function variable qt. What can be substituted for qt is a quantifier free λ-expression in a first order function variable. It may be interesting to study the sets of first order sentences that can be generated by such second order sentence schemata. Presumably, sets of sentences can be generated in this way that cannnot be generated by schemata with only first order function variables. .cb Exercises. .item←0 #. Simple structural induction proofs. Prove the following statements. ##. ⊗⊗∀u: u * qNIL = u⊗ ##. ⊗⊗∀u: islist reverse1 u⊗ ##. ⊗⊗∀u: reverse u = reverse1 u⊗ ##. ⊗⊗∀u v: reverse[u * v] = [reverse v] * [reverse u]⊗ ##. ⊗⊗∀u: reverse reverse u = u⊗ ##. ⊗⊗∀x: flatten x = fringe x⊗ ##. ⊗⊗∀x: (¬qat x ⊃ size gopher x = size x)⊗ ##. ⊗⊗∀x: (¬qat x ⊃ qat qa gopher x)⊗ where the necessary LISP function definitions are: ⊗⊗u * v ← qif qn u qthen v qelse qa u . [qd u * v]⊗ ⊗⊗reverse1 u ← if qn u qthen qNIL qelse [reverse1 qd u] * <qa u>⊗ ⊗⊗reverse u ← rev[u, qNIL]⊗ ⊗⊗rev[u, v] ← qif qn u qthen v qelse rev[qd u, qa u . v]⊗ ⊗⊗flatten x ← flat[x, qNIL]⊗ ⊗⊗flat[x, u] ← qif qat x qthen [x . u] qelse flat[qa x, flat[qd x, u]]⊗ ⊗⊗fringe x ← qif qat x qthen <x> qelse [fringe qa x] * [fringe qd x]⊗ ⊗⊗gopher x ← qif qat qa x qthen x qelse gopher[qaa x . [qda x . qd x]]⊗ ⊗⊗size x ← qif qat x qthen 1 qelse size qa x + size qd x⊗ .bb 2. Properties of substitutions and substitution lists. With function definitions as given below, ⊗⊗subst[x,_y,_z]⊗ is the result of replacing the variable ⊗y by the S-expression ⊗x whereever ⊗y occurs in ⊗z. If ⊗s is a list of substitutions of the form ⊗⊗y_._x⊗ then ⊗⊗sublis[z,_s]⊗ is the result of "simultaneously" performing all of the substitutions on the list to ⊗z. If ⊗s1 and ⊗s2 are lists of substitutions then ⊗s1 @ ⊗s2 is "composition" of the two. Prove the following properties. .NOFILL i) ⊗⊗∀x y z: subst[x, y, z] = sublis[z, <y . x>]⊗ ii) ⊗⊗∀z s1 s2: sublis[z, s1 @ s2] = sublis[sublis[z, s1], s2]⊗ iii) ⊗⊗∀z s1 s2 s3: sublis[z, s1 @ [s2 @ s3]] = sublis[z, [s1 @ s2] @ s3]⊗ iv) ⊗⊗∀x y z: (¬occur[y, z] ⊃ subst[x, y, z] = z)⊗ v) ⊗⊗∀x x1 y y1 z: ((y ≠ y1 ∧ ¬occur[y, x1]) ⊃ ⊗ ⊗⊗subst[x1, y1, subst[x, y, z]] = subst[subst[x1, y1, x], y, subst[x1, y1, z]])⊗ where ⊗⊗assoc[x, s] ← qif qn s qthen qNIL qelse qif x = qaa s qthen qa s qelse assoc[x, qd s]⊗ ⊗⊗subst[x, y, z] ← qif qat z qthen [qif y = z qthen x qelse z] ⊗ ⊗⊗qelse subst[x, y, qa z] . subst[x, y, qd z]⊗ ⊗⊗occur[x, y] ← [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]⊗. ⊗⊗sublis[x, s] ← qif qat x qthen α{assoc[x, s]α}[λz: qif qn z qthen x qelse qd z]⊗ ⊗⊗qelse sublis[qa x, s] . sublis[qd x, s]⊗ ⊗⊗s1 @ s2 ← subsub[s1, s2] * s2⊗ ⊗⊗subsub[s1, s2] ← qif qn s1 qthen qNIL qelse [qaa s1 . sublis[qda s1, s2]] . subsub[qd s1, s2]⊗ .FILL .bb 3. Pattern matching and unification properties. (This is a fairly substantial exercise.) With the further function definitions given below, ⊗⊗inst[x,_y,_qNIL]⊗ is $NO if ⊗x is not and instance of the pattern ⊗y, and otherwise is the list of substitions which will convert ⊗y into ⊗x. In the latter case we have ⊗⊗x_=_sublis[y,_inst[x,_y,_qNIL]⊗. Prove i) ⊗⊗∀x y s: (inst[x, y, s] ≠ $NO ⊃ x = sublis[y, inst[x, y, s]])⊗ ⊗unify[x,y] attempts to find the most general pattern which is an instance of both ⊗x and ⊗y. If no such pattern exists the it returns $NO, otherwise it returns a list of substitutions which will convert both ⊗x and ⊗y into that pattern. Prove ii) ⊗⊗∀x y: (unify[x, y] ≠ $NO ⊃ sublis[x, unify[x, y]] = sublis[y, unify[x, y]])⊗ iii) ⊗⊗∀x y: (unify[x, y] = $NO ⊃ ∀s: sublis[x, s] ≠ sublis[y, s])⊗ iv) ⊗⊗∀x y s: (sublis[x, s] = sublis[y, s] ⊃ ∃s1: ∀z: sublis[z, s] = sublis[z, unify[x, y] @ s1])⊗ where .NOFILL ⊗⊗inst[x, y, s] ← qif s = $NO qthen $NO ⊗ ⊗⊗qelse qif qat y qthen [qif isvar y qthen ⊗ ⊗⊗α{assoc[y, s]α}[λz: qif qn z qthen [y . x] . s qelse qif qd z = x qthen s qelse $NO ]⊗ ⊗⊗qelse qif y = x qthen s qelse $NO ]⊗ ⊗⊗qelse qif qat x qthen $NO ⊗ ⊗⊗qelse inst[qd x, qd y, inst[qa x, qa y, s]]⊗ ⊗⊗isvar x ← x = $U ∨ x = $V ∨ x = $W ∨ x = $X ∨ x = $Y ∨ x = $Z ⊗ ⊗⊗unify[x, y] ← qif x = y qthen qNIL⊗ ⊗⊗qelse qif isvar x qthen [qif occur[x, y] qthen $NO qelse <x . y>]⊗ ⊗⊗qelse qif isvar y qthen [qif occur[y, x] qthen $NO qelse <y . x>]⊗ ⊗⊗qelse qif [qat x ∨ qat y] qthen $NO ⊗ ⊗⊗qelse α{unify[qa x,qa y]α}⊗ ⊗⊗[λs1: qif s1 = $NO qthen $NO ⊗ ⊗⊗qelse α{unify[sublis[qd x, s1],sublis[qd y, s1]]α}⊗ ⊗⊗[λs2: qif s2 = $NO qthen $NO qelse s1 @ s2]]⊗ .FILL