Exchange lemma

Exchange is the property of a hypothetical judgment that if $\Gamma, A, B \vdash J$, then $\Gamma, B, A \vdash J$ (assuming A and B are independent hypotheses).

Often, we represent an an object-language hypothetical judgement by using LF binding to model hypotheses. When a judgement is represented in such a fashion, exchange comes “for free” from the LF representation. In particular, we can exchange hypotheses by re-arranging the order of the lambdas in a derivation.

For example, consider the following simply typed λ-calculus:

%% Syntax
%sort tp %.
%term tp/unit tp %.
%term tp/arrow %pi tp %-> tp %-> tp %.
%sort exp %.
%term exp/unit exp %.
%term exp/lam %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term exp/app %pi exp %-> exp %-> exp %.
%% Typing
%sort of {_ exp} {_ tp} %.
%term of/unit of exp/unit tp/unit %.
%term of/lam
  %pi (of (exp/lam T E) (tp/arrow T T'))
  %<- ({x exp} %pi (of x T) %-> (of (E x) T')) %.
%term of/app %pi (of (exp/app E1 E2) T') %<- (of E2 T) %<- (of E1 (tp/arrow T T')) %.

Object-language typing is a hypothetical judgement; we represent it using LF variables to model hypotheses (see Representing the judgements of the STLC for more discussion of this representation).

We can prove exchange for this judgement as follows:

%sort exchange {_ {x exp} {dx of x T} {y exp} {dy of y T'} of (E x y) T''} {_ {y exp} {dy of y T'} {x exp} {dx of x T} of (E x y) T''} %.
%mode exchange %in %out %.
%term _ exchange ([x] [dx of x T] [y] [dy of y T'] D1 x dx y dy) ([y] [dy of y T'] [x] [dx of x T] D1 x dx y dy) %.
%block of-block [T tp] {x exp} {dx of x T}%.
%worlds (of-block) (exchange _ _) %.
%total {} (exchange _ _) %.