# Behavioral Equivalence Today we will do proofs with behavioral equivalence and induction. ##### Exercise: double [&#10029;] Prove that for all integers `x`, `double x ~ 2*x`, where `double` is defined as follows: ``` let double n = n + n ``` &square; ##### Exercise: exp [&#10029;&#10029;] Prove that for all integers `a` and natural numbers `x`, `exp a x ~ a ** x`, where `**` denotes the mathematical operation of integer exponentiation (hence overloading the built-in `**` operator), and where `exp` is defined as follows: ``` let rec exp a x = if x = 0 then 1 else a*(exp a (x-1)) ``` Use the following as a template for your proof about `exp`: ``` Theorem: for all ints a, for all naturals x, exp a x ~ a ** x Proof: by induction on x Case: x=0 Show: TODO TODO Case: x=k+1, where k >= 0 Show: TODO IH: TODO TODO QED ``` &square; ##### Exercise: facti [&#10029;&#10029;] Prove that for all natural numbers n and for all ints p, `facti n p ~ n! * p`, where `facti` is defined as follows: ``` (* [facti n p] is [n! * p]. * The implementation is a tail-recursive (sometimes called *iterative*) * generalization of the usual recursive factorial function. * Precondition: n >= 0 *) let rec facti n p = if n = 0 then p else facti (n-1) (n*p) ``` Use the following as a template for your proof about `facti`. Note carefully how induction on `n` leaves `p` universally quantified&mdash;which you will need to finish the second case. ``` Theorem: for all naturals n, for all ints p, facti n p ~ n! * p Proof: by induction on n Case: n=0 Show: for all ints p, facti 0 p ~ 0! * p TODO Case: n=k+1, where k >= 0 Show: for all ints p, facti (k+1) p ~ (k+1)! * p IH: for all ints p, facti k p ~ k! * p TODO QED ``` &square; ##### Exercise: fact [&#10029;] Prove that for all natural numbers n, `fact n ~ n!`, where `fact` is defined as follows: ``` let fact n = facti n 1 ``` *Hint: use the previous theorem as a lemma.* &square; Let `fact` have the following *specification*: ``` (* precondition: n >= 0 *) (* postcondition: (fact n) = n! *) val fact : int -> int ``` You have proven the correctness of a tail-recursive implementation of the factorial function. Reflect on why that is so. ## Additional exercises ##### Exercise: sum_sqrs [&#10029;&#10029;] Prove that for all natural numbers n, `sum_sqrs n ~ (n * (n+1) * (2*n + 1))/6`, where `sum_sqrs` is defined as follows: ``` let rec sum_sqrs n = if n <= 0 then 0 else (n*n) + sum_sqrs(n-1) ``` &square; ##### Exercise: exp square [&#10029;&#10029;&#10029;&#10029;] The recursive implementation of `exp`, above, is inefficient. Implement [exponentiation by squaring][exp-square] in OCaml. Prove the correctness of your implementation. Use the proofs you did for `fact` as an inspiration. *Hint: recall strong induction (aka [complete induction][compl-ind]) from CS 2800.* [exp-square]: https://en.wikipedia.org/wiki/Exponentiation_by_squaring [compl-ind]: https://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction &square;