PFPL Ch 46 Speaker: Stephanie
potential proposal: skip chapter 47 so we can spend more time on this chapter?
This week's subject: program equivalence. Today, System T.
We are going to define what it means for programs to be equivalent. We will focus on two definitions:
"observational equivalence"
and
"logical equivalence"
These two definitions of equality are equivalent to eachother. However, they work in different ways.
Note, there is a Coq script to go with this chapter.
-
Bob mentioned that the transitivity of Kleene equality follows from determinacy of evaluation. Why does the transitivity rely on the determinacy?
[SCW: Say you know that
e1 ->* j /\ e2 ->*j and e2 ->* k /\ e3 ->*kTransitivity requires showing some common number i such that e1 and e3 both evaluate to it. However, if evaluation is deterministic, then because e2 evaluates to both j and k, we know that j=k. So we can use that.]
-
How do we define the equality between non-determinate programs?
[SCW: If we don't have determinism, then we need a property called confluence. This property says that even if two evaluation sequences diverge, there always is a way for them to come together.]
-
This chapter discusses the equivalence problem on system T with eager dynamics. However, how do we consider the equivalence problem for languages with lazy dynamics?
[SCW: we can do so similarly, but perhaps we may not have access to the "proof by nat-induction" Bob refers to in 46.8]
-
Why do we define observational equivalence using holes and program contexts. It seems more complicated than the type of program equivalence defined in the Software Foundations book:
Definition cequiv (c1 c2 : com) : Prop := ∀(st st' : state), (c1 / st ⇓ st') ↔ (c2 / st ⇓ st')
[SCW: This is a good question. The answer depends on the observations of the language. In SF, only the final state of the computation is observable. However, in this language we don't have state, we only have results. If those results are ints, then we can compare them. But what if they are functions? How do well tell if they are equivalent? In that case, we need to "observe" them by applying them to arguments until we get ints out that we can look at.]
-
One of our theorems states: "Observational equivalence is the coarsest consistent congruence of expressions". What does it mean by "coarsest"?
[SCW: Coarsest means that this one equates the most it can, while still being consistent. ]
-
I am not clear about why theorem 46.6 can license the principle of proof by coinduction.
[SCW: See TAPL 21.1
Suppose you have a monotone function, F : Set -> Set. We'll call F a generating function. Now consider the follwing definitions.
A set X is a fixpoint if F(X) = X. A set X is F-closed if F(X) <= X A set X is F-consistent if X <= F(X)
The Knaster-Tarski theorem states:
- lfp(F) is intersection of all F-closed sets (i.e. mu F) - gfp(F) is the union of all F-consistent sets (i.e. nu F)
This gives us the principle of induction:
If X is F-closed, then mu F <= X
And the principle of coinduction:
If X is F-consistent, then X <= nu F
How does this relate in this case? Suppose we want to show that two expressions are related --- in other words, that the pair (e1,e2) is in the observational equivalence relation. We can do this via the principle of coinduction if we can find some F, such that observational equivalence is nu F, i.e. the union of all F-consistent sets. We then only must show that the set {(e1,e2)} is F-consistent, i.e. {(e1,e2)} <= F{(e1,e2)}.
However, I'm a bit stuck here. An F-consistent set in this case should be any consistent congruence relation. But I'm not sure how to derive F from that. ]
-
Could we perhaps go through what exactly does Bob mean by a "coarsest" relation in class? And what does being the coarsest have to do with the principle of proof by coinduction?
[SCW: see above]
-
If possible, I would love to have more precision about why th. 46.6 permits proof by coinduction (2nd paragraph of page 439). I possibly have some remote intuition about why this would be the case, but I'm really not sure about that - so a clear and precise argument would be very helpful
[SCW: see above]
-
At the start of Section 46.2 Bob talks about classifying uses of expressions of a type into active and passive uses. How does the definition of logical equivalence correspond to this intuition? I don't quite see the connection.
[SCW: Look in 46.8 --- we define equivalence at function types in terms of applications (of related arguments). What if we wanted to add products to System T? How would this definition change?]
-
I'm not sure how the distinction between active and passive uses of an expression is playing out in the definition of logical equivalence. Could you go through that in the lecture?
[SCW: see above]
-
Generally, how can you tell when proving a theorem that you need logical relations?
[SCW: Hmmm. Good question.]
-
Shouldn't Kleene equality suffice for System T since every program terminates? Seems like the extra book-keeping arguments that we used in the proof of termination like open hereditary termination are being replicated with logical equivalence in some way e.g. open logical equivalence...
[SCW: Yes. The termination proof is essentially the same proof as our proof of reflexivity for logical equivalence. However, logical equivalence gets us more than kleene equivalence. For example, it justifies the equivalence rules in 46.4. These rules don't fall out of kleene equivalence.]
-
In fact, I'm not even sure that I understand the real difference between logical equivalence and hereditary termination. Also, why is logical equivalence a family of relations satisfying the conditions described? Does he just mean that any relation on closed typed expressions which satisfies the conditions described is a logical equivalence, or that logical equivalence is actually a family of relations? Why the use of the word family?
[SCW: See above. The connection you are seeing is real. Bob uses the word family because it is a relation indexed by types. Kinda like overloading. ]
-
I'm having a hard time seeing how termination (46.15) is an immediate corollary of reflexivity.
[SCW: See the Coq script. Reflexivity is a bit of overkill, the important thing for termination is not that all elements are related to themselves, but that all elements are related to something. The definition of this logical relation only includes terminating expressions.]
-
Also, (minor), is "closing substitution" a widely used term? I feel like I needed to use it quite a few times in the past (especially when talking about valuations/random generation) and I just ended up describing it in a couple of phrases.
[SCW: I've seen it used before.]
-
I cannot follow some of the proofs such as theorem 46.20. Could you give a bigger picture of the proof of logical and observational equivalence coincide and how each Lemma can contribute to the final proof?
[SCW: I will try in class. Also see the Coq script.]
-
Could we go over the proof of coincidence of logical and observational equivalence? Indeed, while I could follow the individual arguments while reading, I feel like the presentation of this part is a little messy; it is hard to get a good global view of the argument(s)/proof without re-sketching it oneself
[SCW: ditto.]
-
This chapter shows that observational and logical equivalences are the same for system T. Is this true for any system in general? If not, can you give examples of systems where observational equivalence implies logical equivalence but not the other way around and vice-versa?
[SCW: It is true for this system and also will be true for PCF and System F. In fact, we would not define logical equivalence unless we can show it equivalent.]
-
What’s the relationship between logical and observational equivalence in general? Is there a language setting such that observational equivalence does not imply logic equivalence, or that logical equivalence does not imply observational equivalence?
[SCW: see above]
-
I don't understand the real difference between logical equivalence and observational equivalence. In particular, I don't understand why/how they could fail to coincide in any reasonable programming language since both logical and observational equivalence boil down to Kleene equality on base types. Is there a true statement which is proved much more naturally using logical equivalence instead of observational equivalence or vice versa?
[SCW: see above. In practice, if you want to show that two terms are equivalent, it is easier to use logical equivalence because you do not have to quantify over all contexts. ]
-
What is the intuition behind using logical equivalence to simplify observational equivalence. Is there any other relation that can do the similar thing?
[SCW: Hmmm. ]