14
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I think I could answer some of this, but I am confused as to what it is you're asking. The question you refer to is not about program equivalence. Do you mean observational equivalence? For what operational semantics? So, essentially, if you explain exactly what "the proof" in Question 1 refers to, I think I can guess what's going on. My best guess so far: you would like an equational theory which is complete for observational equivalence, and you're asking us whether $\eta$-rules suffice. Is that it? $\endgroup$ – Andrej Bauer May 16 '13 at 6:52
  • $\begingroup$ @AndrejBauer: your guess is correct, I'll start updating the question. $\endgroup$ – Blaisorblade May 19 '13 at 3:40
  • $\begingroup$ I'm not sure about the operational semantics - does that make a difference for the original theorems? $\endgroup$ – Blaisorblade May 19 '13 at 3:57
  • $\begingroup$ I tried to refine the question further. But I still think your best guess is correct. $\endgroup$ – Blaisorblade Nov 20 '13 at 21:00
  • $\begingroup$ There's a small problem here: it's really not clear what $\eta$ is for the natural numbers! If you just have just function and product types, then you're in the clear: terms are observationally equivalent iff they are $\beta\eta$ equal. More generally, I think this is related to the problem of full abstraction. $\endgroup$ – cody Nov 22 '13 at 22:15
7
$\begingroup$

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!).

$\endgroup$
  • $\begingroup$ Thanks for your answer! My first question is: is it usual to have substitutions in contexts for observational equivalence? At least Plotkin's LCF paper (1997) does not do that (though I can imagine something like that would make sense in some closure calculus, where something like substitutions is part of the syntax). But I can easily see for each "substitution" context one can define a more (for me) "standard" context which uses just lambda-abstraction and application, say (λx.[]) c_x; so I guess the observational equivalence above is equivalent to the definition I'm used to. $\endgroup$ – Blaisorblade Dec 2 '13 at 22:17
  • $\begingroup$ The "true but not provable" equation is (I assume) $t = \lambda x.0$, not $0 =_{\beta\eta} S 0$, right? To construct ${\cal M}$, I guess you just need to enumerate proofs looking for one of $0 =_{\beta\eta} S 0$. However, I'm still lost as to why 0 = 1 is hard enough — actually, it should be easy to prove that $0 \not=_{\beta\eta} S\ 0$ since they're both normal forms, and I'd be surprised if Peano arithmetic weren't strong enough. $\endgroup$ – Blaisorblade Dec 2 '13 at 22:38
  • $\begingroup$ Say instead that ${\cal M}$ searches for a proof of the inconsistency of arithmetic. You still have $t = \lambda x . 0$ because arithmetic is consistent, but by the second incompleteness theorem, proving this requires more metatheoretic power than Peano arithmetic (or than the rules we discussed), so our simple rules won't be able to proof this observational equivalence. Does this make sense? I've looked up Wikipedia, but it's not very specific on Kleene's variant of Gödel's result; maybe if I knew that proof better, I would also understand your proof. (Meanwhile, upvoting you anyway). $\endgroup$ – Blaisorblade Dec 2 '13 at 22:57
  • 1
    $\begingroup$ 3. Note that $\mathrm{PA}$ can prove $0\neq 1$, but not "$\mathrm{PA}\not\vdash 0=1$", so you can try looking for that proof for ever. I've used the same kind of trick above to find an observational equality in $T$ that can't be captured by any "reasonable" equality rule. You could always add the rule $$ \frac{f\ 0=g\ 0\quad f\ (S\ 0)=g\ (S\ 0)\ldots}{f=g} $$ but that would be non-effective (and complete!). I have a feeling that's not what you're looking for though. $\endgroup$ – cody Dec 2 '13 at 23:36
  • 1
    $\begingroup$ That's right! Though it does sometimes make sense to consider such "infinitary" systems for proof-theoretical purposes (e.g. ordinal analysis). $\endgroup$ – cody Dec 3 '13 at 16:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.