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_inline1451 for tex2html_wrap_inline1453 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_inline1461 is a pf and tex2html_wrap_inline1463 and tex2html_wrap_inline1465 are gbfs, then tex2html_wrap_inline1467 is a gbf. If, in addition, tex2html_wrap_inline1463 and tex2html_wrap_inline1465 are pfs, so is tex2html_wrap_inline1473

The value of a gbf tex2html_wrap_inline1463 for given values (T, F or undefined) of the propositional variables will be T or F in case tex2html_wrap_inline1463 is a pf or a general variable otherwise. This value is determined for a gbf tex2html_wrap_inline1467 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_inline1489 and tex2html_wrap_inline1491 is given on the foregoing page.


According to the table, tex2html_wrap_inline1489 and tex2html_wrap_inline1491 are strongly equivalent.

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

Consider the table,


which proves that tex2html_wrap_inline1521 and tex2html_wrap_inline1523 are weakly equivalent. They are also strongly equivalent. We shall write tex2html_wrap_inline1525 and tex2html_wrap_inline1527 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_inline1529 and tex2html_wrap_inline1531 is the result of substituting any gbf for any variable in tex2html_wrap_inline1533 then tex2html_wrap_inline1535 This is called the rule of substitution.

2. If tex2html_wrap_inline1529 and tex2html_wrap_inline1463 is subexpression of tex2html_wrap_inline1243 and tex2html_wrap_inline1543 is the result of replacing an occurrence of tex2html_wrap_inline1463 in tex2html_wrap_inline1243 by an occurrence of tex2html_wrap_inline1465 , then tex2html_wrap_inline1551 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_inline769 be the variables of the gbf a taken in an arbitrary order. Then a can be transformed into the form


where each tex2html_wrap_inline1561 has the form


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


and each tex2html_wrap_inline1569 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_inline1577 cases of the truth or falsity of tex2html_wrap_inline769 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_inline1461 in tex2html_wrap_inline1467 consists of a single propositional variable.

2) The variable tex2html_wrap_inline761 is moved to the front by repeated application of axiom 8. There are three cases: tex2html_wrap_inline1587 to which axiom 8 is directly applicable; tex2html_wrap_inline1589 where axiom 8 becomes applicable after axiom 1 is used to make it tex2html_wrap_inline1591 the case tex2html_wrap_inline1593 which is handled in a manner similar to that of case 2.

Once the main expression has the form tex2html_wrap_inline1595 we move any tex2html_wrap_inline761 's which occur in tex2html_wrap_inline1463 and tex2html_wrap_inline1465 to the front and eliminate them using axioms 5 and 6. We then bring tex2html_wrap_inline1603 to the front of tex2html_wrap_inline1463 and tex2html_wrap_inline1465 using axiom 1 if necessary to guarantee at least one occurrence of tex2html_wrap_inline1603 in each of tex2html_wrap_inline1463 and tex2html_wrap_inline1465 . 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_inline1595 , where tex2html_wrap_inline1463 and tex2html_wrap_inline1465 do not contain tex2html_wrap_inline761 and are themselves in canonical form. However, the variable tex2html_wrap_inline761 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_inline1467 is defined to be either the first propositional variable or else an inevitable variable of both tex2html_wrap_inline1463 and tex2html_wrap_inline1465 . 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_inline1641 and put a in the form tex2html_wrap_inline1595 by using axiom 8.

3) The next step is to eliminate occurrences of tex2html_wrap_inline761 in tex2html_wrap_inline1463 and tex2html_wrap_inline1465 . 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_inline1653


(10) tex2html_wrap_inline1655

Suppose there is an occurrence of tex2html_wrap_inline761 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_inline761 until the objectionable tex2html_wrap_inline761 occurs as the inner tex2html_wrap_inline761 of one of the forms




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

Thus we have tex2html_wrap_inline1595 with tex2html_wrap_inline761 missing from tex2html_wrap_inline1463 and tex2html_wrap_inline1679

4) Inevitable variables are then brought to the front of tex2html_wrap_inline1463 and tex2html_wrap_inline1465 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_inline1463 is an occurrence of a subexpression of an expression tex2html_wrap_inline1465 . We define a certain propositional expression tex2html_wrap_inline1461 called the premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1465 as follows:

1) The premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1463 is T

2) The premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1725 where tex2html_wrap_inline1463 is part of tex2html_wrap_inline565 is the premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1733

3) If tex2html_wrap_inline1463 occurs in tex2html_wrap_inline763 and the premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline815 is tex2html_wrap_inline1461 , then the premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1747 is tex2html_wrap_inline1749

4) If tex2html_wrap_inline1463 occurs in tex2html_wrap_inline1753 and the premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1753 is tex2html_wrap_inline1461 , then the premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1747 is tex2html_wrap_inline1765

The extension of the rule of replacement is that an occurrence of tex2html_wrap_inline1463 in tex2html_wrap_inline1465 may be replaced by tex2html_wrap_inline1771 if tex2html_wrap_inline1773 where tex2html_wrap_inline1461 is the premiss of tex2html_wrap_inline1463 in tex2html_wrap_inline1465 . 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 20:03:21 PDT 1996