INFERENCE RULES
===============

Inference rules are a useful tool for expressing conditional knowledge in a variety of circumstances.  Inference rules look like this:

Hyp0 Hyp1 ...
-------------- (rule-name)
  Conclusion
    
The rule looks like a big fraction with the name of the rule next to the line.  Above the line are any number of logical statements, and below the line is only one statement.  The rule is read much like an implication from top to bottom:  If Hyp0, Hyp1, ... are all true, then Conclusion is true.

We can use inference rules to express data definitions.  Let's dust off the old LoN:

  LoN ::= nil | (cons Number LoN)

The data definition can be understood as defining a set of data called LoN.  The first clause says that nil is a member of the set (nil : LoN), and the second clause says that if n:Number and x:LoN, then (cons n x):LoN also.  We can express this using two inference rules:

--------- (nil-rule)
nil : LoN


n : Number   x : LoN
-------------------- (cons-rule)
  (cons n x) : LoN


The first rule, nil-rule, has no statements above the line:  this is okay.  That simply means that nil is a LoN, with no restrictions.  The second rule says that if n is a Number and x is a LoN, then (cons n x) is also a LoN.  

In general, to express a data definition using inference rules, we have one rule per clause.  If the clause uses structured data, then there will be one statement above the line per field of the structure.  In our example, `cons' creates structured data, and it has two fields.  Therefore we find two hypotheses above the line:  one that restricts the data that goes into the `car' field of the cons, and one that restricts the data that goes into the `cdr' field of the cons.  You can choose the names of the rules as you please, but a typical choice is to name each one after the constructor that appears in the corresponding clause of the data definition.

Here's another example:

  AE ::= Number | Symbol | (add AE AE) | (mul AE AE)

We'll need four rules.  The first clause is the name of a class of data.  It means that every Number is an AE.  The rule is:

n : Number
---------- (number-ae)
 n : AE

Similarly for Symbol:

s : Symbol
---------- (variable-ae)
 s : AE

add and mul create structured data with two fields, and so their rules each have two hypotheses.

e1 : AE  e2 : AE
---------------- (add-ae)
(add e1 e2) : AE


e1 : AE  e2 : AE
---------------- (mul-ae)
(mul e1 e2) : AE


So far our inference rules have expressed only set-membership knowledge.  But we can use them for other things too.  For example, our structural induction principle for LoN is:

If p?(nil)
   all x:LoN.[p?(x) -> all n:Number.p?((cons n x))]
then
   all x:LoN.p?(x)

The translation to an inference rule is straightforward. Just put the hypotheses above the line and the conclusion below:

p?(nil)   all x:LoN.[p?(x) -> all n:Number.p?((cons n x))]
---------------------------------------------------------- (LoN-induct)
                  all x:LoN.p?(x)

PREDICATES AND SETS
-------------------
Suppose we have a predicate p? : LoN -> Boolean.  Then we can define the set of all LoNs that satisfy it via the axiom of comprehension:

  S = {x | x:LoN and p?(x)}

This says that S contains all those lists x for which p?(x) holds.

Conversely, given any set S of LoNs we can define a predicate that produces true for members of S and false otherwise:

  ;; p? : LoN -> Boolean
  p?(x) = x:S

We can use this to reformulate the structural induction principle in terms of set membership.  Let's translate p?(x) to x:S in the LoN-induct rule:

nil:S  all x:LoN.[x:S  ->  all n:Number. (cons n x):S]
---------------------------------------------------------- (LoN-induct)
                   all x:LoN. x:S

Notice that the conclusion of this rule now expresses a subset relationship:  it says that every member of LoN is a member of S.  That's equivalent to saying that LoN is a subset of S.  So let's rewrite the rule again (using <= for subset):

nil:S  all x:LoN.[x:S  ->  all n:Number. (cons n x):S]
---------------------------------------------------------- (LoN-induct)
                     LoN <= S

There is one more fact we can exploit to simplify the LoN-induct rule.  If the set S we are given is known ahead of time to be a subset of LoN, then we have both S <= LoN and LoN <= S in the conclusion of the rule.  That means that LoN = S.  Since we started under the assumption that p? : LoN -> Boolean, we know that the elements that satisfy p? must all be LoNs.  

Let's refine the rule once more:

Given some subset S of LoN:

nil:S  all x:LoN.[x:S  ->  all n:Number. (cons n x):S]
---------------------------------------------------------- (LoN-induct)
                     LoN = S


Let's use this rule by redoing the proof for:

Theorem:  all xs,ys:LoN.(sum (append xs ys)) = (+ (sum xs) (sum ys)).
Proof:

Define S = 
 {xs | xs:LoN and all ys:LoN.(sum (append xs ys)) = (+ (sum xs) (sum ys))}.

S <= LoN due to the condition x:LoN, and S's members satisfy the property stated in the theorem.  We can use the LoN-induct rule to show that S is in fact equal to LoN.  That is, the subset of LoN whose members satisfy the property actually contains every LoN.

nil:S because nil:LoN and for any ys:LoN we have:
  (sum (append nil ys)) 
  = (sum ys)
  = (+ 0 (sum ys))
  = (+ (sum nil) (sum ys))
  (in other words, nil satisfies the property that defines S).

For the other case, assume x:S and take any ys:LoN and n:Number.  The assumption x:S means that x is a LoN that satisfies the equation in the definition of S:

  all ys. (sum (append x ys)) = (+ (sum x) (sum ys))

Now we calculate:

  (sum (append (cons n x) ys))
  = (sum (cons n (append x ys)))
  = (+ n (sum (append x ys))
  = (+ n (+ (sum x) (sum ys)))   [uses induction hyp x:S]
  = (+ (+ n (sum x)) (sum ys))
  = (+ (sum (cons n x)) (sum ys))

Obviously (cons n x):LoN, and since it satisfies the equation, (cons n x):S.

Thus we have LoN <= S and therefore LoN = S.
Q.E.D.

Pop quiz:  

Recall qsort:

;; select-<= : LoN Number -> LoN
;; Produce a list of numbers contained in xs that are all <= ub.
(defun select-<= (xs ub)
  (cond ((endp xs) nil)
        ((consp xs) (if (<= (car xs) ub)
                        (cons (car xs) (select-<= (cdr xs) ub))
                        (select-<= (cdr xs) ub)))))

;; select-> : LoN Number -> LoN
;; Produce a list of numbers contained in xs that are > ub.
(defun select-> (xs lb)
  (cond ((endp xs) nil)
        ((consp xs) (if (> (car xs) lb)
                        (cons (car xs) (select-> (cdr xs) lb))
                        (select-> (cdr xs) lb)))))

;; qsort : LoN -> LoN
;; Quickly sort the given list of numbers.
(defun qsort (xs)
  (cond ((endp xs) nil)
        ((consp xs)
         (let ((pivot (car xs)))
           (let ((smaller (select-<= (cdr xs) pivot))
                 (larger  (select->  (cdr xs) pivot)))
             (append (qsort smaller)
                     (list pivot)
                     (qsort larger)))))))

Puzzle:  Prove all xs:LoN.(qsort xs) = (isort xs)
         (where isort is insertion sort from HW 5).