DOC PREVIEW
CMU CS 15312 - Handout

This preview shows page 1-2-3 out of 8 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Lecture Notes onProgram Equivalence15-312: Foundations of Programming LanguagesFrank PfenningLecture 24November 30, 2004When are two programs equal? Without much reflection one might saythat two programs are equal if they evaluate to the same value, or if bothof them run forever. This explicitly ignores the issue of effects, and we willcontinue to think about a pure language until later in this lecture. So, in apure language the statement above reduces the equality of programs to theequality of values. But when should two values be equal? For example,how about the following two functions.id1= λx.xid2= λx.x + 0The first observation is that they are both values, so they definitely will notdiverge.Now, id1and id2return the same integer when applied to an integer,but id1has more types than id2. We conclude from that the we shouldcompare t wo values at a type. In general, the judgment has the for mv ' v0: τwhere we assume that · ` v : τ and · ` v0: τ . Here we want to ask if(λx.x) ' (λx.x + 0) : i nt → int?The answer to this question depends on our point of view. If we careabout efficiency, for example, they are no t equal since the left-hand sidealways takes one fewer st ep t h an the right-hand side. If we care about th esyntactic fo r m of the function, t h ey are not equal either. On the oth er hand,SUPPLEMENTARY NOTES NOVEMBER 30, 2004L24.2 Program Equivalenceif we only care about the result of the function when applied to all possiblearguments, then the two sho uld be considered equal at the given type, sinceboth of them are (mathematically) the identity function on integers.In this lecture we are concerned with observational equivalence betweenprograms: we consider to programs (and values) equal if whatever we canobserve about their behavior is identical. In pure functional languages, theonly t h ing you can obs erve about a program is the final value it returns. Butthere are further restrictions. F or example, we cannot observe the intern alstructure of functions. In implementations, they have been compiled tomachine code—all w e see is a token such as fn indicating the given valuecannot be printed.If we cannot observe the structure of a function, what can be obse r veabout a function? We can apply it to arguments and observe its result. Butthis result may again be a function who se structure we cannot see directly.It appears we are moving in a vicious circle, trying to define observationalequivalence of functions in ter ms of itself.Fortunately, there is a way out. We once again use types in order tocreate order out of chaos. In our example above, the functions λx.x andλx.x + 0 should be equal at type int → int because apply both of them toequal arguments of type int will always yield equal results of type int. Andvalues of type int are directly observable—they form a basic data type ofour language.Using this intuition we can now define two relations of observationalequivalence for a pure, call-by-value language by simultaneous indu ctionon the structure of a type of t h e expressions w e are comparing. We writee ⇑ if the evaluation of e does not terminate. We also use the conventionthat w h en we write e∼=e0: τ that · ` e : τ and · ` e0: τ and similarly forvalues without restating this every time.e∼=e0: τ iff either e ⇑ and e0⇑or e 7→∗v and e07→∗v0with v ' v0: τv ' v0: int iff v = v0= n for an integer n.v ' v0: bool iff v = v0= true or v = v0= falsev ' v0: τ1→ τ2iff for all v1' v01: τ1we have v v1∼=v0v01: τ2The last clause requires careful analysis. Functions are not observabledirectly, although we can apply them to arguments to observe their result.The case of values of function type can the refore be s ummarized as: “Twofunctions are equal at type τ1→ τ2if they deliver equal results of type τ2when ap-plied to equal arguments of type τ1.” Note that o n the right-hand side the typesare smaller than o n th e left-hand side, so the de fin ition is well-founded. ItSUPPLEMENTARY NOTES NOVEMBER 30, 2004Program Equivalence L24.3is also allowed that ne ither of the tw o functions terminates when givenequal arguments. This follows from comparing the expressions v v1andv0v01which have to be evaluated first.We can use this definition to prove our original assertion that λx.x 'λx.x + 0 : int → i nt .v1' v01: int Assumptionv1= v01= n for some inte ger n By definition of 'n ' n : int By definition of '(λx.x) n 7→∗n By de fin ition of 7→(λx.x + 0) n 7→∗n By de fin ition of 7→(λx.x) n∼=(λx.x + 0) n : int By definition of∼=(λx.x) v1∼=(λx.x + 0) v01: int Since v1= v01= n(λx.x) ' (λx.x + 0) : i nt → int By definition of 'In many cases equivalence proofs are not that straightforward, but re-quire cons iderable effort. As a slightly more complicated example considerid1= λx.xid3= rec f. λx.if x = 0 th en 0 else f (x − 1) + 1We notice that id1and id3are in fact not equal at type int → int becauseid3(−1) diverges, while id1(−1) 7→∗−1. However, w h en applied to nat-ural numbers, that is, integers greater or equal to 0, then they are obser-vationally equal (both return the argument). In order to capture this weintroduce nat ≤ int under the subset interpretation of subtyping and ex-tend observational e q uivalence with the clausev ' v0: nat iff v = v0= k for some k ≥ 0.With these definitions we need a lemma, which can be proven by in-duction on k. For this, we introduce the definitionid03= λx. if x = 0 then 0 else id3(x − 1) + 1which has the property that id37→ id03and id03is a value. Now we canprove:For any k ≥ 0, we have id1k∼=id03k : nat.Proof: B y induction on k.Case: k = 0. Then id10 7→ 0 and id030 7→ if 0 = 0 then 0 else id3(k − 1) +1 7→∗0.SUPPLEMENTARY NOTES NOVEMBER 30, 2004L24.4 Program EquivalenceCase: k = k0+1. Then id1k 7→ k and id03k 7→∗id3(k−1)+1 7→∗id03(k0)+1.By ind uction h ypothesis, id03(k0)∼=id1(k0) so id03(k0)∼=k0and id03k 7→∗k0+ 1 = k, which is what we needed to sho w. From this it follows directly by definition of ' that id1= i d3, sincev1' v01: nat iff v1= v01= k for some k and id37→ id03.Some care must be taken in ge n eral to define observational equivalencecorrectly with respect to what is observable. For ex ample, in a call-by-namelanguage we would have to apply functions to arbitrary e x pressions, in-stead of testing them just on values.It s h ould also be clear that in t h e presence of e ffects, be it store


View Full Document

CMU CS 15312 - Handout

Download Handout
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Handout and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Handout 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?