% Girard-Reynolds isomorphism % based on Wadler's paper % Kevin Watkins % April 2005 % Wadler's "F2" tp : type. % Types tm : tp -> type. % Terms of a given type => : tp -> tp -> tp. % Function arrow %infix right 8 =>. ! : (tp -> tp) -> tp. % Forall \ : (tm A -> tm B) -> tm (A => B). @ : tm (A => B) -> tm A -> tm B. %infix left 7 @. gen : ({X:tp} tm (B X)) -> tm (![X] B X). inst : tm (![X] B X) -> {A:tp} tm (B A). %infix left 7 inst. % Another way to think about F2 is as the pure type system % tp : kd % (tp, tp, tp) % (kd, tp, tp) % Wadler's "P2" % This is not actually a system treated in Girard's thesis, as % far as I can tell. o : type. % Propositions pf : o -> type. % Proofs of a given proposition % In LF there's no need for an explicit syntax of predicates; % they're just LF functions from terms to propositions. % This has the effect of internalizing beta- and eta-equivalences % over predicates into LF's own notion of equality. pr : tp -> type = [A] tm A -> o. --> : o -> o -> o. % Implies %infix right 3 -->. tp! : (tp -> o) -> o. % Forall (types) tm! : (tm C -> o) -> o. % Forall (terms of a given type) pr! : (pr C -> o) -> o. % Forall (predicates over a given type) lam : (pf A -> pf B) -> pf (A --> B). app : pf (A --> B) -> pf A -> pf B. %infix left 1 app. tpgen : ({X:tp} pf (B X)) -> pf (tp![X] B X). tpinst : pf (tp![X] B X) -> {A:tp} pf (B A). %infix left 1 tpinst. tmgen : ({x:tm C} pf (B x)) -> pf (tm![x] B x). tminst : pf (tm![x] B x) -> {t:tm C} pf (B t). %infix left 1 tminst. prgen : ({X:pr C} pf (B X)) -> pf (pr![X] B X). prinst : pf (pr![X] B X) -> {A:pr C} pf (B A). %infix left 1 prinst. % Irritatingly, Wadler's paper is not precise about the congruences % for beta equivalence. I adopt the most restrictive interpretation. % Since we have quantification over predicates, these could also be % modeled as equalities within the logic itself. beta : {C} pf (C ((\[x] T x) @ U)) -> pf (C (T U)). instbeta : {C} pf (C ((gen[x] T x) inst A)) -> pf (C (T A)). % Combinators for conversions %abbrev at : ({C:pr A} pf (C T) -> pf (C U)) -> {C:pr A} pf (C T) -> pf (C U) = [cnv] cnv. %infix left 2 at. %abbrev conv : pf A -> (pf A -> pf B) -> pf B = [d] [e] e d. %infix left 1 conv. %abbrev rev : ({C:pr A} pf (C T) -> pf (C U)) -> ({C:pr A} pf (C U) -> pf (C T)) = [cnv] [C] [d] (lam[x] x) conv cnv at ([h] C h --> C T) app d. % The conversions on proofs are tedious, so I'm not representing them. % P2 seems to be related to the PTS % tp : kd % (tp, tp, tp) % (kd, tp, tp) % o : ltp (logical types) % (o, o, o) % (ltp, o, o) % (tp, ltp, ltp) % (tp, o, o) % (kd, o, o) % The system U does come up in Girard's thesis, where it's proved % inconsistent. I think the relevant fragment of U in PTS would be % tp : kd % (tp, tp, tp) % (kd, tp, tp) % o : tp % (o, o, o) % (tp, o, o) % Simulations of nullary and binary predicates 1 : tp = ![X] X => X. unit : tm 1 = gen[X] \[x] x. %abbrev nullary : o -> pr 1 = [C] [x] C. % The beta-conversion for nullary predicates listed in Wadler's paper % is internalized by LF's notion of equality. * : tp -> tp -> tp = [A] [B] ![X] (A => B => X) => X. %infix left 10 *. pair : tm A -> tm B -> tm (A * B) = [t] [u] gen[X] \[k] k @ t @ u. fst : tm (A * B) -> tm A = [s] s inst A @ (\[x] \[y] x). snd : tm (A * B) -> tm B = [s] s inst B @ (\[x] \[y] y). %abbrev binary : (tm A -> tm B -> o) -> pr (A * B) = [C] [z] C (fst z) (snd z). %abbrev fstbeta : {C} pf (C (fst (pair T U))) -> pf (C T) = [C] [d] d conv instbeta at ([h] C (h @ (\[x] \[y] x))) conv beta at ([h] C h) conv beta at ([h] C (h @ U)) conv beta at ([h] C h). %abbrev sndbeta : {C} pf (C (snd (pair T U))) -> pf (C U) = [C] [d] d conv instbeta at ([h] C (h @ (\[x] \[y] y))) conv beta at ([h] C h) conv beta at ([h] C (h @ U)) conv beta at ([h] C h). %abbrev binarybeta : {C} pf (C (binary Pred (pair T U))) -> pf (C (Pred T U)) = [C] [d] d conv fstbeta at ([h] C (Pred h (snd (pair T U)))) conv sndbeta at ([h] C (Pred T h)). % Definitions of other logical connectives true : o = pr![X] X unit --> X unit. false : o = pr![X] X unit. && : o -> o -> o = [A] [B] pr![X] (A --> B --> X unit) --> X unit. %infix left 5 &&. || : o -> o -> o = [A] [B] pr![X] (A --> X unit) --> (B --> X unit) --> X unit. %infix left 4 ||. <-> : o -> o -> o = [A] [B] (A --> B) && (B --> A). %infix none 3 <->. % Relations on predicates <= : pr A -> pr A -> o = [A] [B] tm![x] A x --> B x. %infix none 6 <=. pr== : pr A -> pr A -> o = [A] [B] A <= B && B <= A. %infix none 6 pr==. % Leibniz equality == : tm A -> tm A -> o = [t] [u] pr![X] X t --> X u. %infix none 6 ==. refl : pf (T == T) = prgen[X] lam[x] x. sym : pf (T == U) -> pf (U == T) = [d] d prinst ([x] x == T) app refl. trans : pf (T == U) -> pf (U == V) -> pf (T == V) = [d] [e] prgen[X] lam[x] e prinst X app (d prinst X app x). ==beta : pf ((\[x] T x) @ U == T U) = prgen[X] lam[x] x conv beta at ([h] X h). % Generally, in LF it's better to use meta-congruences than this sort % of extensionality axiom, but I'm too lazy to modify Wadler's treatment. ext : pf (tm![f] tm![g] (tm![x] f @ x == g @ x) --> f == g). tpext : pf (tm![f] tm![g] (tp![X] f inst X == g inst X) --> f == g). % The "Girard projection" % Judgments o# : o -> tp -> type. pr# : pr A -> tp -> type. pf# : pf A -> tm A# -> type. % The projection of propositions --># : o# (A --> B) (A# => B#) <- o# A A# <- o# B B#. tp!# : o# (tp![X] A X) A# <- {X} o# (A X) A#. tm!# : o# (tm![x] A x) A# <- {x} o# (A x) A#. pr!# : o# (pr![X] A X) (![X#] A# X#) <- ({X} {X#} pr# X X# -> o# (A X) (A# X#)). % The projection of predicates % This is slightly awkward (it doesn't mode check) pred# : o# (A T) A# <- pr# A A#. % The projection of proofs lam# : pf# (lam[x] U x) (\[x#] U# x#) <- ({x} {x#} pf# x x# -> pf# (U x) (U# x#)). app# : pf# (S app T) (S# @ T#) <- pf# S S# <- pf# T T#. tpgen# : pf# (tpgen[X] U X) U# <- ({X} pf# (U X) U#). tpinst# : pf# (S tpinst T) S# <- pf# S S#. tmgen# : pf# (tmgen[x] U x) U# <- ({x} pf# (U x) U#). tminst# : pf# (S tminst T) S# <- pf# S S#. prgen# : pf# (prgen[X] U X) (gen[X#] U# X#) <- ({X} {X#} pr# X X# -> pf# (U X) (U# X#)). prinst# : pf# (U prinst X) (U# inst X#) <- pf# U U# <- ({x} o# (X x) X#). % Wadler's paper leaves out projections for the extensionality axioms. % However, they are probably trivial, because every term equality % (T == U) projects to the unit type, as Twelf can demonstrate: %solve _ : o# (T == U) 1. % The "Reynolds embedding" % This turns into a bit of a nightmare for Twelf's term reconstruction % engine unless you annotate heavily. % Judgments tp\$ : {X:tp} pr X -> type. tm\$ : tm A -> pf A\$ -> type. % The embedding of types =>\$ : tp\$ (A => B) ([z] tm![x] A\$ x --> B\$ (z @ x)) <- tp\$ A A\$ <- tp\$ B B\$. !\$ : tp\$ (![X] B X) ([z] tp![X] pr![X\$] B\$ X X\$ (z inst X)) <- ({X} {X\$} tp\$ X X\$ -> tp\$ (B X) (B\$ X X\$)). % The embedding of terms \\$ : tm\$ (\[x] U x) (tmgen[x] lam[x\$] U\$ x x\$ conv rev beta at ([h] B\$ h) : pf (B\$ ((\[x] U x) @ x))) <- ({x} {x\$} tm\$ x (x\$ : pf (A\$ x)) -> tm\$ (U x) (U\$ x x\$ : pf (B\$ (U x)))). @\$ : tm\$ (S @ T) (S\$ tminst T app T\$) <- tm\$ S (S\$ : pf (tm![x] A\$ x --> B\$ (S @ x))) <- tm\$ T (T\$ : pf (A\$ T)). gen\$ : tm\$ (gen[X] U X) (tpgen[X] prgen[X\$] U\$ X X\$ conv rev instbeta at ([h] B\$ X X\$ h) : pf (B\$ X X\$ ((gen[X] U X) inst X))) <- ({X} {X\$} tp\$ X X\$ -> tm\$ (U X) (U\$ X X\$ : pf (B\$ X X\$ (U X)))). inst\$ : tm\$ (S inst A) (S\$ tpinst A prinst A\$) <- tm\$ S (S\$ : pf (tp![X] pr![X\$:pr X] B\$ X X\$)) <- tp\$ A A\$. % Note that I haven't sanity checked Twelf's reconstructions for % either translation. They might be excessively general, requiring % further annotations.