2
$\begingroup$

From the text Principles of Type Refinement page 14:

The author introduces in definition 2.2.7 the rule:

$$ \dfrac{\Pi \vdash t : R \qquad R \le S}{\Pi \vdash t : S} $$

and gives the following contravariant form:

$$ \dfrac{\Omega \le \Pi \qquad \Pi: t : R}{\Omega \vdash t:R} $$

where $\Omega,\Pi \sqsubset \Gamma$ and $\Omega \le \Pi$ is interpreted as if the type assigned to each variable in $\Omega$ is a subtype of the type assigned to the same varaible in $\Pi$.

The author then states that this rule is admissible in the refined simply typed lambda calculus and that this can by shown by induction on typing derivations.

I'm used to natural and structural induction. But what does it mean to perform induction on typing derivations? Can you given an example?

$\endgroup$
3
$\begingroup$

It's a form of structural induction.

As we see on page 12 of the text, the typing relation is defined inductively by four rules.

For example, the rule abs says that given a deduction $\Gamma, x:r \vdash t : S$ we can form the new deduction $\Gamma \vdash \lambda x.t : R \to S$.

Compare with how, given a natural number $n$ you can form a new natural number $n+1$.

To prove a proposition $P(n)$ about an arbitrary natural number by induction you note that $n$ is either

  1. $0$, or
  2. $m+1$ for some $m$

In the first case, you prove $P(0)$ directly. In the second, you assume you have a proof of $P(m)$ and use this to prove $P(m+1)$.

Similarly, to prove a proposition about an arbitrary derivation $\Delta$ of the type judgement $\Pi \vdash t :R$ you note that $\Delta$ is either

  1. $ \dfrac{}{\Pi \vdash x : R}\textsf{ var}$ and $t=x$ a variable
  2. $\dfrac{\Pi \vdash s : S \to R, \Pi \vdash u : S }{\Pi \vdash s(u) : R}\textsf{ app}$ and $t=s(u)$, an application, for some derivations $\Delta_1, \Delta_2$ of the type judgements $\Pi \vdash s : S \to R, \Pi \vdash u : S $
  3. $\dfrac{\Pi, x:r \vdash s : S}{\Pi \vdash \lambda x.s : R \to S}\textsf{ abs}$ and $t=\lambda x.s$, an abstraction, for some derivation $\Delta_1$ of the type judgement $\Pi \vdash s : S$
  4. $\dfrac{\Pi \vdash t:S, R \leq R}{\Pi \vdash t : R}\textsf{ sub}$, for some supertype $S$ of $R$ and a derivation $\Delta_1$ of $\Pi \vdash t : S$

In the first case, you prove $P(\Delta)$ directly, and in the other three you assume $P(\Delta_1)$ and $P(\Delta_2)$ and then prove $P(\Delta)$.

There is an example in the proof of lemma 2.3.10 of the text, page 33.

$\endgroup$
  • $\begingroup$ As a minor addition, induction over typing derivations is usually a structural induction over an inductive family as opposed to a plain inductive type such as the naturals. So it is a bit more complicated than a "usual" structural induction. $\endgroup$ – Derek Elkins Jul 30 '18 at 0:36

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.