Contextual Equivalence & Privacy Equation

Privacy Equation

最近出现的地方：Probabilistic programming semantics for name generation

最开始是Andrew Pitts & Ian Stark 93 的 paper, Example 4(3) （其实这个paper里面的denotational model也不能证明这个ctx equiv，需要SIPL那篇paper）

Also Ian Stark’s PhD thesis, chap 2, section 5, example 13

写在iris里差不多长这样

From iris.proofmode Require Import proofmode.
From reloc Require Import reloc.
Set Default Proof Using "Type".

Definition prog1: expr :=
  let: "x" := ref #() in
  let: "y" := ref #() in
  (λ: "f" (* unit ref -> bool *), "f" "x" = "f" "y").

Definition prog2 : expr :=
  (λ: "f", #true).

（这个在reloc里面是证不了的） 因为f可以non-deterministic

就算你的language是deterministic和terminating的（eg: system F with first order state¹） 你也不能证明这个ctx eq 比如

f = let: "a" := ref #true in
    \lambda _.
    match "a" with
    | #true -> "a" <- #false ;; !"a"
    | #false -> "a" <- #true ;; !"a"

Contextual Equivalence

这个line of work感觉folklore挺多的。。。

Bob Harper的PFPL管这个叫observational equivalence 但是其实跟general的contextual equivalence（在non-terminating的语言中）通常以termination作为observable event:

The extension of System F with a “positive” (inductively defined) observable type appears to be needed to even define observational equivalence, but this point seems not to have been made elsewhere in the literature. - PFPL 48.6 (p.466)

Andrew Pitts’ argument for using termination as observable events:

But what if I had used a different interpreter—would it affect the notion of contextual equivalence? Probably not. Evidence for this is given by the fact that we can replace obs by a constant function and still get the same notion of contextual equivalence (see Exercise B.3). In other words, rather than observing particular things about the final results of evaluation, we can just as well observe the fact that there is some final result at all, i.e. observe termination of evaluation. This gives us the following definition of contextual equivalence. - Operational Semantics and Program Equivalence, Applied Semantics, 2000