next up previous
Next: Recursion Induction Up: Properties of Computable Functions Previous: Properties of Computable Functions

Formal Properties of Conditional Forms


The theory of conditional expressions corresponds to analysis by cases in mathematics and is only a mild generalization of propositional calculus.

We start by considering expressions called generalized Boolean forms (gbf) formed as follows:

1. Variables are divided into propositional variables p, q, r, etc. and general variables x, y, z, etc.

2. We shall write tex2html_wrap_inline3536 for tex2html_wrap_inline3538 is called an elementary conditional form (ecf) of which p, x, and y are called the premiss, conclusion and the alternative, respectively.gif

3. A variable is a gbf, and if it is a propositional variable it is called a propositional form (pf).

4. If tex2html_wrap_inline3546 is a pf and tex2html_wrap_inline3548 and tex2html_wrap_inline3550 are gbfs, then tex2html_wrap_inline3552 is a gbf. If, in addition, tex2html_wrap_inline3548 and tex2html_wrap_inline3550 are pfs, so is tex2html_wrap_inline1526

The value of a gbf tex2html_wrap_inline3548 for given values (T, F or undefined) of the propositional variables will be T or F in case tex2html_wrap_inline3548 is a pf or a general variable otherwise. This value is determined for a gbf tex2html_wrap_inline3552 according to the table


We shall say that two gbfs are strongly equivalent if they have the same value for all values of the propositional variables in them including the case of undefined propositional variables. They are weakly equivalent if they have the same values for all values of the propositional variables when these are restricted to F and T.

The equivalence of gbfs can be tested by a method of truth tables identical to that of propositional calculus. The table for tex2html_wrap_inline3574 and tex2html_wrap_inline3590 is given on the foregoing page.

According to the table, tex2html_wrap_inline3574 and tex2html_wrap_inline3590 are strongly equivalent.

For weak equivalence the u case can be left out of the table.

Consider the table,


which proves that tex2html_wrap_inline3606 and tex2html_wrap_inline3608 are weakly equivalent. They are also strongly equivalent. We shall write tex2html_wrap_inline3610 and tex2html_wrap_inline3612 for the relations of strong and weak equivalence.

There are two rules whereby an equivalence can be used to generate other equivalences.

1. If tex2html_wrap_inline3614 and tex2html_wrap_inline3616 is the result of substituting any gbf for any variable in tex2html_wrap_inline3618 then tex2html_wrap_inline3620 This is called the rule of substitution.

2. If tex2html_wrap_inline3614 and tex2html_wrap_inline3548 is subexpression of tex2html_wrap_inline3328 and tex2html_wrap_inline3628 is the result of replacing an occurrence of tex2html_wrap_inline3548 in tex2html_wrap_inline3328 by an occurrence of tex2html_wrap_inline3550 , then tex2html_wrap_inline3636 This is called the rule of replacement.

These rules are applicable to either strong or weak equivalence and in fact to much more general situations.

Weak equivalence corresponds more closely to equivalence of truth functions in propositional calculus than does strong equivalence.

Consider the equations


All are strong equivalence except the first, and all can be proved by truth tables.

These eight equations can be used as axioms to transform any gbf into any weakly equivalent one using substitution and replacement.

In fact, they can be used to transform any gbf into a canonical form. This canonical form is the following. Let tex2html_wrap_inline2862 be the variables of the gbf a taken in an arbitrary order. Then a can be transformed into the form


where each tex2html_wrap_inline3646 has the form


and in general for each k = 1,...,n-1


and each tex2html_wrap_inline1622 is a truth value or a general variable.

For example, the canonical form of


with the variables taken in the order r, q, p is


In this canonical form, the 2 tex2html_wrap_inline3662 cases of the truth or falsity of tex2html_wrap_inline2862 are explicitly exhibited.

An expression may be transformed into canonical form as follows:

1) Axiom 7 is used repeatedly until in every subexpression the tex2html_wrap_inline3546 in tex2html_wrap_inline3552 consists of a single propositional variable.

2) The variable tex2html_wrap_inline2854 is moved to the front by repeated application of axiom 8. There are three cases: tex2html_wrap_inline3672 to which axiom 8 is directly applicable; tex2html_wrap_inline3674 where axiom 8 becomes applicable after axiom 1 is used to make it tex2html_wrap_inline3676 the case tex2html_wrap_inline3678 which is handled in a manner similar to that of case 2.

Once the main expression has the form tex2html_wrap_inline3702 we move any tex2html_wrap_inline2854 's which occur in tex2html_wrap_inline3548 and tex2html_wrap_inline3550 to the front and eliminate them using axioms 5 and 6. We then bring tex2html_wrap_inline3688 to the front of tex2html_wrap_inline3548 and tex2html_wrap_inline3550 using axiom 1 if necessary to guarantee at least one occurrence of tex2html_wrap_inline3688 in each of tex2html_wrap_inline3548 and tex2html_wrap_inline3550 . The process is continued until the canonical form is achieved.

There is also a canonical form for strong equivalence. Any gbf a is strongly equivalent to one of the form tex2html_wrap_inline3702 , where tex2html_wrap_inline3548 and tex2html_wrap_inline3550 do not contain tex2html_wrap_inline2854 and are themselves in canonical form. However, the variable tex2html_wrap_inline2854 may not be chosen arbitrarily but must be an inevitable propositional variable of the original gbf and can be chosen to be any inevitable variable. An inevitable variable of a gbf tex2html_wrap_inline3552 is defined to be either the first propositional variable or else an inevitable variable of both tex2html_wrap_inline3548 and tex2html_wrap_inline3550 . Thus p and q are the inevitable variables of


A gbf a may be put in strong canonical form as follows:

1) Use axiom 7 to get all premisses as propositional variables.

2) Choose any inevitable variable, say tex2html_wrap_inline3726 and put a in the form tex2html_wrap_inline3702 by using axiom 8.

3) The next step is to eliminate occurrences of tex2html_wrap_inline2854 in tex2html_wrap_inline3548 and tex2html_wrap_inline3550 . This can be done by the general rule that in any ecf occurrences of the premiss in the conclusion can be replaced by T and occurrences in the alternative by F. However, if we wish to use substitution and replacement on formulas we need the additional axioms

(9) tex2html_wrap_inline3738


(10) tex2html_wrap_inline3740

Suppose there is an occurrence of tex2html_wrap_inline2854 in the conclusion; we want to replace it by T. To do this, we use axioms 9 and 10 to move in a tex2html_wrap_inline2854 until the objectionable tex2html_wrap_inline2854 occurs as the inner tex2html_wrap_inline2854 of one of the forms




In either case, the objectionable tex2html_wrap_inline2854 can be removed by axiom 5 or 6, and the tex2html_wrap_inline2854 's that were moved in can be moved out again.

Thus we have tex2html_wrap_inline3702 with tex2html_wrap_inline2854 missing from tex2html_wrap_inline3548 and tex2html_wrap_inline3764

4) Inevitable variables are then brought to the front of tex2html_wrap_inline3548 and tex2html_wrap_inline3550 and so forth.

Two gbfs are equivalent (weakly or strongly) if and only if they have the same (weak or strong) canonical form. One way this is easy to prove; if two gbfs have the same canonical form they can be transformed into each other via the canonical form. Suppose two gbfs have different weak canonical forms when the variables are taken in the same order. Then values can be chosen for the p's giving different values for the form proving non-equivalence. In the strong case, suppose that two gbfs do not have the same inevitable propositional variables. Let p be inevitable in a but not in b. Then if the other variables are assigned suitable values b will be defined with p undefined. However, a will be undefined since p is inevitable in a which proves non-equivalence. Therefore, strongly equivalent gbfs have the same inevitable variables, so let one of them be put in front of both gbfs. The process is then repeated in the conclusion and alternative etc.

The general conditional form


can be regarded as having the form


where u is a special undefined variable and their properties can be derived from those of gbf's.

The relation of functions to conditional forms is given by the distributive law


The rule of replacement can be extended in the case of conditional expressions. Suppose tex2html_wrap_inline3548 is an occurrence of a subexpression of an expression tex2html_wrap_inline3550 . We define a certain propositional expression tex2html_wrap_inline3546 called the premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3550 as follows:

1) The premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3548 is T

2) The premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3810 where tex2html_wrap_inline3548 is part of tex2html_wrap_inline2652 is the premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3818

3) If tex2html_wrap_inline3548 occurs in tex2html_wrap_inline2856 and the premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline2908 is tex2html_wrap_inline3546 , then the premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3832 is tex2html_wrap_inline1802

4) If tex2html_wrap_inline3548 occurs in tex2html_wrap_inline3838 and the premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3838 is tex2html_wrap_inline3546 , then the premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3832 is tex2html_wrap_inline1818

The extension of the rule of replacement is that an occurrence of tex2html_wrap_inline3548 in tex2html_wrap_inline3550 may be replaced by tex2html_wrap_inline3856 if tex2html_wrap_inline3858 where tex2html_wrap_inline3546 is the premiss of tex2html_wrap_inline3548 in tex2html_wrap_inline3550 . Thus in a subcase one needs only prove equivalence under the premiss of the subcase.

next up previous
Next: Recursion Induction Up: Properties of Computable Functions Previous: Properties of Computable Functions

John McCarthy
Wed May 1 17:18:52 PDT 1996