CS 345 slide 129 Spring 200522 February 2005Inductive proofs over listsTo prove P (xs) for any finite xs :: [ ]:Case P ([]) : Prove that P ([]) holds unconditionally.Case P (xs) P (x:xs): Prove thatif P (xs) holds for some xsthen P (x:xs) holds.Example: P (xs): len(xs++ys) = len xs + len ysCase P ([]): len([ ] ++ ys) = len[] + len ys len( [ ] ++ys) = len[ ] + len ys= {++.1, len.1}len ys = 0 + len ys={ arithmetic, reflexivity of = }TrueCase P (xs) P (x:xs):len((x:xs)++ ys) = len(x:xs) + len yslen((x:xs)++ ys)={ ++.2 }len(x:(xs++ ys))={ len.2 }1 + len(xs++ ys)={ induction hypothesis }1 + (len xs + len ys)={ + associative }(1 + len xs) + len ys={ len.2 }len(x:xs) + len ys CS 345 slide 130 Spring 200522 February 2005Example: Proof that (++) is associative— i.e., that forall lists xs, ys, and zs, P (xs): xs ++ (ys++zs) = (xs++ys) ++ zsThe proof, by induction on xs:Case P ([]): [ ] ++ (ys++zs) = ( [ ] ++ ys) ++ zs[] ++ (ys++zs) = ( [ ] ++ ys) ++ zs={ ++.1, twice }ys ++ zs = ys ++ zs={ reflexivity of = }TrueCase P (xs) P (x:xs): (x:xs) ++ (ys++zs) = ((x:xs)++ ys) ++ zs(x:xs) ++ (ys++zs)={ ++.2 }x : (xs ++ (ys++zs))={ induction hypothesis }x : ((xs++ ys) ++ zs)={ ++.2 }(x:(xs++ ys)) ++ zs={ ++.2 again }((x:xs)++ ys) ++ zs CS 345 slide 131 Spring 200522 February 2005Example: Double induction on Int and [a]Given definitions> take, drop :: Int -> [a] -> [a]> take 0 _ = [ ]> take _ [ ] = [ ]> take k (t:ts) | k>0 = t : take (k-1) ts> drop 0 vs = vs> drop _ [ ] = [ ]> drop k (_:vs) | k>0 = drop (k-1) vsprove P (n,xs): take n xs ++ drop n xs = xsProof: by induction on n and xsCase P (0,xs): take 0 xs ++ drop 0 xs = xstake 0 xs ++ drop 0 xs={ take.1, drop.1 }[ ] ++ xs={ ++.1 }xsCase P (n,[]):take n [ ] ++ drop n [ ] = [ ]take n [ ] ++ drop n [ ]={ take.2, drop.2 }[ ] ++ [ ]={ ++.1 }[]CS 345 slide 132 Spring 200522 February 2005Case P (n+1, x:xs):take (n+1) (x:xs) ++ drop (n+1) (x:xs) = (x:xs)take (n+1) (x:xs) ++ drop (n+1) (x:xs)={ take.3, drop.3 }(x : take n xs) ++ drop n xs={ ++.2 }x : (take n xs ++ drop n xs)={ induction hypothesis }x : xs Points to note: In these proofs• we have made heavy use of Haskell definitions asequations• this approach works only under conditions ofreferential transparencyCS 345 slide 133 Spring 200522 February 2005Programming with Assignment“Imperative” programming:0. expressions +1. update (= “assignment”) operation +2. explicit sequencing (= time-ordering) of operations(a.k.a. “control flow”).program state: central to all HL imperativelanguages.In a true expression:a variable’s value is constant throughout itsscope.but in an imperative program:a variable can be bound to different values atdifferent times (which correspond to differentpoints in its scope).State: the set of all of a program’s variable-valuebindings; commonly expressed as a function:state :: name value[This definition is a first approximation, soon to berefined.]CS 345 slide 134 Spring 200522 February 2005Imperative processing’s three (idealized) stages:0. input: create state0 from external data1. computation: transformstate0 state1 state2 … statei …until a desired condition on states is satisfied bysome staten 2. output: extract results from statenWhat users (and programmers) want isresults, not statesbut imperative languages force us to deal with states.So why do we continue to program imperatively?• habit and history: Imperative HLLs were thefirst to grow out of machine-oriented pro-gramming. The outlines of the underlyingmachine —memory, program counter, i/ofiles— are still visible.• efficiency: The closer correspondencebetween the imperative abstract machine andactual hardware makes efficient implementa-tions easier.CS 345 slide 135 Spring 200522 February 2005The Update Operation (imperative programming’s hallmark)The operationx := E assignment or updatebinds the value of E to variable x — replacing x’sformer value and thereby changing the program’sstate ( update initialize).Every variable has two kinds of values: R and L.In the statementx := y + 2• what matters about y is its R-value• what matters about x is its L-value.R-values (right-hand-side values):• data objects• contents of storage locationsL-values (left-hand-side values)• pointers• addresses of storage locationsConsequently, the mapping from variable-names tovalues actually has two parts:0. environment :: name location1. state :: location R-valueCS 345 slide 136 Spring 200522 February 2005Control FlowConsider two statementsx := 2 and x := 3.The value bound to x after both statements havebeen executed depends on which of the twostatements is executed last. Imperative programs must specify the timeordering of update operations explicitly.A compound expression specifies the functionaldependencies between its parts (and the (partial) timeordering of their operations follows directly).Example:(2+3) * (4+5)The (+)’s must both precede the (*), but they can beperformed in either order (or even concurrently) withno effect on the expression’s value.A compound assignment statement specifies thetime ordering of its parts (but their functionaldependencies do not follow directly).Example:x := 2; x := x + 3; y := 4; y := y + 5; x := x*yWhich statements can be performed concurrently?What permutations of the statements yield the samefinal
View Full Document
Unlocking...