Reasoning by Cases and the Formation of Conditional Programs

I Introduction

Reasoning by cases, a natural feature of human reasoning, has been difficult to formulate so that it can be performed naturally when needed. Several difficulties arise: (1) how to motivate the use of reasoning by cases when and only when needed, (2) how to determine an appropriate anal­ ysis of the goal into cases, and (3) how to carry out the deduction in each case and combine the results. On moti­ vating the use of reasoning by cases, we merely note that this type of reasoning is typically used only as a last resort since it multiplies the number of goals that need to be con­ sidered. Our main technical contributions in this paper are (1) a set of strategies that draw on the context of a deduc­ tion to provide an appropriate case analysis for a goal, and (2) inference rules for carrying out reasoning by cases and forming conditional terms for the existentially quantified variables in the initial goal.

We restrict our attention to goal formulas of the form

1 This research was supported in part by the Office of Naval Re­ search under Contract N00014-84-C-0473 and in part by the Defense Advanced Research Projects Agency Contract N00014-81-C-0582, monitered by the Office of Naval Research. The views and conclu­ sions contained in this paper are those of the author and should not be interpreted as representing the official policies, either expressed or implied of DARPA, ONR, or the US Government.

although the techniques presented are not necessarily lim­ ited to this type of goal. What is desired as an output of the deductive process is a way to construct an algorithm that computes a value for z as a function of the variables x1 , ... , Xn. We sometimes call ( 1) a problem specification and refer to x1 , ... , Xn as input variables and z as the output variable. When a reasoning by cases argument is needed to establish (1) then the corresponding algorithm has the form of a conditional, where each case corresponds to a branch of the conditional. That is, if (1) can be established by separately considering the cases Ct. ... , Cm then we want to be able to construct a conditional expression

where if ... fi is a functional version of Dijkstra's nondeter­ ministic conditional. The function f; computes a value for the output variable z corresponding to case C;. Predicate P;, called a guard, characterizes the conditions under which /; provides a solution to the initial problem specification.

Evidently, what is needed in order to form a conditional ex­ pression from a reasoning by cases argument is an analysis of the goal into cases C1 , ... , Cm and extraction of a guard P; and function /;from the proof of case C; for i = 1, ... , m. There are many ways to analyze a goal into cases. Such analysis is easy when the cases are explicitly in the initial goal. We present below several strategies for handling the more difficult situation in which the analysis depends on the context of a goal.

In the next section we review the notion of a system for deriving antecedents and present a few inference rules per­ tinent to reasoning by cases. In the succeeding section we analyze the notion of reasoning by cases into two general types and present several instances of these types, called strategies for reasoning by cases. The application of these strategies to a number of program synthesis tasks may be found in (Smith 1985a).

II Derived Antecedents

Reasoning by cases can be naturally accomplished in the framework of derived antecedents (Smith 1982,Smith 1985b). This framework allows a deduction whose aim is not lim­ ited to establishing the validity of a goal formula G, but more generally seeks to derive a formula A, called a de­ rived antecedent, satisfying certain constraints and such that A ==> G is valid. The constraint we are concerned with simply checks whether the free variables of a formula are a subset of some fixed set that depends on G. If G hap­ pens to be a valid formula in our current theory then the antecedent true should be derived - thus ordinary theorem­ proving is a special case of deriving antecedents.

A solution to a problem specification (1) is a tuple (A, a:} where a: is a term called the answer, and A, called the derived antecedent, is a formula whose free variables are a subset of { xb ... , xn} and such that, if we define the algo­ rithm F by F(xb ... , xn) = a:, then the formula

is valid. In other words a solution provides a term that computes a value for the existentially quantified variable as a function of the input variables xl> ... , Xn, but only under the additional assumption of the derived antecedent. The derived antecedent A is called the derived input condition of algorithm F.

In a natural deduction-like system the derivation of a solu­ tion for a goal G can be described by a two stage process. In the first stage reduction rules are repeatedly applied to goals reducing them to subgoals. A primitive rule is ap­ plied whenever possible. The result of this reduction pro­ cess can be envisioned as a goal tree in which 1) nodes represent goals/subgoals, 2) arcs represent reduction rule applications, and 3) leaf nodes represent goals to which a primitive rule has been applied. The second stage involves the bottom-up composition of solutions. Initially each ap­ plication of a primitive rule to a subgoal yields a solution. Subsequently whenever a solution has been found for each subgoal of a goal G then a solution is composed for G ac­ cording to the reduction rule employed. In a working sys­ tem we have developed, called RAINBOW, a single solution is selected from among the alternate derived solutions of a goal by maximizing over a heuristic measure of weakness and structural simplicity.

Solutions obtained by solving subgoals are composed to ob­ tain a solution for the parent goal. The reduction rules presented below require two composition methods: the dis­ junctive and conjunctive composition of solutions. The dis­ junctive composition of solutions (AI> a:1) and (A2, a:2) is

Intuitively, the disjunctive composition of solutions returns an answer which behaves like a:1 when A1 holds and be­ haves like 0:2 when A2 holds. If A1 or A2 is false then the conditional collapses to just a:2 or a:1 respectively. For ex­ ample, the disjunctive composition of solutions (a ~ b, a} and (b ~a, b) is

The conjunctive composition of solutions (AI> a:1} and (A2, a:2} is

where uc computes the unifying composition of substitu­ tions (Nilsson 1980). We do not elaborate on conjunctive composition since it does not play a central role in this paper.

Natural deduction-like systems for deriving solutions may be found in (Smith 1982,Smith 1985b). Here we merely list the inference rules necessary· to support reasoning by cases. Goals are prepared by treating the universally quantified variables as constants and then dropping all quantifiers. We use the notation ; where H = {h1, h2, ... ,h.~;} as an abbreviation of the formula h1 1\ h2 1\ ... 1\ h.~; ==> G.

Rule R2. Reduction of a disjunctive goal. If the goal formula has the form F-;G, then generate subgoals ~ and ; . If these subgoals return solutions (P, a:1) and ( Q, a:2} respectively, then return the disjunctive composition

as a solution to goal F-;G. Naturally if subgoal ~is explored first and a solution (true, a:1) is returned, then F has been proved and there is no need to explore ;. The solution (true, a:1) can be returned for F-;G .

Rule R2 assumes that the goal has only two disjuncts. The generalization to multiple disjuncts in this and later rules is straightforward.

Something like the following rule is commonly called the "case analysis" rule in many theorem-proving systems (see for example (Bledsoe 1977)).

Rule R3. Reduction by a disjunctive hypothesis. If P V Q is an axiom or hypothesis then reduce goal ; to sub­ goals J:P and J:Q where HR is a set of hypotheses obtained by limited forward inference on R and the set H 2 · If solu­ tions (AI> a:1} and (A2, a:2) are obtained for these subgoals respectively, then return their conjunctive composition as the solution to ; .

While this rule is sound, it often fails to find a solution when one exists. The solutions to the various cases typically have incompatible answers. The unifying composition operator simply reports that such answers are inconsistent. A better rule is the following.

2 I.e. Hn contains R and all hypotheses in H plus any interesting consequences of H and R deriveable within some bounded amount of computational resource.

Rule R4. Reduction by disjunctive hypothesis. If there is axiom or hypothesis P V Q then reduce goal ; to subgoals :;P and :: . If solutions (AI> o:1) and (A2, o:2) are obtained for these ~ubgoals respectively, then return their composition

as a solution to the goal ;.

III Strategies for Reasoning By Cases

The idea behind reasoning by cases is to treat a goal in a number of alternate contexts, or cases, that are collectively exhaustive. Often the difficulty in solving a goal is due to the fact that each case requires a different argument .

There are two identifiable types of reasoning by cases. In the first type, the goal G is reduced to a conjunction of weaker goals. This occurs for instance when we assume a disjunction P V ·P. The goal becomes P V -,p ==> G or equivalently (P ==> G) 1\ ( -,p ==> G) . Rules R3 and R4 can then be used to handle the cases. The second type of reasoning by cases involves reducing the goal G to a disjunction of stronger goals. This occurs for instance when we conjoin a disjunction P V -,p to the goal. The goal becomes G 1\ (P V ·P) or equivalently (G 1\ P) V (G 1\ ·P). Rule R2 can then be used to handle the cases.

Sometimes the motivation for performing a case analysis is intrinsic to the goal. Rules R2 and R4 can be used to carry out the reasoning by cases. Sometimes however, motivation for case analysis must come from context. To exploit con­ text in setting up a case analysis we use special procedures called strategies that have the effect of an inference rule but may involve arbitrary amounts of processing. Strategies are intended to encode in one deductive step a commonly oc­ curring reasoning pattern. We present several strategies for reasoning by cases below. They are described in terms of (i) a heuristic for determining when to apply reasoning by cases and with what cases, and (ii) a description of how cases are generated and how the solutions for these cases are composed. Omitted from the description of these strategies is the common heuristic that they be applied only as a last resort; that is, only if other means are not applicable or have failed.

Strategy RBCl. Exploiting an unverified subgoal.

Apply-when: A subgoal P of goal G cannot be easily ver­ ified and the variables of P are a subset of the input vari­ ables.

Procedure: Use rule R4 with assumption P V ·P.

The procedure part of RBCl should be viewed as descrip­ tive rather than prescriptive. We do not propose that RBCl form the disjunction P V -,p only to have rule R4 break it down. Rather, RBCl should directly create subgoals ::P and H:p and should compose the solutions to these sub­ goals as R4 would. Similar remarks hold for the following strategies.

A typical use of strategy RBCl occurs when term r in a conditional rewrite rule

matches term tin goal G(t) with unifier 6 but the condition CO cannot be verified. Strategy RBCl would apply rule R4 with CO v ·CO. Concrete examples of the use of a strategy like RBCl may be found in (Buchanan and Luckham 1974).

Strategy RBC2. Alternate ways to apply a conditional rewrite rule.

Apply-when: The goal has the form G(t) and there is a conditional rewrite rule

such that r matches t with several distinct unifiers. Suppose that there are only two such unifiers el and 62 and that eel and C02 are both verifiable.

Procedure: Use rule R2 after reducing G(t) to G(8)61 V G(8)62·

Strategy RBC3. Alternate forms of an input variable.

Apply-when: A set of terms can be constructed that de­ scribe the possible forms of an input. Suppose for exam­ ple that an input x of type D either has the form / 1 or !2(81(x),82(x)) where / 1 and / 2 are generators of typeD and 8 1 and 8 2 are selectors for /2.

Procedure: Use rule R4 with assumption x = / 1 V x = /2 ( 81 ( x), 8 2 (x)).

To support RBC3 each data type known to the system should have one or more inductive definitions in terms of a set of generators. These provide standard alternative struc­ tures for the values of the type. Since they are based on inductive definitions of the type, they prepare the way for an inductive proof of the initial goal.

Sometimes there is an input condition that restricts the set of values that a variable may vary over. A technique for creating a set of alternative forms taking into account an input condition is presented in (Smith 1985a).

Strategy RBC4. Alternate forms of a term for the output variable.

Apply-when: A set of terms can be constructed that de­ scribe the possible forms of the output. Suppose for exam­ ple that the output variable has type R and either has the form / 1 or f 2 (u,v).

Procedure: Use rule R2 after reducing goal G(z) to G(fl) V G(f2(u, v)) where u and v are fresh variables.

The previous strategies break a goal into cases that are determined before the cases are explored. They may be called a priori strategies. Our last strategy creates subgoals based on the solutions to previous subgoals and so may be called an a posteriori strategy.

Strategy RBC5. Handling an unsolved case.

Apply-when: Solution (AI> a 1) is produced for goal ~ but A1 is insufficiently weak or simple.

Procedure: Generate subgoal H G ; if solution (A2, a 2) is -Al produced then generate the solution

for~-

IV Concluding Remarks

A limited form of antecedent derivation is used by Bledsoe and Tyson (Bledsoe and Tyson 1977) to perform reason­ ing by cases on program variables during program verifica­ tion. The difficulty in getting rules like R3 to produce a satisfactory solution has stimulated a number of potential extensions, including the use of "conditional substitutions" (Nilsson 1980) and "generalized substitutions" (Tyson and Bledsoe 1979).

This paper is based on experience with the CYPRESS pro­ gram synthesis system (Smith 1985b). This system de­ pended on an antecedent deriver for all of its deduction and used strategies related to RBC3 and RBC4 for creating var­ ious divide-and-conquer algorithms, including the selection sort algorithm in Example 4. CYPRESS used a strategy re­ lated to RBC2 for creating composition and decomposition operators on various composite data types, including the decomposition operator derived in Example 3. We are cur­ rently constructing a new version of this system at Kestrel Institute. This new system not only includes special strate­ gies for constructing various classes of algorithms but can fall back on general purpose deductive program synthesis when these special methods fail.

One goal of this paper has been to explore the notion of rea­ soning by cases and to formulate the logical mechanisms needed to implement this type of reasoning in a natural way. The framework of derived antecedents supplements the ease with which a natural deduction-like system can motivate and introduce case analysis with essentially logical mechanisms for handling case structure and forming condi­ tional terms for existentially quantified variables. Although we have presented strategies for reasoning by cases in the context of a natural deduction-like system, we helieve these strategies can also usefully augment a resolution-based sys­ tem.

ACKNOWLEDGEMENTS

I would like to thank Allen Goldberg for his valuable com­ ments on a previous draft .