# Clarification about what is being asked in this computer science proof?

I am supposed to prove this statement(part of a presentation on MinML-Syntax and Static Semantics) using typing rules:

If G, x:t |-- e’ : t’ and G |-- e: t then
G |-- e’[e/x] : t’


I am lost about what this means. Is this using the standard math proof and symbols?

I appreciate any tips or advice.

-
Is your |-- actually $\vdash$ (latex code "vdash")? – Austin Mohr Apr 8 '12 at 23:37
@AustinMohr - Yes I believe so, after seeing this link- math.stackexchange.com/questions/90787/… – Adel Apr 9 '12 at 1:07

Normally one would write this as follows (and this is a standard way of writing the typing rules and some other logic-related stuff): $${G, x:t \vdash e' : t' \quad\quad G \vdash e : t \over G \vdash e'[e/x] : t' }$$

Notation $e : t$ means that expression $e$ is of type $t$. Also, here $G$ is some context (e.g. implied by other rules in the proof tree), usually it contains things like $e_1 : t_1$ and so on, i.e. we could set $G' = G, x:t$ and write the first part as $G' \vdash e' : t'$. Moreover, $\alpha[\beta / x]$ means substitution, i.e. term $\alpha$ with all $x$-s replaced by $\beta$, some authors also write this as $\alpha[x\leftarrow \beta]$ or $\alpha[x := \beta]$ or even $\alpha[x \mapsto \beta]$ (what is substituted for what can be usually recognized by variable naming convention, e.g $x$-s, $y$-s and $z$-s are replaced by $e$-s, $t$-s, $\alpha$-s or other things). Given all this, the aforementioned rule reads as:

If $G$ and $x : t$ implies that expression $e'$ has type $t'$, and if from $G$ follows that $e$ is of type $t$, then the context $G$ also implies that $e'[e/x]$ has type $t'$.

This is quite intuitive: if $e' : t'$ while we know nothing about $x$ but that $x : t$, then if we would to replace $x$ with something different also with type $t$, this shouldn't make any difference. However, from the assumption we have that $e$ is such a term and the result is just what we want: $e'[e/x]$.

Of course this holds (I just guess it does) in this particular type-system and it needs to be proven, there are type-systems in which this is not true. In fact, I do not recall any real-life type-system in which it would not hold (this is a very much desired property), but it is very easy to create an artificial example (but nevertheless I will skip it here).

Hope that helps ;-)

-
Thank You So Much! It's much clearer now. One small question - So this type of proof is different from an inductive proof ? I'm still a little fuzzy on the next step. – Adel Apr 9 '12 at 14:10
@Adel There are inductive proofs in type theory (usually the induction is on the structure of the term), however, this does not seem like it. Normally, such proof would use type-system axioms and simple logic, I am almost sure that this should suffice in your case. Wikipedia page on sequent calculus should give you some idea how a logic proof looks like (there is an example there). Of course this is not the only correct way, but this indeed is a standard notation. – dtldarek Apr 9 '12 at 18:19
Thanks so much dtldarek. I'm still scratching my head on this, but I'm making progress! I found that if I translate all the variables to physical daily-life items it helps visualize (x is food, t is kosher etc). – Adel Apr 11 '12 at 15:28