<p>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.</p>

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

<p>I find it more natural to consider terms with "holes" or <em>contexts</em>
 $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]$.</p>

<p>Now it is a fact that observational equality in the untyped calculus
 is <strong>not captured</strong> 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 <strong>perpetual terms</strong> or <strong>unsolvable terms</strong>, 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.</p>

<p>If all perpetual terms are identified, then observational equality is
 completely captured, by a classic result (see <a href="http://rads.stackoverflow.com/amzn/click/0444875085" rel="noreferrer">Barendregt</a> theorem 16.2.7).</p>

<hr>

<p>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$.</p>

<ol>
<li><p>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.</p></li>
<li><p>At arrow type, $t_1\downarrow t_2$ iff both terms $\beta$-reduce to a
$\lambda$-abstraction.</p></li>
</ol>

<p>Note that I only use $\beta$-conversion in this definition.</p>

<p>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.</p>

<p>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 <strong>closed</strong>.
 $$ E[t]\downarrow E[t']$$
 we will write $t=_{\mathrm{obs}}t'$ in this case</p>

<p>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:</p>

<ol>
<li><p>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 (<a href="http://rads.stackoverflow.com/amzn/click/0444875085" rel="noreferrer">Barendregt again</a>
10.4.2).</p></li>
<li><p>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'$$</p></li>
</ol>

<p>That was harder than expected!</p>

<hr>

<p>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)$$</p>

<p>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.</p>

<p>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$).</p>

<p>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 <a href="http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Relationship_with_computability" rel="noreferrer">Wikipedia</a>). 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.</p>

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

CC BY-SA 3.0
2013-12-02T22:17:07.137Z
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.
Blaisorblade
CC BY-SA 3.0
2013-12-02T22:38:09.070Z
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.
Blaisorblade
CC BY-SA 3.0
2013-12-02T22:57:26.260Z
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).
Blaisorblade
CC BY-SA 3.0
2013-12-02T23:30:37.240Z
I'm going to try and answer your questions in order. 

1. I added the substitution part just so I would only have to define value equality on closed terms. One way to look at it is that an evaluation context is a "machine state" in which the term is reduced.

2. The "true but not provable" equation is indeed $t_{\cal M} = \lambda x.0$. I tried to clarify my proposal above. However the machine ${\cal M}$ in question here is a machine that enumerates proofs *in $T$* and tries to find a proof of $0=S\ 0$. System $T$ doesn't know how to prove things are disequal, only that things are equal.
cody
CC BY-SA 3.0
2013-12-02T23:36:48.137Z
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.
cody
CC BY-SA 3.0
2013-12-03T00:47:34.187Z
3. Ah! Proving PA $\not\vdash 0 = 1$ requires proving that PA is consistent (ultimately, because of the explosion principle), and PA is too weak for that by the second incompleteness theorem. Thanks for the major "Eureka" moment.
Also, your alternative rule highlights that "observational equivalence can't be completely captured by *effective* inference rules" (indeed, ${\cal M}$ would not be able to produce a finite proof using this rule). A rule using quantification in the premise could be stated using first-order logic, but it would still fail by the second theorem.
Blaisorblade
CC BY-SA 3.0
2013-12-03T16:44:37.890Z
That's right! Though it does sometimes make sense to consider such "infinitary" systems for proof-theoretical purposes (e.g. ordinal analysis).
cody
CC BY-SA 3.0
2013-12-02T21:10:18.630Z
2017-03-13T15:07:37.640Z
2017-03-13T15:07:37.640Z
cody
<p>I'm often confused by the relation between η-conversion and extensionality.</p>

<p>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.</p>

<p>In the untyped lambda-calculus, the eta-rule gives the same proof system as the extensionality rule, as proven by Barendregt (cited in <a href="https://cstheory.stackexchange.com/a/8263/989" title="Answer citing Barendregt">an answer</a> to <a href="https://cstheory.stackexchange.com/q/8259/989" title="What&#39;s the point of η-conversion in lambda calculus?">this question</a>). 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).</p>

<p>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.</p>

<p><strong>Question 1</strong>: does Barendregt's theorem extend to STLC? Is the η-equivalence equivalent to extensionality in that context?</p>

<p>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: <code>pair (Proj1 P, Proj2 P) = P</code>. Interestingly, this rule relates the introduction and elimination of pairs exactly like the η-rule relates the introduction and elimination of functions.</p>

<p><strong>Question 2</strong>: Is it sufficient to add the surjective pairing axiom to prove extensionality in simply-typed λ-calculus with pairs? <strong><em>edit</em></strong>: <strong>Question 2b</strong>: is surjective pairing an η-law, as the η-laws mentioned in <a href="http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf" rel="nofollow noreferrer" title="Observational equality now">this paper</a>, because of the structural similarity I mention?</p>

<p>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, <a href="https://cstheory.stackexchange.com/a/14152/989" title="Answer to &#39;Is it possible to compute whether two functions are extensional equal?&#39;">extensional equality is undecidable</a>. 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 <code>fix</code>, and to Gödel's System T.</p>

<p><strong>Question 3</strong>: Is there a complete proof system for observational equivalence in PCF? What about PCF without <code>fix</code>?</p>

<h3>Update: full abstraction</h3>

<p>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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2013-05-16T06:52:13.363Z
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?
Andrej Bauer
CC BY-SA 3.0
2013-05-19T03:40:13.520Z
@AndrejBauer: your guess is correct, I'll start updating the question.
Blaisorblade
CC BY-SA 3.0
2013-05-19T03:57:31.143Z
I'm not sure about the operational semantics - does that make a difference for the original theorems?
Blaisorblade
CC BY-SA 3.0
2013-11-20T21:00:00.960Z
I tried to refine the question further. But I still think your best guess is correct.
Blaisorblade
CC BY-SA 3.0
2013-11-22T22:15:59.180Z
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_.
cody
CC BY-SA 3.0
2013-11-23T00:42:03.207Z
@cody: There's no eta, but axiomatizations for the equational theory add an induction proof rule.
Blaisorblade
CC BY-SA 3.0
2013-11-23T01:14:15.540Z
@cody: I added an answer on full abstraction.
Meanwhile, thanks for your answer anyway.
Blaisorblade
<pl.programming-languages><lambda-calculus>
η-conversion vs extensionality in extensions of lambda-calculus
Blaisorblade
# η-conversion vs extensionality in extensions of lambda-calculus

(Asked by: username_0 on 2013-05-15)

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](https://cstheory.stackexchange.com/a/8263/989 "Answer citing Barendregt") to [this question](https://cstheory.stackexchange.com/q/8259/989 "What's the point of η-conversion in lambda calculus?")). 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](http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf "Observational equality now"), 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](https://cstheory.stackexchange.com/a/14152/989 "Answer to 'Is it possible to compute whether two functions are extensional equal?'"). 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.

**Tags:** pl.programming-languages, lambda-calculus

> **Comments:**
> **username_1**: 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?  
> **username_0**: @AndrejBauer: your guess is correct, I'll start updating the question.  
> **username_0**: I'm not sure about the operational semantics - does that make a difference for the original theorems?  
> **username_0**: I tried to refine the question further. But I still think your best guess is correct.  
> **username_2**: 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_.  
> **username_0**: @username_2: There's no eta, but axiomatizations for the equational theory add an induction proof rule.  
> **username_0**: @username_2: I added an answer on full abstraction. Meanwhile, thanks for your answer anyway.  

---

## 1 answers

### Answer by username_2 on 2013-12-02. Score: 9 | Accepted answer

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](http://rads.stackoverflow.com/amzn/click/0444875085) 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](http://rads.stackoverflow.com/amzn/click/0444875085)
   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](http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Relationship_with_computability)). 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!).

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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.  
> **username_0**: 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).  
> **username_2**: I'm going to try and answer your questions in order.   1. I added the substitution part just so I would only have to define value equality on closed terms. One way to look at it is that an evaluation context is a "machine state" in which the term is reduced.  2. The "true but not provable" equation is indeed $t_{\cal M} = \lambda x.0$. I tried to clarify my proposal above. However the machine ${\cal M}$ in question here is a machine that enumerates proofs *in $T$* and tries to find a proof of $0=S\ 0$. System $T$ doesn't know how to prove things are disequal, only that things are equal.  
> **username_2**: 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.  
> **username_0**: 3. Ah! Proving PA $\not\vdash 0 = 1$ requires proving that PA is consistent (ultimately, because of the explosion principle), and PA is too weak for that by the second incompleteness theorem. Thanks for the major "Eureka" moment. Also, your alternative rule highlights that "observational equivalence can't be completely captured by *effective* inference rules" (indeed, ${\cal M}$ would not be able to produce a finite proof using this rule). A rule using quantification in the premise could be stated using first-order logic, but it would still fail by the second theorem.  
> **username_2**: That's right! Though it does sometimes make sense to consider such "infinitary" systems for proof-theoretical purposes (e.g. ordinal analysis).  

---

