η-conversion vs extensionality in extensions of lambda-calculus

Question

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 fix?

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.

Answer 1

I'm not sure I can completely answer your question, but I'll give it a shot, and ask a few questions of my own that might spur some further discussion on this subject.

My first point is this: two terms $t, t'$ in the untyped $\lambda$-calculus are said to be observably equal iff for every term $M$: $$M\ t \mbox{ terminates } \Leftrightarrow M\ t' \mbox{ terminates }$$ Where terminates means "has a $\beta$-normal form"

I find it more natural to consider terms with "holes" or contexts $E[\_]$ instead of simply terms $M$ and write $E[t]$ instead of $M\ t$. The two views are certainly equivalent (if variables are not bound by the context), as abstraction allows you to turn the context $E[\_]$ into the term $\lambda x.E[x]$.

Now it is a fact that observational equality in the untyped calculus is not captured by $\beta\eta$-equality! Indeed there is a whole class of terms, which both do not terminate and have no head normal forms and are all therefore observably equal. These are sometimes called the perpetual terms or unsolvable terms, and here are two such terms: $$ (\lambda x. x\ x)(\lambda x. x\ x)$$ and $$ (\lambda x. x\ x\ x)(\lambda x. x\ x\ x)$$ It's quite easy to show that these terms are not $\beta\eta$-equal.

If all perpetual terms are identified, then observational equality is completely captured, by a classic result (see Barendregt theorem 16.2.7).

---

Now for typed calculi. Let's consider the simply typed $\lambda$-calculus without natural numbers first. The above definition of observational equality becomes trivial, as every term normalizes! We need a finer distinction. We will use value equality $t_1\downarrow t_2$ for closed terms, defined by induction on the type of $t_1$ and $t_2$. Let's first add for each type $A$, an infinite number of constants $c_A, c_A', c''_A,\ldots$. We'll choose some constant $c_x$ of the appropriate type to correspond to each variable $x$.

1. At base type $B$, $t_1\downarrow t_2$ iff the $\beta$-head normal form of $t_1$ is $c\ u_1\ldots u_n$ and that of $t_2$ is $d\ v_1\ldots v_n$ and $c=d$ and $u_1\downarrow v_1,\ldots, u_n\downarrow v_n$ at their respective types.

2. At arrow type, $t_1\downarrow t_2$ iff both terms $\beta$-reduce to a $\lambda$-abstraction.

Note that I only use $\beta$-conversion in this definition.

Now I define contexts to be: $$[\_]\mid E[\_]\ u\mid t\ E[\_]\mid \lambda x.\ E[\_]\mid E[\_]\theta $$ with the head context, application, abstraction and substitution (by closed terms) respectively.

We can then define $t$ and $t'$, well typed of type $T$ to be observationally equivalent if and only if for every context $E[\_]$ such that $E[t],E[t']$ are well-typed and closed. $$ E[t]\downarrow E[t']$$ we will write $t=_{\mathrm{obs}}t'$ in this case

Now it is easy to observe that if $t=_{\beta\eta}t'$ then $t=_{\mathrm{obs}}t'$. The other direction is less trivial, but also holds: indeed, if $t=_{\mathrm{obs}}t'$, then we can show that the terms are equal for $\beta\eta$ by induction on the type:

1. At base type, simply take $E[\_]$ to be $[\_]\theta$, with $\theta$ the substitution that sends $x$ to $c_x$. We have $E[t]=t\theta$ and $E[t']=t'\theta$. We have $t\theta\rightarrow_\beta c_x\ u_1\theta\ldots u_n\theta$ and $t'\theta\rightarrow_\beta c_{x'}\ v_1\theta\ldots v_n\theta$. We then have $c_x=c_{x'}$ and so $x=x'$. Now we can't immediately conclude that $u_i\theta=_{\beta\eta}v_i\theta$. Indeed, if $u_i$ and $v_i$ are $\lambda$-abstractions, then trivially $u_i\theta\downarrow v_i\theta$! The trick here is to send $x$ to $$\lambda \vec{y}.\tilde{c_x}\ (y_1\vec{c_1})\ldots (y_n\vec{c_n})$$ and to repeat this as many times as necessary. I'm a bit fuzzy on the details here, but the idea is similar to Böhm's theorem (Barendregt again 10.4.2).

2. At arrow type, take $E[\_]$ to be $[\_]\ c_y$, i.e. application to $c_y$ with $c_y$ and $y$ not in $t$ or $t'$. By the induction hypothesis we have: $$ t\ c_y \ =_{\beta\eta}\ t'\ c_y$$ and so $$ t\ y \ =_{\beta\eta}\ t'\ y$$ Which gives $\lambda y.t\ y\ =_{\beta\eta}\ \lambda.t'\ y$ and finally by $\eta$-equality: $$t\ =_{\beta\eta}\ t'$$

That was harder than expected!

---

Alright let's tackle system T. Let's add a type $\mathbb{N}$ to the mix, constructors $0$ and $S$, and a recursor $\mathrm{rec_T}$ for each type $T$, with the "$\beta$-rules" $$ \mathrm{rec_T}\ u\ v\ 0\rightarrow_{\beta} u$$ $$ \mathrm{rec_T}\ u\ v\ (S\ n)\rightarrow_{\beta} v\ n\ (\mathrm{rec_T}\ u\ v\ n)$$

We want to prove the same theorem as above. It's tempting to add "$\eta$-rules" to prove equivalences like: $$ \lambda x.x\ =_{\beta\eta}\ \mathrm{rec_{\mathbb{N}}}\ 0\ (\lambda k\ m.S\ m)$$ where the term on the right is the "stupid identity" that peels off $m$ successors just to add them again.

For example let's add this rule: $$ \frac{f\ (S\ x)\ =_{\beta\eta}\ h\ x\ (f\ x)}{f\ t\ =_{\beta\eta}\mathrm{rec_T}\ (f\ 0)\ h\ t}$$ where $x$ is a fresh variable as in the usual $\eta$ rule. Now note that this rule is recursively enumerable (you can try every possible choice for $h$).

Can we prove the same theorem as above? Unfortunately, as you suspected, you're going to run into some Gödel nastiness, or rather, the Kleene variant (see Wikipedia). For every Turing machine ${\cal M}$, it's easy to build a term $t_{\cal M}$ in system $T$ such that $t_{\cal M}\ (S\ldots\ S\ 0)$ (with $n$ $S$es) returns $1$ if ${\cal M}$ finishes in at most $n$ steps and $0$ otherwise.

So now if ${\cal M}$ does not terminate, you can ask whether the (true) equation $$t_{\cal M}\ = \lambda x.0$$ is provable using the $\beta\eta$ rules above. But taking ${\cal M}$ to be the machine that terminates iff $$0\ =_{\beta\eta}\ S\ 0$$ is provable in system $T$ (with the above rules), you're going to run into trouble, i.e. the equation $t_{\cal M}=\lambda x.0$ is true but not provable (or Peano Arithmetic is inconsistent!).