CS217 Day 2 Wednesday, March 29, 2000

Inductive Specification and Mathematical Induction

• A set S is said to be inductively specified if it is the smallest set such that
  1. S contains a certain set S₀.
  2. If certain elements are in S, then certain other elements are in S.

  For each n > 0, let Let S_n be the set of elements in S_n-1 together with the elements that must be in S by applying 2 to elements in S_n-1.

  Then S_n is a subset of S for n = 0, 1, ..., and S is the union of S₀, S₁, ... because this union is the smallest set satisfying conditions 1 and 2

  Things can be proved about inductively defined sets by Mathematical Induction.
  

• Principle of Mathematical Induction
  Let P(x) be a proposition about x, for x in an inductively defined set S. Then P(x) will be true for all x in S if
  1. (base case) P(x) is true for x in S₀, the elements in S by rule 1, and
  2. (inductive case) If elements in B are in S whenever elements in A are in S by rule 2, then P(x) is true for x in B whenever P(x) is true for all x in A.

  Proof.
  Suppose these conditions hold but P(z) is false for some z in S.
  There is a smallest n such that P(z) is false for some z in S_n.
  Let z be such an element for this smallest n.

  Then n > 0 because P(x) is true for all x in S₀ (base case).
  By definition of n, P(x) is true for all x in S_n-1.
  But then P(x) is true for all x in S_n (inductive case).
  

  But z is in S_n and P(z) is false.
  This contradiction implies P(x) must be true for all x in S.

Examples.

• list-of-numbers is defined by the BNF rules

  [list-of-numbers] ::= () | ([number] . [list-of-numbers])

  Then, with the above notation,
  

  S₀ = {()},
  S₁ = {()} union {(n . ()) | n is a number}
  S₂ = {()} union {(n . ()) | n is a number} union {(n . (m . ())) | n, m are numbers}}
  ...

  We can use the inductive definition of list-of-numbers to define a recognizer, list-of-numbers?

  (define list-of-numbers?
    (lambda (x)
      (if (null? x)
  	;; base case
  	#t
  	(if (pair? x)
  	    ;; inductive case
  	    (and (number? (car x))
  		 (list-of-numbers? (cdr x)))
  	    #f))))
  

  Then,

  (list-of-numbers? datum) => #t if datum is in list-of-numbers,
                           => #f, otherwise
  

  because, by mathematical induction, the result is #t in the base case where datum = () and in the inductive case where datum = (n . lon), when n is an integer and lon is in list-of-numbers, and the result is #f in all other cases.

• s-list, lists whose members are symbols or s-lists.

  [s-list]            ::= () | ([symbol-expression] . [s-list])
  [symbol-expression] ::= symbol | [s-list]
  

  The literal representation contains only symbols and parentheses.
  Recognizer for s-lists, s-list?

  (define s-list?
    (lambda (x)
      (or (null? x)
  	(and (pair? x)
  	     (or (symbol? (car x))
  		 (s-list? (car x)))
  	     (s-list? (cdr x))))))
  

  This procedure is correct by Mathematical Induction.
  (s-list? x) returns #t if x = () or if x is a pair whose cdr is a symbol or an s-list and whose cdr is an s-list, and #f otherwise. According to the BNF, this is exactly what has to be checked.

• binary-tree, binary trees with numerical leaves and symbols at interior nodes.

  [bintree] ::= [number] | ([symbol] [bintree] [bintree])
  

  E.g.,

  1
  (a 1 2)
  (a (b 1 (c 2)) 3)     -- not a binary-tree
  (a (b 1 (c 2 3)) 4)
  

  (binary-tree? x) => #t if x is a binary-tree, #f otherwise.

  (define binary-tree?
    (lambda (x)
      (if (number? x)
  	#t
  	(and (list? x)
  	     (= (length x) 3)
  	     (symbol? (car x))
  	     (binary-tree? (cadr x))
  	     (binary-tree? (caddr x))))))
  

  list? and length are built in.
  You can write correct definitions using the BNF for list.

  (leaf-sum bt) => the sum of the leaf values, if bt is a binary-tree.

  (define leaf-sum
    (lambda (tree)
      (if (number? tree)
  	tree
  	(+ (leaf-sum (cadr tree)) (leaf-sum (caddr tree))))))
  

  Trace of an example:

  > (trace leaf-sum)
  (leaf-sum)
  > (leaf-sum '(a (b 1 (c 2 3)) 4))
  |(leaf-sum (a (b 1 (c 2 3)) 4))
  | (leaf-sum (b 1 (c 2 3)))
  | |(leaf-sum 1)
  | |1
  | |(leaf-sum (c 2 3))
  | | (leaf-sum 2)
  | | 2
  | | (leaf-sum 3)
  | | 3
  | |5
  | 6
  | (leaf-sum 4)
  | 4
  |10
  10
  > 
  

• Simple lambda calculus expressions.

  [expression] ::= [identifier]
                 | ([lambda]([identifier]) [expression])
                 | ([expression] [expression])
  

  where [identifier] is any symbol but lambda.
  The three types are called
  • variable references
  • lambda expressions
  • applications
  This mini-language will be used to study lexical concepts of variables, such as scope, region, free, bound.

  A straight-forward expression recognizer:

  (define expression?
    (lambda (x)
      (cond ((and (symbol? x)
  		(not (eqv? x 'lambda)))
  	   #t)
  	  ((and (pair? x)
  		(eqv? (car x) 'lambda)
  		(list? x)
  		(= (length x) 3)
  		(let ((formals (cadr x))
  		      (body (caddr x)))
  		  (and (pair? formals)
  		       (symbol? (car formals))
  		       (null? (cdr formals))
  		       (expression? body))))
  	   #t)
  	  ((and (list? x)
  		(= (length x) 2)
  		(expression? (car x))
  		(expression? (cadr x)))
  	   #t)
  	  (else #f))))
  

• Code for above procedures and fib, fact: cs217.scm
• Code for possible test procedures: tests.scm

Read TSPL Ch2 and EOPL 1.2. Study the examples. Be able to prove them correct.
Review the kinds of Scheme expressions from Day 1.
set! special form has been added.
Continue work on Assignment 1.