3/5/101Albert R Meyer, March 5, 2010 Mathematics for Computer Science MIT 6.042J/18.062J State Machines: Derived Variables lec 5F.1 Albert R Meyer, March 5, 2010 Euclidean Algorithm --for GCD(a, b) 1.x ::= a, y ::= b. 2.If y = 0, return x & terminate; 3.else simultaneously: (x, y) := (y, rem(x,y)) 4.Go to step 2. lec 5F.2 Albert R Meyer, March 5, 2010 GCD correctness Example: GCD(662,414) = GCD(414, 248) since rem(662,414) = 248 = GCD(248, 166) since rem(414,248) = 166 = GCD(166, 82) since rem(248,166) = 82 = GCD(82, 2) since rem(166,82) = 2 = GCD(2, 0) since rem(82,2) = 0 return value: 2 lec 5F.3 Albert R Meyer, March 5, 2010 Euclid Algorithm State Machine States ::= start ::= (a,b) state transitions defined by (x,y) (y, rem(x,y)) for y 0 lec 5F.4 Albert R Meyer, March 5, 2010 GCD correctness preserved invariant P(x,y): [gcd(a,b) = gcd(x,y)] lec 5F.5 Albert R Meyer, March 5, 2010 transitions: (x, y) (y, rem(x, y)) Proof: x = qy + rem. any divisor of 2 of these 3 terms divides all 3. P is preserved because: gcd(x,y) = gcd(y, rem(x,y)) for y 0 GCD correctness lec 5F.6 3/5/102Albert R Meyer, March 5, 2010 GCD correctness P is true at start: x = a , y = b, so P(start) [gcd(a,b) = gcd(a,b)]lec 5F.7 Albert R Meyer, March 5, 2010 GCD correctness Conclusion: on termination x = gcd(a,b) Proof: at termination, y = 0, so x = gcd(x,0) = gcd(x,y) = gcd(a,b) preserved invariant lec 5F.8 Albert R Meyer, March 5, 2010 GCD Termination y decreases at each step (another invariant) Well Ordering implies reaches minimum & stops y N lec 5F.9 Albert R Meyer, March 5, 2010 Derived Variables A derived variable, v, is a function assigning a “value” to each state: v: States → Values If Vals = , say v is “ -valued” or “nonnegative-integer-valued”lec 5F.10 Albert R Meyer, March 5, 2010 Robot on the grid example: States = 2. Define the sum-value, , of a state: (x,y) ::= x+y an -valued derived variable lec 5F.11 Derived Variables Albert R Meyer, March 5, 2010 Called derived to distinguish from actual variables that appear in a program. For robot Actual: x, y Derived: lec 5F.12 Derived Variables 3/5/103Albert R Meyer, March 5, 2010 Another derived variable: ::= (mod 2) is {0,1}-valued lec 5F.13 Derived Variables Albert R Meyer, March 5, 2010 For GCD, have (actual) variables x, y. Proof of GCD termination: y is strictly decreasing & natural number-valued lec 5F.14 Derived Variables Albert R Meyer, March 5, 2010 Derived Variables Termination followed by Well Ordering Principle: y must take a least value. then the algorithm is stuck lec 5F.15 Albert R Meyer, March 5, 2010 Strictly Decreasing Variable State 16 12 8 4 0 Goes down at every step lec 5F.16 Albert R Meyer, March 5, 2010 Weakly Decreasing Variable State Down or constant after each step lec 5F.17 16 12 8 4 0 Albert R Meyer, March 5, 2010 Diagonal Robot variables : up & down all over the place neither increasing nor decreasing : is constant both weakly increasing & weakly decreasing lec 5F.18 3/5/104Albert R Meyer, March 5, 2010 Partial-order valued variables Defs of increasing/decreasing variables extend to variables with partially ordered values. lec 5F.22 Albert R Meyer, March 5, 2010 Team Problems Problems 13 lec 5F.25 MIT OpenCourseWare http://ocw.mit.edu 6.042J /18.062J Mathematics for Computer Science Spring 2010 For information about citing these materials or our Terms of Use, visit: http://ocw.mit.edu/terms.