2
$\begingroup$

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.

  • 0
    @AustinMohr - Yes I believe so, after seeing this link- http://math.stackexchange.com/questions/90787/whats-the-difference-between-to-implication-and-vdash-therefore2012-04-09

1 Answers 1

6

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 ;-)

  • 0
    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).2012-04-11