• Hereditary Termination and Logical Equivalence Recap
• Extension to Polymorphic Types
  • System T - Extend to F
• Logical Equivalence of Polymorphic Types
  • “Admissible Relation”
  • Formal Definition
• Main Theorm
• Existential Type

Hereditary Termination:

• $HT_{tau}(e)$ hereditary termination at type $tau$
• $HT_{nat}(e)$ $iff $$emapsto^*z$ or $emapsto^*s(e’)$ such that $HT_{nat}(e’)$ (inductively defined)
• $HT_{tau_1rightarrowtau_2}(e)$ $iff $$if HT_{tau_1}(e_1) then HT_{tau_2}(e(e_1))$ (implication)

Logical Equivalence:

• $esim_{nat}e’$ $iff $either $emapsto^*n^*leftarrow e’$ or $emapsto^*s(e_1),e’mapsto^*s(e_1’),e_1sim_{nat}e_1’$
• $esim_{tau_1rightarrowtau_2}e’$ $iff $$if e_1sim_{tau_1}e_1’ then e(e_1)sim_{tau_2}e’(e_1’)$

Some theorem:

• $e:tau implies esim_{nat} e$
• $esim_{tau}e’$ $iff$ $esimeq_{tau}e’$
• $esim_{tau}e iff HT_{tau}(e)$

Extension to Polymorphic Types

System T - Extend to F

$$tau ::= nat|tau_1rightarrowtau_2|forall t.tau|t(variable type)\ e ::=x...|Lambda t.e(type abstraction)|e[tau](type application)$$

Now that we can define Existential Type in system F (client is polymorphic):

$$exists t.tau:=forall u(forall t.taurightarrow u)rightarrow u$$

Logical Equivalence of Polymorphic Types

We can do the following:

$$esim_{forall t.tau}e' iff forallsigma(small)type,e[sigma]sim_{[sigma/t]tau}e'[sigma]$$

But this is saying type variables range over type expression, which is not what we want.

We want to say type variables range over all conceivable types (not sure the ones
you can write down)

Idea: types are certain relations!

“Admissible Relation”

1. domain type $tau_1$
2. range type $tau_2$
3. binary relations between exp’s of those types $R:tau_1leftrightarrowtau_2$

• Exact definition varies with application language
• Demand respect observational equality:

$$e_1Re_2,e_1cong e_1',e_2cong e_2' iff e_1'Re_2'$$

Getting back to equiv. of polymorphic types using our admissible relations. The idea
is approximately to say:

$$esim_{forall t.tau}e' iff "forall R admissible esim_{tau}e' modulo t=R"$$

In order to make this precise we have to define a more general relation which is
heterogeneous.

Formal Definition

Define:

$$esim_tau e'[eta:deltaleftrightarrowdelta']$$

idea:

$$delta:t_1mapstosigma_1,...,t_nmapstosigma_n \ delta:t_1mapstosigma_1',...,t_nmapstosigma_n' \ eta:t_1mapsto R_1sigma_1leftrightarrowsigma_1',...,t_nmapsto R_nsigma_nleftrightarrowsigma_n' (R is admissible relation)\ e:hat{delta}(tau),e':hat{delta'}(tau) (e and e' are disparate types)\$$

1. $esim_t e’[eta:deltaleftrightarrowdelta’] iff eeta(t)e’ (sigma(t)leftrightarrowsigma’(t))$
2. $esim_{nat} e’[eta:deltaleftrightarrowdelta’] iff (emapsto^* z and e’mapsto^* z)or(emapsto^* s(e_1),e’mapsto^* s(e_1’),e_1sim_{nat}e_1’[eta:deltaleftrightarrowdelta’])$
3. $esim_{tau_1rightarrowtau_2}e’[eta:deltaleftrightarrowdelta’] iff e_1sim_{tau_1}e_1’[eta]supset e(e_1)sim_{tau1}e’(e_1’)[eta]$
4. $esim_{forall t.tau}e’[eta] iff forallsigma,sigma’forall R:sigmaleftrightarrowsigma’ admissible,e[sigma]sim_tau e[sigma’] [eta[tmapsto R]:delta[tmapstosigma]leftrightarrowdelta’[tmapstosigma’]]$ (Note that $tau$ in $sim_tau$ has free $t$’s in it and $tau$ is a piece of $forall t.tau$!)

Main Theorm

In system F:

$$If e:tau,then esim_tau e'[emptyset]$$

And there is Identity Extension:

“If all type variables are interpreted as obs. equiv., then logically related things
are obs. equiv.”

Existential Type

We have existential type of a counter defined as

$$% <![CDATA[ exists t:<inc:trightarrow t,dec:trightarrow t,val:trightarrow nat, zero:t> %]]>$$

and we have the client of that as type:

$$forall t((trightarrow t)rightarrow(trightarrow t)rightarrow (trightarrow nat)rightarrow t rightarrow rho)$$

We have two implementation of our counter: $I$ and $II$, and their types are related by $R$
$tau_I R tau_{II}$ where $R$ means “they represent the same number”.

Because the client has that such polymorphic type, it is “uniform accross all possible t’s” by
the main theorm:

$$if\ inc_Isim_{trightarrow t}inc_{II}[tmapsto R]\ dec_Isim_{trightarrow t}dec_{II}[..]\ val_Isim_{trightarrow nat}val_{II}[..]\ zero_Isim_t zero_{II}\ then\ client[tau_I] (inc_I)(dec_I)(val_I)(zero_I)\ cong_{obs}\ client[tau_{II}] (inc_{II})(dec_{II})(val_{II})(zero_{II})\$$