PDF file - LFCS - University of Edinburgh
Contents
1. E F F en gt Un E F Hf e en gt CW Un f O EF v1 Un Edom This is the only rule that introduces partiality into the semantics it assigns meanings to certain fully applied occurrences of f but not to others There is no clash here with rule 4 2 iv for application since there is no value v such that E F f e n 1 v because we have not assigned any independent meaning to f We can now prove the following properties Thus our semantics is as strict for f n expressions as it is for their eta reducts This is not the case for the semantics of Standard ML for instance 8Tn fact since here we are not handling mutual recursion we never require F to contain more than one entry 13 Proposition 3 i Given any well typed environment E function environment F and expres sion e possibly containing occurrences of f there is at most one value v such that E F F e v is derivable using the rules of 4 2 together with the rule x ui If E F F e v is derivable in this system and e has type t then ve ze iii If E F f 0 F e v is derivable and 0 S T extends 0 then also E F f 0 e v is derivable Proof i and ii are proved by simultaneous induction as in Proposition 1 For iii just observe that any valid derivation remains valid when is replaced everywhere by 6 O We now show how given an approximation 0 to f we can construct a next approximation F0 We su2. 2 we have E Ftee if E Fte and E Fr e iff xe gt e gt true iff lt e e gt true e If e is of the form Qz e Q a binder then by rules viii and ix of Section 4 2 we have E F H Qa t e if E x v FH el fralve t iff e Jew true for alve ft if lt Qza t e gt true The other cases are handled similarly using the appropriate clauses in the definition of gt 0O Proposition 9 Suppose A is first order Then the axioms DOM f paty patin lt exp gt t for DOM f are valid under the given interpretations of f and DOM f Proof Clearly 4 is valid provided for any environment E giving interpretations to the pattern variables we have pata lz patin z dom 6 iff lt exp gt pr r true 16 But this holds in our model since lt exp gt pe r true iff DE F exp by Lemma 8 iff patalz patin z dom FO by definition of F and dom F dom fx O Finally we need the following proposition which says that the general case may be reduced to the first order case Proposition 10 Let A be a general declaration If the axioms generated from A are valid under the given interpretation for f and DOM f then the axioms generated from A are likewise valid Proof Note first that A and A yield the same values for f and DOM f by definition For the axioms t for f we need the fact that erp o erpi lp where
3. Verification for Fault Tolerant Architec tures Prolegomena to the Design of PVS IEEE Transactions on Software Engineering 21 2 107 125 1995 J Rushby F von Henke and S Owre An Introduction to Formal Specific ation and Verification using EHDM Technical Report SRI CSL 91 02 SRI International 1991 D S Scott Identity and existence in intuitionistic logic In Lecture Notes in Mathematics Volume 735 661 696 Springer Verlag 1979 J M Spivey Understanding Z A Specification Language and its Formal Semantics Cambridge Tracts in Computer Science 3 CUP 1988 22
4. and e has type t then v t Proof By simultaneous induction on the structure of e If e is a Case ex pression then rule v applies for some unique value of i since the patterns are exhaustive and non overlapping If e is an application then the side condition in rule iv automatically holds since by the induction hypothesis u belongs to the appropriate total function space O Definition 2 If E F F e v is derivable we write elzr v We also write le in place of le z and e in place of ely Note that by Proposition 1 2 this defines e for all closed terms e 4 3 Interpretation of functions We now give the interpretation of f un definitions As in Section 2 we consider just a single declaration of the form fun f paty pati exp f pate paton expe f patm patmn e pm mutual recursion can be dealt with similarly We will find it convenient to distinguish notationally between this declaration and the function f it declares we thus use A to denote the piece of syntax constituting the above declaration 12 Our goal is to give definitions of f and DOM f We regard the meaning of A as being given by these two components AJ f DOM f Suppose that the pati are patterns of type s and the exp are expressions of type t Then we expect to obtain f E s gt gt s gt t DOM f si x x sn bool The first step in de
5. formulae In specification languages such as Z writing such formulae would seem to be good practice in any case The loose specification interpretation may also be appropriate in the context of hardware verification Suppose we wish to reason about a hardware component 19 whose behaviour is only specified for certain input values Typically the design of such a component will ensure that it still exhibits some determinate behaviour even on incorrect inputs though what this behaviour is may not be specified In this case our scheme would be particularly suitable the conclusions derived in the logic would be correct for any component satisfying the specification However there are problems if we try to use our logic to reason about the behaviour of programs Although in Sections 2 and 3 we used program termination as an analogy to help motivate our scheme this analogy should not be pressed too far A non terminating program is not the same as a program returning an unknown value but our semantics is not capable of reflecting this distinction Here LPF reflects the real world situation perhaps more faithfully We now give some examples of predicates that are misleading if interpreted as statements about Standard ML programs The first kind of discrepancy arises in connection with functions of higher type Consider the following declarations fun apply f x f x fun id 0 id S n 0 S apply id n In Standard ML
6. patin lz dom s gt bo patia z patin z exper But this assertion is indeed true in our model since from Definition 4 and the remark following it it is easy to see that lexpilpr r FO pata z patin z where if either side is defined then so is the other O The corresponding theorem for the DOM f axioms is somewhat harder Let us write E F F e to mean e z r is defined i e E F F e v for some v The following lemma says that this property behaves formally like the operator lt _ gt defined in Section 2 Lemma 8 Lete be any first order expression relative tof and n and suppose E is any environment giving interpretations to all the constants and free variables ofe other thanf Then E F F el iff lt e gt pr r true Proof By induction on the structure of e We consider only a selection of the cases 15 e If e is an atom other than f then lt e gt z r true always likewise E F e always since e z r E e e Ife is of the form f e eg with k lt n then k n by the assumption that e is first order But now BRT e Oy if E FF el fri lt i lt n and ler e r enl gF dom 6 iff lt e gt gt true forl1 lt i lt n and DOM f e1 n true iff f e1 en gt true by definition of lt gt e If e is of the form e e where e is not of the form f e ep with k lt n then by rule iv of Section 4
7. D is the updated environment D f f But this follows easily by induction from the fact that the eta rule is valid in our model f Cir ees ex lo fn LTk 1 Ln gt f Ci aes CR CREI woos Ln p For the axioms tf it suffices to note that the predicates exp gt gt and lt xp gt are syntactically identical this follows by induction from the fact that K e Cp ST oy gt sep k es n gt O This completes the proof that our axioms are valid In order to show that our system was consistent we would also need to check that the inference rules of our logic were sound for our model For any reasonable formulation of higher order logic this would be completely routine 5 Further remarks We conclude with some miscellaneous remarks concerning the strengths subtleties and weaknesses of our approach We also mention some areas where there is scope for further work 17 5 1 Quantifiers and any Our treatment of the binding operators in Section 3 v deserves further comment The behaviour of any in combination with recursion is especially subtle For the quantifiers foral and exists we could have given a more generous interpretation for instance in Section 3 we could have defined exists ve gt forall z lt e gt exists z lt e gt e with corresponding changes to the semantic clauses in Section 4 2 However in the case of any we are forced to take a very strict interpre
8. F esu E F F esv E F F ee u v ee doe we will see later that the side condition is redundant v E FreesulsFl pnsau ER s Fre sv dom E FV p E F case eof py gt ei pk gt ek gt v com Pi where 1 lt i lt k and EE means the environment in which the bindings in E are enriched and possibly overwritten by those in F vi E FF esv E oF re Sy E F F eze gt po vi E F F es gt sv E sFre sv E F Pee gt vrv and similarly for the other propositional connectives 11 viii E z v F F e gt u v for eachv jt E F F N ctes u dom u t ix E x v F F e u v foreachve t B E F Fany z t e gt choose u dom u t where for each type t we have a semantic choice function choose satisfying u choose u true for all u Av false x E x v F F e gt u v foreachve t E F H forall x t e u Av trie and dually for exists dom u Note that in general viii ix and x will be infinitary rules so our derivation trees may be infinite However they will always have finite depth by induction on the size of e The following are now easy observations Proposition 1 i Given any well typed environment E function environment F and expres sion e where dom E contains all constants and free variables appearing in e there is a unique value v such that E F F e gt v is derivable using the above rules ii If E F F e v is derivable
9. Partial Functions in a Total Setting Simon Finn si mon ahl co uk Michael Fourman M Fourman ed ac uk John Longley j rl fcs ed ac uk January 19 1996 Abstract We discuss a scheme for defining and reasoning about partial recursive functions within a classical two valued logic in which all terms denote We show how a total extension of the partial function introduced by a recursive declaration may be axiomatised within a classical logic and illustrate by an example the kind of reasoning that our scheme supports By presenting a naive set theoretic semantics we show that the system we propose is logic ally consistent We discuss some of the practical advantages and limitations of our approach in the context of mechanical theorem proving 1 Introduction Partial functions appear ubiquitously in formal descriptions of computer systems They arise for example in connection with non terminating programs or pro grams that terminate exceptionally and in situations where we are interested in the behaviour of a function only on some restricted set of argument values Partial functions also arise frequently in specification formalisms such as the Z notation 15 Partial functions arise because we want to declare functions using general recursive definitions which don t automatically guarantee totality So an important problem is to find a logic in which we can reason about these functions conveniently but safely This tu
10. a DOM f 1 k k41 Tn iii Other function applications are treated structurally Thus for e not of the form f e ep fork lt n Kee gt lt e gt m Ke gt 3In both these sets of axioms all atoms occurring in the pat are considered as free variables For simplicity we assume that the theorem prover is able to distinguish these from constants which may have the same name In applying these clauses to generate the axioms for the examples in Section 2 we have taken the liberty of optimising out a few redundant conjuncts One case deserves special mention if e is f the condition we obtain here is stricter than say termination of the corresponding ML program iv Case expressions are treated in a way which takes account of the flow of control within the expression Here for simplicity the patterns in a case construct are assumed to be non overlapping and exhaustive case e of py gt e pe gt ek gt lt e gt ll forall m p e gt gt lt e gt forall Zp pe e gt gt Ker where 7 stands for all the variables occurring in the pattern p v A variable binding expression is considered to terminate iff the body of the expression terminates for all values of the bound variable Thus Z lt OF 6 gt forall z Ke gt where Q is any binder i e forall exists fn any Note that this corres ponds to a very strict interpretation of the binders M
11. atica 21 251 269 1984 2 R S Boyer and J S Moore A Computational Logic ACM Monograph Series Academic Press 1979 3 J H Cheng and C B Jones On the usability of logics which handle partial functions In C Morgan and J Woodcock eds Proceedings of the Third Refinement Workshop Springer Verlag 1990 4 S Finn and M P Fourman Logic Manual for the Lambda System Abstract Hardware Limited version 3 2 1990 5 S Finn and M P Fourman Logic Manual for the Lambda System Abstract Hardware Limited version 4 2 1 1992 6 W M Farmer A Partial Functions Version of Church s Simple Theory of Types Journal of Symbolic Logic 55 3 1269 1291 1990 21 7 12 13 14 15 M J C Gordon HOL A proof generating system for higher order logic In G Birtwistle and P A Subrahmanyam eds VLSI Specification Verification and Synthesis 73 128 Kluwer Academic Publishers 1987 M Gordon R Milner and C Wadsworth Edinburgh LCF Volume 78 of Lecture Notes in Computer Science Springer Verlag 1979 C B Jones Systematic Software Development Using VDM Prentice Hall International 1986 C B Jones et al eds Mural A Formal Development Support System Springer Verlag 1991 Z Luo and R Pollack LEGO proof development system User s manual LFCS Report Series ECS LFCS 92 211 Department of Computer Science University of Edinburgh 1992 S Owre J Rushby et al Formal
12. d as having no value In particular the role of the DOM predic ates in our system is purely auxiliary we introduce them to provide a formal means for reasoning about the values of function calls It is tempting but mis leading to think of them expressing definedness DOM g x really only means the function J obeys its defining equation for the value x In our final example g x x f x independently of whether we can prove anything about f x We have described the details of our scheme as it has been implemented in the LAMBDA theorem prover However as we discussed in Section 3 variants of the scheme are certainly possible in particular there is scope for variation in our definition of the syntactic operator lt _ gt gt It seems that there amay be other definitions that avoid some of the above problems in particular the over definedness phenomenon mentioned above For such alternative definitions we expect to obtain metatheorems guaranteeing certain relationships between our logic and the behaviour of programs in Standard ML We have not yet worked out all the details however and it is not yet clear to us what the trade offs are between competing definitions of lt _ gt References 1 H Barringer J H Cheng and C B Jones because we chose to use equality rather than implication in our axiomatisation of DOM predicates f in sec tion 3 A logic covering undefinedness in program proofs Acta Inform
13. di f f as follows fun diff 0 y y diff Sx S y diff xy Our scheme then gives the more immediately useful axioms diff Oy y diff Sx Sy diff xy Because we use primitive recursion all DOM predicates can be optimised away automatically The DOM predicate does duty for the E predicate of LPE for instance and in the case of a genuinely partial function we would still expect to have to spend time propagating and discharging DOM conditions Notice the gains however for total functions we can prove totality once for all and then forget about the DOM predicates as above and even for partial functions we only need the DOM predic ates for reasoning that depends specifically on the value of a function application Thus for instance we can prove the theorem forall x P x P f 0 without mentioning the predicate DOM f at all Moreover we have retained the familiarity and simplicity of two valued classical logic For a discussion of some possible drawbacks of our approach see Section 5 3 3 Axiomatising partial functions In this section we describe in detail the general procedure whereby the axiomat isation of a function can be derived syntactically from its declaration we want the theorem prover to be able to do this automatically We here assume that as in HOL or LAMBDA we are reasoning only about non empty well founded datatypes which may be modelled semantically as free algebras thus we exclude f
14. dressed to the logician who seeks assurance that the scheme is logically consistent Furthermore such a semantics helps to clarify the intended meaning of the function definitions and provides reassurance that the axioms say the things one would expect In Section 5 we mention some advantages subtleties and potential pitfalls associated with our scheme The authors would like to thank Matt Fairtlough and Wesley Phoa for their valuable input during discussions on this work and Cliff Jones for his perceptive and helpful comments 2 Examples We begin with some concrete examples These should convey the basic ideas and should help to motivate the more technical discussions of Sections 3 and 4 Our goal is to show how general function definitions can be incorporated into a theorem prover for classical higher order logic For the kind of theorem prover we have in mind a user may enter a function declaration and the system will respond by introducing logical theorems or rules axiomatising its behaviour Prim itive recursive functions are unproblematic we can introduce a function constant satisfying the recursion equations Consider the following definition of the sorting function quicksort fun quicksort quicksort h t case partition h t of before after gt quicksort before h quicksort after Here we are assuming that we have already defined a suitable function partition this is primitive recursive and
15. e we write u v in place of the expression true ifu v false otherwise 10 4 2 Interpretation of terms We will define the interpretation of a term e in an environment E that is a finite function that assigns interpretations to all the constants and free variables appearing in e For convenience we assume here that our logic is explicitly typed all constants and free variables have some specific type and all variable bindings carry explicit type annotations We say that an environment F is well typed if for all z dom E we have E x t where t is the type of z In fact for the interpretation of function definitions we need both an envir onment E and a function environment F whose role is explained in Section 4 3 We use the notation te ed ee esv to mean v is the interpretation of e in environment E and function environment F This notation allows us to present the semantics in an operational style by means of inference rules The following rules define interpretations for all well typed expressions other than those occurring as part of a function definition Note that F plays no active role in any of these rules G BAe ey Sn n 0 1 2 where 7 is the numeral for n Similarly for the other basic types ii E F F x gt E x x dom E x dom F iii E F k esv Eek Pe sv E F H e e gt w v and similarly for the term constructors for other type forming operations iv E F
16. erpi gt DOM f paty patin for pragmatic reasons we want to use rewriting to eliminate DOM predicates There are many different ways in which lt _ gt could be defined depending on how we wished to interpret the phrase is guaranteed to terminate Firstly whether a given call terminates might depend on semantic choices for instance on whether we are thinking of call by name or call by value semantics Secondly we must decide how to interpret termination for non executable logical con structs such as quantifiers Finally we do not insist that the DOM predicate repres ents a necessary condition for termination we thus have some freedom in deciding how much of the termination behaviour we want to capture We discuss this point more fully in Section 5 3 The definition below illustrates one way of responding to these issues However the same idea applies to other variants and indeed to logical constructs other than those we consider here We define the operator lt _ gt inductively on terms of our logic as follows i Atomic expressions other than occurrences of f always terminate Thus if x is any atom other than f aes TRUE ii For each occurrence of f we generate a call to DOM f If the occurrence of f is not fully applied then we introduce extra universally quantified variables for the missing arguments Thus for 0 lt k lt n f I Ek gt Kain Py Kea l forall span cls w
17. finedness premises Much time and effort may be expended in propagat ing and discharging these even when we are reasoning only about total func tions For instance in LPE there is a special existence predicate E and we need to prove that E t holds in order to deduce P t from Vx P x 2 In this article we discuss yet another approach one that combines the practical benefits of a familiar logic expressive flexibility and decidable type checking The basic idea is as follows we regard a function application f x as always defined but if x is outside the intended domain of f we will not be able to prove anything about its value In this case we may think of f x as an arbitrary or random value of the appropriate type There is an analogy here with the Hilbert choice operator familiar to users of HOL and LAMBDA as and any respectively if T is any inhabited type then ex 7T false represents an arbitrary value of type T Similarly in our treatment hd where hd takes the head of a list represents an arbitrary value of the appropriate type However this expression has the same logical status as any other expression hence for example the theorem hd 5 v hd 5 is provable even though neither hd 5 nor hd 45 is provable This approach to the semantics of partiality has been proposed previously by Abrial in the context of Z see 15 Section 4 3 Our goal in this paper is to develop this idea
18. fining these is to transform the declaration syntactically into a form that we call first order We say the declaration A is first order provided every occurrence of f in the exp is fully applied i e occurs at the head of some subexpression f e e A general declaration A may be translated into a first order one by eta expanding occurrences of f in the exp i e replacing every subexpression f e e 0 lt k lt n that is not itself an applicand by Giger ee pee an ecg rs oe eer We write A to denote the transformed declaration we also write erp for the translations of the exp Note that these depend implicitly on the atom f and the value of n We define the meaning of a general declaration to be the same as the meaning of its first order expansion A A For the rest of this subsection we will therefore assume that A is first order We now explain the role of the function environment F introduced earlier Let us write S s x x sn and T t suppose now that we are given a set theoretic partial function 0 S T We can regard 0 as an approximation to an uncurried form of f We express this intention by putting the pair f 0 in the function environment A function environment is thus a finite map taking function names to partial functions between the appropriate sets The idea is now to interpret f by 8 To do this we augment the inference rules of Section 4 2 with the rule T E F Re Sop
19. hence total and that we have managed to prove the following theorem partition ht before after length before lt length t length after lt length t Given the qui cksort definition the system will introduce a constant quicksort to denote the function defined plus an auxiliary predicate DOM qui cksort The expression DOM qui cksort x will be used to mean that x lies within the intended domain of qui cksort the declaration determines the value of quicksort x for such Xx or more loosely the function application quicksort Xx is guaranteed to terminate The system will then generate axioms stipulating that for arguments satisfying DOM qui cksort the function qui cksort obeys its defining clauses For arguments not satisfying DOM quicksort we say nothing about the result Each clause of the definition will in fact generate one axiom for qui ckSort and one for DOM qui cksort The first clause will generate the two axioms DOM quicksort quicksort DOM quicksort TRUE and the second clause will generate the axioms 1Throughout this paper we use an ML style syntax compatible with LAMBDA v 4 2 1 DOM quicksort h t quicksort h t case partition ht of before after gt quicksort before h quicksort after DOM quicksort h t forall before after before after partition h t gt gt DOM quicksort before DOM quicksort after In t
20. his particular case it so happens that the function we have defined is total the quicksort algorithm always terminates The above axioms together with the theorem for partition are enough to allow a user to prove the following theorem forall k DOM quicksort k Once we have proved this theorem we can use it to prune the above axioms so that we need never refer to the DOM predicate again We could also prove theorems asserting that the list returned by qui kS ort is indeed sorted or that the function quicksort is identical to the function defined by some other sorting algorithm forall k sorted quicksort k forall k quicksort k othersort k Of course we do not expect the machine to be able to deduce this automatically from the syntactic form of the declaration although there is scope for tactics to automate such reasoning for common patterns of recursion Our scheme also allows us to declare genuinely partial functions in exactly the same way For example declaring the difference function fun diff x y if x y then 0 else 1 diff x 1 y generates the axioms DOM diff x y diff x y a gt lt Il y then 0 else 1 diff x 1 y DOM diff x y x y false gt gt DOM diff x 1 y We can then prove that DOM diff x y x lt y and that x lt y x diff x y y Of course there are simpler ways to tackle this example A more experienced proof hacker might define
21. i d will behave as an identity function By contrast in our scheme the theorem id 1 1 is not provable although id 0 0 is The prob lem is that we cannot in general keep track of how a higher order function such as apply will choose to apply its argument To be safe we take in Section 3 ii the pessimistic view and universally quantify the missing arguments The res ulting i d is thus under defined relative to ML This example is artificial but similar remarks apply to the following natural code for summing the nodes of a labelled tree fun sumNodes Tree n ts n Sum map sumNodes ts We can strengthen such examples Consider fun hal 0 0 hal 1 1 hal 1 hal S S n S apply hal n hal is almost half In ML hal n will terminate for all even n However because in our axiomatisation of DOM predicates in section 3 we chose to use equality rather than implication we can prove that DOM hal x x 0 On the other hand a function application may provably have some concrete value in our scheme when the corresponding ML program diverges This is perhaps the more serious problem Consider for instance 20 X f x gx x Sead E pas Sees f x The resulting function g is over defined relative to ML we can prove the theorem g 0 0 even though g 0 diverges in ML These examples illustrate the differences between regarding f X as having an unknown value an
22. ired to prove theorems guaranteeing their totality We can incorporate subtyping into our type discipline given a partial func tion on some type T we can regard its domain as a subtype o of r Elements of o may then be construed also as elements of 7 This is the approach taken in the EHDM proof environment 13 12 This approach offers considerable expressive power though it has the disadvantage that our type system will become undecidable if the allowed function definitions are sufficiently gen eral In the EHDM system for instance the user sometimes has to discharge a proof obligation in order to show that a term is well typed We can incorporate the notion of partiality into the logic itself by using a logic that takes account of possibly non denoting terms Examples of such logics include e Scott s Logic of Computable Functions used as the basis of the LCF proof system 8 e the three valued Logic of Partial Functions LPF 1 used in VDM 9 and implemented in the Mural system 10 e the Logic of Partial Elements LPE 14 used in earlier versions of the LAMBDA theorem prover 4 e the partial functions version PF of Church s simple type theory used in the IMPS proof system 6 These logics are all very expressive and they all have in common the notion that only certain well formed terms or formulae are defined However in each of them some of the familiar logical rules are complicated by extra de
23. nedness conditions than proofs in other systems see Section 2 This suggests that proofs in our logic may be less time consuming The LAMBDA system incorporates this feature The axioms generated in this case are similar to the theorems generated by a HOL package 18 The gain stems from the fact that the DOM predicates do not feature at all in the rules of the pure logic they are no more than particular object level constants Of course users will still need to prove DOM conditions sometimes But the ana logy with termination of the corresponding program suggests a way in which automated assistance for proving DOM conditions might be provided at least for the executable fragment of the logic A machine could try to prove DOM f e by simulating the execution of f e if this terminated then the course of compu tation would yield a proof of DOM f e Even if e is not a concrete value but an expression containing variables it might still be possible to achieve a similar result by running the computation symbolically Of course this would give us at best a semi decision procedure since such a proof tactic would diverge if applied to an unprovable goal Also there are limitations to the analogy between DOM predicates and termination see below Nevertheless we feel that proof tactics along these lines might be of some benefit to users 5 3 Limitations of our scheme In Section 4 we gave a proof of the logical c
24. onsistency of our system However in practice we are interested in more than this we would like to know that there is a good fit between our formalism and the real world situations that we are using it to describe If this relationship has been misunderstood by the user theorems generated using the theorem prover may be misinterpreted as expressing false or unproven statements about the real world In this subsection we seek to explain more fully the intended use of our logic and to point out some of the possible pitfalls There are essentially two different ways in which partial function declarations can be understood as definitions of genuinely partial functions between the rel evant domains or as loose specifications of total functions Logics such as LPF 1 which has a three valued semantics fit well with the former interpretation whereas our scheme fits more comfortably with the latter as will be clear from the semantics we have given The distinction between these interpretations does not matter much to us if we adhere to the principle of writing function applications only in contexts where they are guarded by conditions ensuring their well definedness For instance the predicate y gt 0 true x divy 1 has the same truth value in our scheme as in LPF for any assignment of values to X and y It seems likely that there is a metatheorem asserting that the two interpretations agree for certain guarded
25. ore generous versions are also possible see Section 5 1 vi Other expressions are treated structurally we simply conjoin together the DOM calls from the various subexpressions For example lt lee gt lt exw Ke Note that clauses ii and iii embody the choice of applicative order call by value semantics The above scheme can be extended in an obvious way to cover mutually recursive functions each mutually recursive function call generates a call to the corresponding DOM predicate 4 Set theoretic semantics We now outline a semantics for our system As mentioned earlier there are at least two reasons for wanting to do this to establish the consistency of our scheme and to provide a framework for thinking about our functions and axioms in an intuitive way The consistency is by no means obvious there certainly are some logical principles that do apply to non terminating function calls and we might be worried that these might allow us to deduce more than we really intend in the case of some pathological function definition We prove that our system actually is consistent by interpreting our function definitions in some model and checking Exhaustiveness is not essential and is not required in the LAMBDA implementation We impose it since it simplifies our presentation of the semantics that the corresponding axioms are valid under this interpretation and that our rules of inference are sound Our model is ver
26. ppose here that D is an environment giving interpret ations for all the constants already in scope at the point of declaration of f Definition 4 Let F S T S T be defined as follows Given 0 S T and v1 Un E S define FO v1 Un w iff for some clause f pati patin exp in A wherel lt i lt m and some environment E with dom E FV pati Patin we have a pati ze v for each 1 lt j lt n and moreover b DE f 0 F exp gt w Note that in the above definition the value of i is necessarily unique since the pat terns are non overlapping We think of E here as the environment generated by the pattern matching pattern matching process determines uniquely for the free algebras we use to model datatypes Given this it follows from Proposition 3 i that w if it exists is unique Proposition 5 i If 8 CO then FO C FO where C is the inclusion ordering on S gt T ii F has a least fixed point 05 Fha Proof i follows immediately from Definition 4 and Proposition 3 iii ii is then an application of Tarski s fixed point theorem Note that since S T is not a complete lattice we need to use transfinite iteration to construct the least fixed point Note also that iteration up to w will not in general suffice because of the presence of the infinitary rules O Definition 6 Suppose the declaration A is first order Then with 0 as above i let f be the c
27. reason about the value of the function call by using the corresponding clause of the definition By contrast if the function call does not terminate then it is not possible to reason about the value our semantics assigns an arbitrary value to the result This is how we avoid paradox in the case of functions such as fung xX g xt The axioms for f simply say that the function obeys its defining clause on all arguments for which it is known that the function call terminates for each 1 lt i lt m we have an axiom DOM f pati patin f pata patin exp t The axioms for DOM f give conditions on z1 n that are sufficient to guarantee that f z n will terminate To specify how the form of these axioms is determined we need to give a syntactic way of transforming an expression exp into a formula lt exp gt gt informally we think of lt exp gt gt as meaning the evaluation of exp is guaranteed to terminate We then take as our axioms for DOM f the equations This informal interpretation of DOM f is reasonable only when all calls to previously defined functions also terminate The semantics of Section 4 gives a precise interpretation for DOM f See Section 5 3 for further discussion of the differences between our DOM predicates and termination in Standard ML DOM f paty patin lt exp gt t for 1 lt i lt m We choose to use equality here rather than the implication
28. rns out to be surprisingly hard if x denotes a value outside the intended domain of a function f then the treatment of the term f x is problematic Several approaches to this problem have previously been proposed for a useful survey see 3 Abstract Hardware Limited Brunel Science Park Uxbridge Middx UB8 3PQ Laboratory for the Foundations of Computer Science University of Edinburgh EH9 3JZ This research was partially supported by SERC grant GR F31199 and SERC DTI grant GR F35890 The choice of a logic is a crucial issue in the design of mechanical theorem provers or proof assistants we would like a logic that satisfied the competing requirements of logical soundness expressive power and ease of reasoning The logics used in existing theorem provers exhibit various strengths and weaknesses and display a range of attitudes towards the problem of partial functions For example i iii We can restrict ourselves to reasoning about total functions and so ignore the problem completely In the HOL system 7 for instance only primitive recursive definitions are allowed a function declaration will thus be legal only if it can be shown by a simple syntactic check to define a total func tion This certainly makes the logic simple but we might hope for greater expressive power Some other theorem provers such as the Boyer Moore 2 and LEGO 11 systems allow more general function definitions but the user is requ
29. rom consideration certain ML types such as datatype d Dofd gt d Suppose the general form of a legal function declaration to be fun f paty pati exp f pata paton expe f patm patmn e pm where the pat are ML style patterns which may contain variables and the exp are expressions of higher order logic There is no notion of sequential execution here so the order of the clauses should not matter hence we stipulate that no two clauses may possess overlapping patterns However we do not require that the patterns should be exhaustive Moreover there is no restriction on the ways in which f can occur in the exp This is in contrast to primitive recursion for instance where f may only take arguments that are syntactically smaller than the corresponding LHS patterns We permit all partial recursive function definitions Given a declaration of this form we introduce an auxiliary predicate DOM f We then use each of the m clauses of the definition to produce one axiom for f and one axiom for DOM f We can think of DOM f 2 2 as meaning very roughly that the function application f 2z 2 is guaranteed to terminate A better intuition is that the DOM predicate characterises those arguments for which the value of the function is determined Our axiomatisation of f is incomplete in that we say nothing about the values of the function for other arguments Providing the predicate DOM f holds we can
30. tation If in the semantics of Section 4 we allowed any z e z r to have a value when not all e x 7 were defined then this value might change as the recursion unwound and new values of e arrived This would cause the operator F to be non monotonic and we would not be able to obtain a fixed point Hence although the following function definition is legal in our scheme we cannot prove it defines the identity function even though the identity is the only total function satisfying its two clauses fun f 0 0 f S n any x f x n 1 There are other uses of any in function definitions that behave more as one would expect For instance the reader is invited to check that the following function can be shown to be the identity fun id 0 0 id S n any x idn lt x true x lt Sn true 5 2 Advantages of our scheme As mentioned in Section 2 one advantage of our approach is that it does not impose unnecessary proof obligations on users who wish to work only with total functions Once we have proved a theorem asserting totality of a function we can forget about the DOM predicates completely Indeed if our theorem prover detects that some function definition is primitive recursive for instance the DOM predic ates need not even be generated and simpler forms of the axioms will suffice Moreover even when reasoning about non total functions it seems that proofs in our logic involve fewer defi
31. to give a semantics for recursively defined functions and to show how such functions can be axiomatised within a conventional classical logic Our motivation is pragmatic rather than philosophical our aim is not to offer the most satisfactory ontology of partial terms but to address some of the issues that arise in the implementation and use of theorem provers We believe our approach has several practical advantages over the others outlined above The rest of the article is structured as follows In Section 2 we introduce the basic idea with the help of examples and illustrate the kind of reasoning that our scheme supports This section presents the scheme as it would appear to the user of a theorem prover Such a user should also be aware of the limitations highlighted in Section 5 In Section 3 we give the formal details of how given a general partial function definition we may syntactically generate logical rules to axiomatise a total extension of the function From a formalist point of view such axioms specify the meaning of the function definition in that they determine pre cisely what can and cannot be proved about the function This section contains what the builder of a theorem prover would need to know in order to implement our scheme which has been implemented in LAMBDA theorem prover 5 In Section 4 we present a naive and intuitive set theoretic semantics for our func tion definitions and axioms This section is ad
32. urried form of any total function S T extending 0 0 ii let DOM f S bool be the characteristic function of dom Ox 14 Note that we have used only the graph ordering on T rather than any sophisticated domain ordering Furthermore we have not used any notion of continuity indeed the operator F will not in general be continuous 4 4 Validity of axioms We must now check that the axioms discussed in Section 3 are valid under the interpretation we have given Recall that for each 1 lt i lt m we have an axiom for f and an axiom t for DOM f We sketch the proofs that these are valid omitting some of the details We use identifiers such as A and 0 with the same meanings as in Section 4 3 Throughout this section F will denote the function environment f and D will denote the current environment at the point of declaration We begin by restricting our attention to first order declarations later we show that the results for the general case may be reduced to those for the first order case The axioms for f are easily shown to be valid Proposition 7 Suppose A is first order Then the axioms DOM f pata patin f pata patin exp t forf are valid under the given interpretations of f and DOM f Proof It is easily seen from the definitions of f and DOM f that 7 is valid iff for any environment F giving interpretations to the pattern variables we have pata llz
33. y elementary and purely set theoretic it allows us to think of a type simply as a set and a term of that type as a member of the set A function definition is then interpreted by just an ordinary function between sets the DOM predicate is modelled by the characteristic function of a subset of its domain In our view it is a virtue of our logic that it can be modelled without using any domain theory or category theory Our contention is that such a logic will be more easily grasped by a non specialist than a logic for which the models are necessarily mathematically abstruse 4 1 Interpretation of types The interpretation _ for the types of our logic is defined inductively as follows i The basic types are interpreted as sets in the obvious way e g bool true false nat 0 1 2 ii Function types are interpreted by set theoretic total function spaces t gt Lt le iii Product types are interpreted by cartesian products ee lx le Similarly for other ways of forming new non empty types sums quotients non empty subtypes etc iv Inductive datatypes are interpreted by sets constructed as free algebras we omit the easy details In fact we can allow any ways of defining types that have natural interpretations as non empty sets e g inductive types modulo equational constraints Henceforth we will identify the booleans with the truth values in our classical meta logic so that for instanc
Download Pdf Manuals
Related Search