<p>A compositional denotational semantics $[\![ {-} ]\!]$ of a programming language (a domain-theoretic or game-theoretic one, for instance) is <strong>adequate</strong> if semantically equal terms imply that they are observationally equivalent:
$$[\![ t_1 ]\!] = [\![ t_2 ]\!] \implies t_1 \cong t_2.$$
It often happens that it is far easier to calculate denotations that to prove observational equivalence. This is a common technique with many known variants. Adequacy is defined already in Plotkin's PCF paper.</p>

CC BY-SA 3.0
2015-03-07T20:22:57.397Z
There is no particular need for the adequate semantics to use some other formalism. You can also soundly approximate $\cong$ within the programming language under discussion, e.g. using operational methods.
Martin Berger
CC BY-SA 3.0
2015-03-08T00:08:19.147Z
Thanks for the answer, but -1: While I agree, the question mentions pure type systems — AFAICS, a denotational semantics for pure type systems is an open problem, so I think an answer should point to some denotational semantics.
(In fact, if I had a denotational semantics, I'd dispense with the operational one altogether, as mentioned in the question).
(But sorry for the overly long question.)
Blaisorblade
CC BY-SA 3.0
2015-03-08T10:02:59.997Z
@MartinBerger, I do not understand your criticism. The OP asks for methods of showing observational equivalence, I mention a common one, and then you object that other ways exist which avoid the method?
Andrej Bauer
CC BY-SA 3.0
2015-03-08T10:03:42.003Z
@Blaisorblade, well then you'll just have to invent a denotational semantics for pure type systems, won't you? :-) But more seriously, I'll ask Alex Simpson, he would know better about denotational semantics for such things.
Andrej Bauer
CC BY-SA 3.0
2015-03-16T18:27:00.330Z
@AndrejBauer It wasn't meant to be a criticism, more as an addendum.
Martin Berger
CC BY-SA 3.0
2016-03-18T13:24:06.800Z
@AndrejBauer Conjecture: you can collapse arbitrary PTSs to $\lambda^*$ and use the existing denotational semantics (based on domain theory) for the latter. I assume the result won't be fully abstract most of the time, but that's probably still useful enough for some purposes.
Blaisorblade
CC BY-SA 3.0
2015-03-07T20:09:43.423Z
2017-03-10T21:09:04.040Z
2017-03-10T21:09:04.040Z
Andrej Bauer
<p>The domain and model theories of PTSes hasn't been explored all that much I'm afraid. One detailed source is Thomas Streicher's PhD work: <a href="http://link.springer.com/book/10.1007%2F978-1-4612-0433-6" rel="nofollow">Semantics of Type Theory</a>. He gives category theoretic semantics for all PTS, though I'm not sure he addresses $\eta$-conversion.</p>

CC BY-SA 3.0
2015-03-16T18:47:43.597Z
I don't think Streicher's PhD is about PTS. It's about semantics of the Calculus of Constructions and independence results via reliability semantics. See [here](http://goo.gl/cdaqE7).
Martin Berger
CC BY-SA 3.0
2015-03-16T19:41:07.233Z
Thanks for the clarification! I'm afraid the link is broken though (and hard to fix with the minified link).
cody
CC BY-SA 3.0
2015-03-16T19:43:20.500Z
The link was to table of content of the book [here](http://link.springer.com/book/10.1007%2F978-1-4612-0433-6). I hope this one works better.
Martin Berger
CC BY-SA 3.0
2015-05-01T19:47:16.850Z
@MartinBerger: thanks for the clarification! I'll go back to assuming that a semantics for arbitrary PTSs (ranging to System U and $\lambda^*$ and all their pathologies) is beyond our reach.
Blaisorblade
CC BY-SA 3.0
2018-04-25T09:49:48.123Z
@MartinBerger: do you mean realizability semantics?
Dominique Devriese
CC BY-SA 3.0
2018-04-25T11:12:09.497Z
@DominiqueDevriese Yes, of course. Autocorrect always catches me off-guard. Thanks for pointing this out.
Martin Berger
CC BY-SA 3.0
2018-04-25T14:38:02.570Z
@Blaisorblade just to be clear, domain theoretic semantics are somewhat impervious to non-termination issues such as occur in system U and its ilk. In general, there are models of polymorphic theories in domains, see e.g. Coquand *et al* "Domain theoretic models of polymorphism". I don't think there is any *theoretical* objection to extending this to arbitrary PTSes, just the work hasn't really been done. Of course, I would be more interested in models capable of implying normalization, but those *do* run into problems for system U.
cody
CC BY-SA 3.0
2018-04-26T15:37:52.270Z
cody: I wasn't expecting difficulties for any given PTS due to non-termination, but giving _one_ semantics parametric in multiple ones seems harder — how many universes are you going to need?

What's more worrisome is that your semantics must be impervious to impredicativity issues. Luckily domain theory lets you solve arbitrary mixed-variance fixpoint equations, and I guess that might help; I'm currently using the other approach to those equations (based on Birkedal et al.'s work on ultrametric spaces/step-indexing) for a different impredicative system.
Blaisorblade
CC BY-SA 3.0
2015-03-09T01:55:31.693Z
2015-03-09T01:55:31.693Z
cody
<p>This answer suggests an approach to the problem. (Feedback is welcome).</p>

<p>PFPL chapter 49 discusses, at once, the equivalent notions of observational equivalence and logical equivalence. Logical equivalence is the same relation used to state parametricity, so the core of the chapter is a proof of parametricity for System F.</p>

<p>Work on parametricity for PTS, AFAICT, does not discuss the relation with observational equivalence. In fact, to even define observational equivalence, unless you have nontermination, you need some positive ground type (naturals, booleans) to use for observations.</p>

<p>However, the key theorem (PFPL 47.6, 48.3, 49.2) to relate the two relations is proven independently from the specific language:</p>

<blockquote>
  <p>Observational equivalence is the coarsest consistent congruence on expressions.</p>
</blockquote>

<p>Then, to show that logical equivalence implies observational equivalence, one only need show that logical equivalence is a consistent congruence. However, the other direction requires some more work: in particular, to show that logical equivalence is a congruence, one does proceed by induction on contexts.</p>

<p>EDIT: there's a big problem with this approach: you wouldn't get <code>n + 1 = 1 + n</code>. Let <code>VecN n</code> be the type of vectors of naturals of length <code>n</code> (assuming that can be defined or encoded), and consider using <code>VecN</code> as a context (well, you'd need in fact a context ending in <code>VecN</code>, but bear with me). Since $n + 1 = 1 + n$ is not a definitional equivalence, types <code>Vec (n + 1)</code> and <code>Vec (1 + n)</code> are incompatible, hence <code>n + 1</code> and <code>1 + n</code> are not observationally equivalent.</p>

CC BY-SA 3.0
2015-03-07T09:44:25.703Z
2016-03-18T13:28:29.557Z
2016-03-18T13:28:29.557Z
Blaisorblade
<p>For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to use the notion, not to investigate it for its own sake.</p>

<p>This notion should be "<em>extensional</em>" — in particular, to prove that $t_1 \cong t_2$, it should be enough to prove that $t_1\; v \cong t_2\; v$ for all values $v$ of the appropriate type.</p>

<h2>Denotational equivalence</h2>

<p>Denotational equivalence easily satisfies all the right lemmas, but a denotational semantics for arbitrary PTS seems rather challenging — it'd appear hard already for System F.</p>

<h2>Contextual/observational equivalence</h2>

<p>The obvious alternative are then various forms of contextual equivalence (two terms are equivalent if no ground context can distinguish them), but its definition is not immediately usable; the various lemmas aren't trivial to prove. Have they been proved for PTS? Alternatively, would the theory be an "obvious extension", or is there reason to believe the theory would be significantly different?</p>

<p>EDIT: I didn't say what's hard above.</p>

<h3>Easy part: the definition</h3>

<p>Defining the equivalence is not too hard, and the definition appears in many papers (starting at least from Plotkin 1975's study of PCF, if not earlier — the source might be Morris's PhD thesis from 1968).
We $t_1 \cong t_2$ if for all <em>ground</em> contexts $C$, $C[t_1] \simeq C[t_2]$ — that is, $C[t_1]$ and $C[t_2]$ give the same <em>result</em>. You have a few choices here with lots of alternatives: For instance, in a strongly normalizing language, if you have a ground type of naturals, you can say that ground contexts are the ones that return naturals, and then $a \simeq b$ means that $a$ and $b$ evaluate to the same number. With nontermination, for reasonable languages it is enough to use "X terminates" as observation, because if two programs are equivalent when observing termination, they're also equivalent when observing the result.</p>

<h3>Hard part: the proofs</h3>

<p>However, those papers often don't explain how hard it is to actually use this definition. All the references below show how to deal with this problem that, but the needed theory is harder than one thinks. How do we prove that $t_1 \cong t_2$? Do we actually do case analysis and induction on contexts? You don't want to do that.</p>

<p>As Martin Berger points out, you want to use, instead, either bisimulation (as done by Pitts) or a logical equivalence relation (that Harper simply calls "logical equivalence").</p>

<p>Finally, how do you prove extensionality as defined above?</p>

<p>Harper solves these questions in 10 pages for System T, through considerable cleverness and logical relations. Pitts takes more. Some languages are yet more complex.</p>

<h2>How to deal with this</h2>

<p>I'm actually tempted to make my proofs conditionally on a conjectured theory of equivalence for PTS, but the actual theories require nontrivial arguments, so I'm not sure how likely such a conjecture would be to hold.</p>

<p>I'm aware (though not in detail) of the following works:</p>

<ul>
<li>Andrew Pitts (for instance in ATTAPL for an extended System F, and in a few papers, such as the 58-page "Operationally-Based Theories of Program Equivalence").</li>
<li>Practical Foundations of Programming Languages (chapters 47-48), which is inspired by Pitts (but claims to have simpler proofs).</li>
<li><a href="http://www.theses.fr/2014EMNA0124">A logical study of program equivalence</a>. I can't find an English abstract, but it seems to spend a great deal of effort for side effects (references), which seems an orthogonal complication.</li>
</ul>

CC BY-SA 3.0
2015-03-06T15:47:29.710Z
For type-theories defining an operational contextual congruence should be easy, since the programs all terminate. Define a notion of observation at a base type (e.g. termination, written $\Downarrow$, at type Unit), and then say $P \cong Q$ for all well-typed and closing contexts $C[\cdot]$ of base type, we have $C[P] \Downarrow$ iff $C[Q] \Downarrow$. With PTSs it's a bit more complicated, as may get non-termination.
Martin Berger
CC BY-SA 3.0
2015-03-06T19:36:11.777Z
@MartinBerger: that's the idea I'm hinting at, but proving it directly is suprisingly hard, because you need to do proofs for all C (I'll explain that better in the question). Also, if all programs terminate, the definition you use, as given, identifies all programs.
Blaisorblade
CC BY-SA 3.0
2015-03-06T19:41:55.217Z
Does your PTS only have functions as computational types? If then, then [this excellent question (and answers)](http://cstheory.stackexchange.com/questions/17636/%CE%B7-conversion-vs-extensionality-in-extensions-of-lambda-calculus) seems to indicate that $\beta\eta$-equivalence is enough for *terminating* pure type systems -- and it nicely explains how to define contextual equivalence for terminating calculi. I think using ground values is *the right way* to define contextual equivalence, and termination is only a convenient shortcut of dubious merit.
gasche
CC BY-SA 3.0
2015-03-06T20:21:48.483Z
@gasche: thanks for the compliment to my question, but I'll need naturals and more (I'm trying to generalize ILC to a language bigger than STLC, and Cai is approaching the question using PTSs). But the problem is not the definition of contextual equivalence — see my edits clarifying what's hard.
Blaisorblade
CC BY-SA 3.0
2015-03-06T20:50:20.693Z
@Blaisorblade Sorry yes, if you use termination as observable, then you are right. Sorry, I was cutting and pasting the definition for turing complete deterministic languages. If you have terminating functions you can use a different basic observable. For example at booleans: ... $C[P] \Downarrow true$ iff $C[Q] \Downarrow true$. The quantification over all contexts is always a problem. The standard way of dealing with it is to define a second relation that (1) is sound w.r.t. $\cong$ and (2)  easy to handle, e.g. some notion of bisimilarity, or logical relation. Depends on the application.
Martin Berger
CC BY-SA 3.0
2015-03-06T20:52:58.343Z
In my experience showing equivalences between programs is considerably easier if everything terminates, because then you can use induction on the length of derivations as a proof technique. But it's always a bit of a struggle.
Martin Berger
CC BY-SA 3.0
2015-03-06T21:31:42.343Z
To prove that $t_1~s_1 \equiv t_2~s_2$, you use transitivity: first $t_1~s_1 \equiv t_1~s_2$ (context $t_1~\square$) then $t_1~s_2 \equiv t_2~s_2$ (context $\square~s_2$).
gasche
CC BY-SA 3.0
2015-03-06T22:12:23.530Z
@gasche: you're right of course — and I did that yesterday in a minute! I shouldn't try to make up examples on the spot.
Blaisorblade
CC BY-SA 3.0
2015-03-06T22:54:47.993Z
@MartinBerger: When you say "the standard way", it sounds like we'd probably have to do this on our own for PTS :-(. I'll take a look.
Blaisorblade
CC BY-SA 3.0
2015-03-06T23:01:34.777Z
@Blaisorblade Probably. Concurrency theorists have been doing this intensively for a long time, because with concurrent processes it's a lot less clear what notion of equivalence to use. This has lead to a division of labour: use a reduction based semantics with quantification over contexts to define the notion of equivalence and then use bisimulations or traces over labelled transitions to prove equivalence (or the absence thereof). A big open research question in concurrency theory is how to go from a the former to the latter algorithmically.
Martin Berger
CC BY-SA 3.0
2015-03-07T01:25:33.200Z
@Blaisorblade In my experience it's worthwhile to tailor the sound approximation of the canonical congruence to the theorem to be proved: use as weak an approximation as you can get away with. That tends to simpify proofs.
Martin Berger
CC BY-SA 3.0
2015-03-07T02:13:52.337Z
Thanks. Luckily I'm not dealing with concurrency (my language is very boring) — in fact, it seems that the logical equivalence I need is the one used in the theory of parametricity (PFPL, Chapter 49). Since parametricity has been extended to (consistent) PTSs (by Bernardy and Lasson), it should be possible to get the lemmas I need.
Blaisorblade
<pl.programming-languages><type-theory><operational-semantics>
For what languages is there already a theory of observational equivalence?
Blaisorblade
# For what languages is there already a theory of observational equivalence?

(Asked by: username_0 on 2015-03-06)

For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to use the notion, not to investigate it for its own sake.

This notion should be "*extensional*" — in particular, to prove that $t\_1 \cong t\_2$, it should be enough to prove that $t\_1\; v \cong t\_2\; v$ for all values $v$ of the appropriate type.

## Denotational equivalence

Denotational equivalence easily satisfies all the right lemmas, but a denotational semantics for arbitrary PTS seems rather challenging — it'd appear hard already for System F.

## Contextual/observational equivalence

The obvious alternative are then various forms of contextual equivalence (two terms are equivalent if no ground context can distinguish them), but its definition is not immediately usable; the various lemmas aren't trivial to prove. Have they been proved for PTS? Alternatively, would the theory be an "obvious extension", or is there reason to believe the theory would be significantly different?

EDIT: I didn't say what's hard above.

### Easy part: the definition

Defining the equivalence is not too hard, and the definition appears in many papers (starting at least from Plotkin 1975's study of PCF, if not earlier — the source might be Morris's PhD thesis from 1968).
We $t\_1 \cong t\_2$ if for all *ground* contexts $C$, $C[t\_1] \simeq C[t\_2]$ — that is, $C[t\_1]$ and $C[t\_2]$ give the same *result*. You have a few choices here with lots of alternatives: For instance, in a strongly normalizing language, if you have a ground type of naturals, you can say that ground contexts are the ones that return naturals, and then $a \simeq b$ means that $a$ and $b$ evaluate to the same number. With nontermination, for reasonable languages it is enough to use "X terminates" as observation, because if two programs are equivalent when observing termination, they're also equivalent when observing the result.

### Hard part: the proofs

However, those papers often don't explain how hard it is to actually use this definition. All the references below show how to deal with this problem that, but the needed theory is harder than one thinks. How do we prove that $t\_1 \cong t\_2$? Do we actually do case analysis and induction on contexts? You don't want to do that.

As username_1 points out, you want to use, instead, either bisimulation (as done by Pitts) or a logical equivalence relation (that Harper simply calls "logical equivalence").

Finally, how do you prove extensionality as defined above?

Harper solves these questions in 10 pages for System T, through considerable cleverness and logical relations. Pitts takes more. Some languages are yet more complex.

## How to deal with this

I'm actually tempted to make my proofs conditionally on a conjectured theory of equivalence for PTS, but the actual theories require nontrivial arguments, so I'm not sure how likely such a conjecture would be to hold.

I'm aware (though not in detail) of the following works:

* Andrew Pitts (for instance in ATTAPL for an extended System F, and in a few papers, such as the 58-page "Operationally-Based Theories of Program Equivalence").
* Practical Foundations of Programming Languages (chapters 47-48), which is inspired by Pitts (but claims to have simpler proofs).
* [A logical study of program equivalence](http://www.theses.fr/2014EMNA0124). I can't find an English abstract, but it seems to spend a great deal of effort for side effects (references), which seems an orthogonal complication.

**Tags:** pl.programming-languages, type-theory, operational-semantics

> **Comments:**
> **username_1**: For type-theories defining an operational contextual congruence should be easy, since the programs all terminate. Define a notion of observation at a base type (e.g. termination, written $\Downarrow$, at type Unit), and then say $P \cong Q$ for all well-typed and closing contexts $C[\cdot]$ of base type, we have $C[P] \Downarrow$ iff $C[Q] \Downarrow$. With PTSs it's a bit more complicated, as may get non-termination.  
> **username_0**: @MartinBerger: that's the idea I'm hinting at, but proving it directly is suprisingly hard, because you need to do proofs for all C (I'll explain that better in the question). Also, if all programs terminate, the definition you use, as given, identifies all programs.  
> **username_2**: Does your PTS only have functions as computational types? If then, then [this excellent question (and answers)](http://cstheory.stackexchange.com/questions/17636/%CE%B7-conversion-vs-extensionality-in-extensions-of-lambda-calculus) seems to indicate that $\beta\eta$-equivalence is enough for *terminating* pure type systems -- and it nicely explains how to define contextual equivalence for terminating calculi. I think using ground values is *the right way* to define contextual equivalence, and termination is only a convenient shortcut of dubious merit.  
> **username_0**: @username_2: thanks for the compliment to my question, but I'll need naturals and more (I'm trying to generalize ILC to a language bigger than STLC, and Cai is approaching the question using PTSs). But the problem is not the definition of contextual equivalence — see my edits clarifying what's hard.  
> **username_1**: @username_0 Sorry yes, if you use termination as observable, then you are right. Sorry, I was cutting and pasting the definition for turing complete deterministic languages. If you have terminating functions you can use a different basic observable. For example at booleans: ... $C[P] \Downarrow true$ iff $C[Q] \Downarrow true$. The quantification over all contexts is always a problem. The standard way of dealing with it is to define a second relation that (1) is sound w.r.t. $\cong$ and (2)  easy to handle, e.g. some notion of bisimilarity, or logical relation. Depends on the application.  
> **username_1**: In my experience showing equivalences between programs is considerably easier if everything terminates, because then you can use induction on the length of derivations as a proof technique. But it's always a bit of a struggle.  
> **username_2**: To prove that $t_1~s_1 \equiv t_2~s_2$, you use transitivity: first $t_1~s_1 \equiv t_1~s_2$ (context $t_1~\square$) then $t_1~s_2 \equiv t_2~s_2$ (context $\square~s_2$).  
> **username_0**: @username_2: you're right of course — and I did that yesterday in a minute! I shouldn't try to make up examples on the spot.  
> **username_0**: @MartinBerger: When you say "the standard way", it sounds like we'd probably have to do this on our own for PTS :-(. I'll take a look.  
> **username_1**: @username_0 Probably. Concurrency theorists have been doing this intensively for a long time, because with concurrent processes it's a lot less clear what notion of equivalence to use. This has lead to a division of labour: use a reduction based semantics with quantification over contexts to define the notion of equivalence and then use bisimulations or traces over labelled transitions to prove equivalence (or the absence thereof). A big open research question in concurrency theory is how to go from a the former to the latter algorithmically.  
> **username_1**: @username_0 In my experience it's worthwhile to tailor the sound approximation of the canonical congruence to the theorem to be proved: use as weak an approximation as you can get away with. That tends to simpify proofs.  
> **username_0**: Thanks. Luckily I'm not dealing with concurrency (my language is very boring) — in fact, it seems that the logical equivalence I need is the one used in the theory of parametricity (PFPL, Chapter 49). Since parametricity has been extended to (consistent) PTSs (by Bernardy and Lasson), it should be possible to get the lemmas I need.  

---

## 3 answers

### Answer by username_3 on 2015-03-07. Score: 5

A compositional denotational semantics $[\![ {-} ]\!]$ of a programming language (a domain-theoretic or game-theoretic one, for instance) is **adequate** if semantically equal terms imply that they are observationally equivalent:
$$[\![ t\_1 ]\!] = [\![ t\_2 ]\!] \implies t\_1 \cong t\_2.$$
It often happens that it is far easier to calculate denotations that to prove observational equivalence. This is a common technique with many known variants. Adequacy is defined already in Plotkin's PCF paper.

> **Comments:**
> **username_1**: There is no particular need for the adequate semantics to use some other formalism. You can also soundly approximate $\cong$ within the programming language under discussion, e.g. using operational methods.  
> **username_0**: Thanks for the answer, but -1: While I agree, the question mentions pure type systems — AFAICS, a denotational semantics for pure type systems is an open problem, so I think an answer should point to some denotational semantics. (In fact, if I had a denotational semantics, I'd dispense with the operational one altogether, as mentioned in the question). (But sorry for the overly long question.)  
> **username_3**: @MartinBerger, I do not understand your criticism. The OP asks for methods of showing observational equivalence, I mention a common one, and then you object that other ways exist which avoid the method?  
> **username_3**: @username_0, well then you'll just have to invent a denotational semantics for pure type systems, won't you? :-) But more seriously, I'll ask Alex Simpson, he would know better about denotational semantics for such things.  
> **username_1**: @AndrejBauer It wasn't meant to be a criticism, more as an addendum.  
> **username_0**: @AndrejBauer Conjecture: you can collapse arbitrary PTSs to $\lambda^*$ and use the existing denotational semantics (based on domain theory) for the latter. I assume the result won't be fully abstract most of the time, but that's probably still useful enough for some purposes.  

---

### Answer by username_4 on 2015-03-09. Score: 3

The domain and model theories of PTSes hasn't been explored all that much I'm afraid. One detailed source is Thomas Streicher's PhD work: [Semantics of Type Theory](http://link.springer.com/book/10.1007%2F978-1-4612-0433-6). He gives category theoretic semantics for all PTS, though I'm not sure he addresses $\eta$-conversion.

> **Comments:**
> **username_1**: I don't think Streicher's PhD is about PTS. It's about semantics of the Calculus of Constructions and independence results via reliability semantics. See [here](http://goo.gl/cdaqE7).  
> **username_4**: Thanks for the clarification! I'm afraid the link is broken though (and hard to fix with the minified link).  
> **username_1**: The link was to table of content of the book [here](http://link.springer.com/book/10.1007%2F978-1-4612-0433-6). I hope this one works better.  
> **username_0**: @MartinBerger: thanks for the clarification! I'll go back to assuming that a semantics for arbitrary PTSs (ranging to System U and $\lambda^*$ and all their pathologies) is beyond our reach.  
> **username_5**: @MartinBerger: do you mean realizability semantics?  
> **username_1**: @DominiqueDevriese Yes, of course. Autocorrect always catches me off-guard. Thanks for pointing this out.  
> **username_4**: @username_0 just to be clear, domain theoretic semantics are somewhat impervious to non-termination issues such as occur in system U and its ilk. In general, there are models of polymorphic theories in domains, see e.g. Coquand *et al* "Domain theoretic models of polymorphism". I don't think there is any *theoretical* objection to extending this to arbitrary PTSes, just the work hasn't really been done. Of course, I would be more interested in models capable of implying normalization, but those *do* run into problems for system U.  
> **username_0**: username_4: I wasn't expecting difficulties for any given PTS due to non-termination, but giving _one_ semantics parametric in multiple ones seems harder — how many universes are you going to need?  What's more worrisome is that your semantics must be impervious to impredicativity issues. Luckily domain theory lets you solve arbitrary mixed-variance fixpoint equations, and I guess that might help; I'm currently using the other approach to those equations (based on Birkedal et al.'s work on ultrametric spaces/step-indexing) for a different impredicative system.  

---

### Answer by username_0 on 2015-03-07. Score: 1

This answer suggests an approach to the problem. (Feedback is welcome).

PFPL chapter 49 discusses, at once, the equivalent notions of observational equivalence and logical equivalence. Logical equivalence is the same relation used to state parametricity, so the core of the chapter is a proof of parametricity for System F.

Work on parametricity for PTS, AFAICT, does not discuss the relation with observational equivalence. In fact, to even define observational equivalence, unless you have nontermination, you need some positive ground type (naturals, booleans) to use for observations.

However, the key theorem (PFPL 47.6, 48.3, 49.2) to relate the two relations is proven independently from the specific language:

> Observational equivalence is the coarsest consistent congruence on expressions.

Then, to show that logical equivalence implies observational equivalence, one only need show that logical equivalence is a consistent congruence. However, the other direction requires some more work: in particular, to show that logical equivalence is a congruence, one does proceed by induction on contexts.

EDIT: there's a big problem with this approach: you wouldn't get `n + 1 = 1 + n`. Let `VecN n` be the type of vectors of naturals of length `n` (assuming that can be defined or encoded), and consider using `VecN` as a context (well, you'd need in fact a context ending in `VecN`, but bear with me). Since $n + 1 = 1 + n$ is not a definitional equivalence, types `Vec (n + 1)` and `Vec (1 + n)` are incompatible, hence `n + 1` and `1 + n` are not observationally equivalent.


---

