Equational Reasoning
Equational Reasoning¶
Equational Reasoning is a method used in Proofs to explain how code works. We step through the code and describe what is happening at each step.
Equational Reasoning will be used as a component part of larger proofs. We will use it inside a larger proof to verify a function does what it is supposed to. In many cases, we will be using abstract values in the proof and reasoning about how the code works on them.
For now, we will just use Equational Reasoning to verify we understand the sequence of events that happen when executing.
There are three justifications that can be used.
Premise/Assume - We either start from a function call or assume a function call happened.
Evaluation of … - We evaluate a command that is built into the language.
Apply Definition of … - We replace a function call with it’s known definition.
The proof structure will match our deductive proofs. There will be line numbers on the left and justifications on the write. This proof is designed to be written in the source code of our file.
Let us return to our custom build length function. This time implemented as size.
(define (size L)
(if (null? L)
0
(+ 1 (size (rest L)))
)
)
We want to prove that (size '(1 2)) will return 2. The proof is given below.
;1. (size '(1 2)) ;Premise
;2. (if (null? '(1 2)) 0 (+ 1 (size (rest '(1 2))))) ;Apply Definition of size
;3. (if #f 0 (+ 1 (size (rest '(1 2))))) ;Evaluation of null predicate
;4. (+ 1 (size (rest '(1 2)))) ;Evaluation of if conditional
;5. (+ 1 (size '(2))) ;Evaluation of rest
;6. (+ 1 (if (null? '(2)) 0 (+ 1 (size (rest '(2)))))) ;Apply Definition of size
;7. (+ 1 (if #f 0 (+ 1 (size (rest '(2)))))) ;Evaluation of null predicate
;8. (+ 1 (+ 1 (size (rest '(2))))) ;Evaluation of if conditional
;9. (+ 1 (+ 1 (size '()))) ;Evaluation of rest
;10. (+ 1 (+ 1 (if (null? '()) 0 (+ 1 (size (rest '()))) ) )) ;Apply Definition of size
;11. (+ 1 (+ 1 (if #t 0 (+ 1 (size (rest '())))))) ;Evaluation of null predicate
;12. (+ 1 (+ 1 0)) ;Evaluation of if conditional
;13. (+ 1 1) ;Evaluation of Addition
;14. 2 ;Evaluation of Addition
By walking through the code in this manner, we provide a pen and paper justification that it does what we want.
There are a few rules of thumb related to the apply and evaluation justifications.
For application, we only use it on functions we have defined. Additionally, it should only be functions we want to prove something about. If a return value has already been proven elsewhere, we could just reference that proof. We could say evaluation of function as seen in proof …. You want your justifications to read well. So, there is a little flexibility. You could write Apply length, apply definition of length, or App. Def. Length. Just make sure you state that it is an application and the name of the function you are applying.
In short, application means “replace a function call with its body”. We copy in the body of the function and replace the parameters with their values. Evaluation means to evaluate a built in. We don’t know how the code works because it came with Racket. We just predict what the return value will be based on our knowledge of the language.
For evaluation, you may only evaluate one type of operator per line. You cannot evaluate a subtraction and an addition on the same line. You could evaluate two subtraction commands on the same line. This can be shortened to Evaluate Operator or Eval. Operator. You must state the operator you are evaluating.
The following function defines Euclid’s classic algorithm to find the greatest common divisor. We prove that (gcd 48 24) returns 24.
(define (gcd a b)
(if (= 0 b)
a
(gcd b (remainder a b))))
The proof is given below.
;1. (gcd 48 24) ;Premise
;2. (if (= 0 24) 48 (gcd 24 (remainder 48 24))) ;Apply Def. gcd
;3. (if #f 48 (gcd 24 (remainder 48 24))) ;Evaluate Equals
;4. (gcd 24 (remainder 48 24)) ;Evaluate If
;5. (gcd 24 0) ;Evaluate Remainder
;6. (if (= 0 0) 24 (gcd 0 (remainder 24 0))) ;Apply Def. gcd
;7. (if #t 24 (gcd 0 (remainder 24 0))) ;Evaluate Equals
;8. 24 ;Evaluate If
Note
Sometimes proofs will get to long to reasonably fit on one line. You may break up a command over multiple lines and tab it over. You may also use an ellipsis … over parts of the code that are not relevant to the current line of the proof.
Equational Reasoning isn’t that powerful on its own. It just traces how the code executes. It becomes powerful when used with other proof techniques like contradiction and subproofs.