I'm currently going through this book about programming languages, and in section 4.2, Lemma 4.2 it says this:

Lemma 4.2 (Inversion for Typing). Suppose that $\Gamma \vdash e : \tau$. If $e = \texttt{plus}(e_1;e_2)$, then $\tau = \texttt{num}$, $\Gamma \vdash e_1 : \texttt{num}$, and $\Gamma \vdash e_2 : \texttt{num}$ ...

Proof. These may all be proved by induction on the derivation of the typing judgment $\Gamma \vdash e : \tau$.

I understand that this is obviously true, but I don't understand how I might explicitly write out the proof for this (e.g., what does "induction on the derivation of the typing judgment" mean?)

This is my current understanding:

The derivation of the typing judgement is simply the sequence of rules applied to figure out the type of some expression (in this case, $e$).

For example, if I have $e_1 : \texttt{num}$ and $e_2 : \texttt{num}$, and I wish to find the type of $\texttt{plus}(e_1;e_2)$, I could derive it as follows in one step according to the rules of the language:

$$\frac{\Gamma \vdash e_1 : \texttt{num}, \Gamma \vdash e_2 : \texttt{num}}{\Gamma \vdash \texttt{plus}(e_1;e_2) : \texttt{num}}$$

But I don't know what it means to use induction "on the derivation".


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.