Lecture 13

​

Equivalence

Programming Languages

UW CSE 341 - Autumn 2021

Last Topic of Unit

More careful look at what “two pieces of code are equivalent” means

​

• Fundamental software-engineering idea
• Made easier with
• Abstraction (hiding things)
• Fewer side effects

​

Not about any “new ways to code something up”

Equivalence

Must reason about “are these equivalent” all the time

• The more precisely you think about it, the better

​

• Code maintenance: Can I simplify this code?
• Backward compatibility: Can I add new features without changing how any old features work?
• Optimization: Can I make this code faster?
• Abstraction: Can an external client tell I made this change?

More specifically

​

To focus discussion: When can we say two functions are equivalent, even without looking at all calls to them?

• May not know all the calls
• For example, editing a library without knowing all the clients

A definition

Two functions are equivalent if they have the same “observable behavior” no matter how they are used anywhere in any program

Given equivalent arguments, they:

• Produce equivalent results
• Have the same (non-)termination behavior
• Mutate (non-local) memory in the same way
• Do the same input/output
• Raise the same exceptions

​

Not observable: time used, space used, local memory

Negative expressiveness

Notice if we know callers cannot “do” or “see” certain things, then more things are equivalent

• Makes maintenance easier
• Makes backwards-compatibility easier
• Makes optimization easier

​

Ways to make sure callers cannot do or see things:

• Restrict the set of possible function arguments
• E.g., with a type system and/or abstraction
• Use immutable data
• Avoid input/output
• Avoid exceptions

Example

Since looking up variables in ML has no side effects, these two functions are equivalent:

​

​

But these next two are not equivalent in general: it depends on what is passed for f

• Are equivalent if argument for f has no side-effects

​

​

​

​

• Example: g (fun i -> print_string "hi" ; i) 7
• Great reason for “pure” functional programming

let f x = x + x

let y = 2

let f x = y * x

let g f x =

(f x) + (f x)

let y = 2

let g f x =

y * (f x)

Another example

These are equivalent only if functions bound to g and h do not raise exceptions or have side effects (printing, updating state, etc.)

• Again: pure functions make more things equivalent

​

​

​

​

​

​

• Example: g divides by 0 and h mutates a top-level reference
• Example: g writes to a reference that h reads from

let f x =

let y = g x in

let z = h x in

(y,z)

let f x =

let z = h x in

let y = g x in

(y,z)

​

​

One that really matters

Once again, turning the left into the right is great but only if the functions are pure:

map f (map g xs)

​

map (f % g) xs

​

Syntactic sugar

Using or not using syntactic sugar is always equivalent

• By definition, else not syntactic sugar

​

Example:

​

​

​

But be careful about evaluation order

let f x =

if x

then g x

else false

let f x =

x && g x

let f x =

if g x

then x

else false

let f x =

x && g x

Three Standard Equivalences

There are three standard equivalences for functions

• Well-studied
• “Should work” in any [decent?] language
• But have some subtlety in when they are applicable

​

Let’s look at each...

Standard equivalences

1. Consistently rename bound variables and uses

​

​

​

But notice you cannot use a variable name already used in the function body to refer to something else

​

​

​

let y = 14

let f x = x+y+x

let y = 14

let f z = z+y+z

let y = 14

let f x = x+y+x

let y = 14

let f y = y+y+y

let f x =

let y = 3 in x+y

let f y =

let y = 3 in y+y

Standard equivalences

2. Use a helper function or do not

​

​

​

​

But notice you need to be careful about environments

​

​

let y = 14

let f x = x+y+x

let g z = (f z)+z

​

let y = 14

let g z = (z+y+z)+z

let y = 14

let f x = x+y+x

let y = 7

let g z = (f z)+z

​

let y = 14

let y = 7

let g z = (z+y+z)+z

Standard equivalences

3. Unnecessary function wrapping

​

​

​

But notice that if you compute the function to call and that computation has side-effects, you have to be careful

​

let f x = x+x

let g y = f y

let f x = x+x

let g = f

let f x = x+x

let h () =

(print_string "hi"; f)

let g y = (h()) y

​

let f x = x+x

let h () =

(print_string "hi"; f)

let g = (h())

​

One more

If we ignore types, then ML let-bindings can be syntactic sugar for calling an anonymous function:

​

​

• These both evaluate e1 to v1, then evaluate e2 in an environment extended to map x to v1
• So exactly the same evaluation of expressions and result

​

But in ML, there is a type-system difference:

• x on the left can have a polymorphic type, but not on the right
• Can always go from right to left
• If x need not be polymorphic, can go from left to right

​

let x = e1 in e2

​

(fun x -> e2) e1

What about performance?

According to our definition of equivalence, these two functions are equivalent, but we learned one is awful

• (Actually we studied this before pattern-matching)

let rec max xs =

match xs with

| [] -> raise Empty

| x::[] -> x

| x::xs' ->

if x > max xs'

then x

else max xs'

let rec max xs =

match xs with

| [] -> raise Empty

| x::[] -> x

| x::xs' ->

let y = max xs' in

if x > y

then x

else y

Different definitions for different jobs

• PL Equivalence (341): given same inputs, same outputs and effects
• Good: Lets us replace bad max with good max
• Bad: Ignores performance in the extreme
• Asymptotic equivalence (332): Ignore constant factors
• Good: Focus on the algorithm and efficiency for large inputs
• Bad: Ignores “four times faster”
• Systems equivalence (333): Account for constant overheads, performance tune
• Good: Faster means different and better
• Bad: Beware overtuning on “wrong” (e.g., small) inputs; definition does not let you “swap in a different algorithm”

​

Claim: Computer scientists implicitly (?) use all three every (?) day

Moral of the story

Equivalence is an essential concept in software development

​

Equivalence is subtle, often depends on:

• Possible side effects
• Variable scope

​

Equivalence is subtle, always depends on:

• What you assume clients can “observe”