I'm often confused by the relation between η-conversion and extensionality.
Edit: According to comments, it seems I'm also confused about the relation between extensional equivalence and observational equivalence. But at least in Agda with extensional equality for functions (as a postulate), and for a simply-typed lambda calculus (which has a fully abstract semantics, if I'm not mistaken), denotational equivalence is the same as observational equivalence. Feel free to correct me in comments or answers; I've never gotten systematic education on these matters.
In the untyped lambda-calculus, the eta-rule gives the same proof system as the extensionality rule, as proven by Barendregt (cited in an answer to this question). I understand that to mean that the proof system with the eta-rule is complete for observational equivalence (from other answers, that might need the ξ-rule rule, that is, reduction under binders IIUC; I have no problem adding that rule too).
However, what happens if we switch to a typed calculus and add extend this calculus with extra base types and corresponding introduction and elimination forms? Can we still write a complete proof system for observational equivalence? I will talk about proof systems in form of an axiomatic semantics, following Mitchell's Foundations of Programming Languages (FPL); the proof system/axiomatic semantics defines program equivalence.
Question 1: does Barendregt's theorem extend to STLC? Is the η-equivalence equivalent to extensionality in that context?
I'm browsing FPL's discussion of PCF (but didn't finish the section yet), and it seems that once you add pairs, extensionality requires an additional rule, namely surjective pairing:
pair (Proj1 P, Proj2 P) = P. Interestingly, this rule relates the introduction and elimination of pairs exactly like the η-rule relates the introduction and elimination of functions.
Question 2: Is it sufficient to add the surjective pairing axiom to prove extensionality in simply-typed λ-calculus with pairs? edit: Question 2b: is surjective pairing an η-law, as the η-laws mentioned in this paper, because of the structural similarity I mention?
Let's go all the way to PCF now. Descriptions of extensional equality I've seen then prove that extensionality implies a rule of proof by induction, but they don't say whether that's sufficient. Since PCF is Turing-complete, extensional equality is undecidable. But that doesn't imply that there is no complete proof system, since length of proofs is unbounded. More relevantly, such a proof system would maybe contradict Gödel's incompleteness theorems. And that argument might apply even to PCF without
fix, and to Gödel's System T.
Question 3: Is there a complete proof system for observational equivalence in PCF? What about PCF without
Update: full abstraction
I answer here on the comment on full abstraction. I think PCF suffers from two different sorts of problems: it has non-termination (via fix), which causes the loss of full abstraction, but it also has natural numbers. Both problems make observational equivalence hard to treat, but I believe independently from each other.
On the one hand, PCF loses full abstraction because parallel or lives in the semantic domain (Plotkin 1977), and that seems to have to do with nontermination. Ralph Loader (2000, "Finitary PCF is not decidable") shows that finitary PCF (without naturals, but with nontermination) is already undecidable; hence, (if I sum up correctly) a fully abstract semantic cannot restrict to domains with computable operations.
On the other hand, take Gödel's System T, which doesn't have nontermination. (I'm not sure it has a fully abstract semantics, but I'm guessing yes, because the problem is only mentioned for PCF; the domain must contain higher-order primitive recursive functions). Harper's Practical Foundations for Programming Languages discusses observational equivalence for this language; Sec. 47.4 is titled "Some Laws of Equality", and shows some admissible proof rules for observational equivalence. Nowhere it says whether the proof system is complete, so I guess it is not, but is also nowhere discusses whether it can be completed. My best guess links back to Gödel's theorem of incompleteness.