## Handout

Previewing pages *1, 2, 3*
of
actual document.

**View the full content.**View Full Document

## Handout

0 0 182 views

Lecture Notes

- Pages:
- 8
- School:
- Carnegie Mellon University
- Course:
- Cs 15312 - Foundations of Programming Languages

**Unformatted text preview: **

Lecture Notes on Program Equivalence 15 312 Foundations of Programming Languages Frank Pfenning Lecture 24 November 30 2004 When are two programs equal Without much reflection one might say that two programs are equal if they evaluate to the same value or if both of them run forever This explicitly ignores the issue of effects and we will continue to think about a pure language until later in this lecture So in a pure language the statement above reduces the equality of programs to the equality of values But when should two values be equal For example how about the following two functions id 1 x x id 2 x x 0 The first observation is that they are both values so they definitely will not diverge Now id 1 and id 2 return the same integer when applied to an integer but id 1 has more types than id 2 We conclude from that the we should compare two values at a type In general the judgment has the form v v0 where we assume that v and v 0 Here we want to ask if x x x x 0 int int The answer to this question depends on our point of view If we care about efficiency for example they are not equal since the left hand side always takes one fewer step than the right hand side If we care about the syntactic form of the function they are not equal either On the other hand S UPPLEMENTARY N OTES N OVEMBER 30 2004 L24 2 Program Equivalence if we only care about the result of the function when applied to all possible arguments then the two should be considered equal at the given type since both of them are mathematically the identity function on integers In this lecture we are concerned with observational equivalence between programs we consider to programs and values equal if whatever we can observe about their behavior is identical In pure functional languages the only thing you can observe about a program is the final value it returns But there are further restrictions For example we cannot observe the internal structure of functions In implementations they have been compiled to

View Full Document