Substituting a term for a variable in a context - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-09-18T14:09:06Z https://cs.stackexchange.com/feeds/question/110667 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/110667 1 Substituting a term for a variable in a context CuriousKid7 https://cs.stackexchange.com/users/93428 2019-06-14T07:36:26Z 2019-06-14T07:36:26Z <p>At <a href="http://www1.maths.leeds.ac.uk/~pmtng/Slides/syntax.pdf" rel="nofollow noreferrer">this link</a> you can read Nicola Gambino's slides on one way to approach the formal syntax of Martin-Löf dependent type theory. (They are concise and very readable.)</p> <p>On slide 10, he gives a standard definition of a <em>context</em> as a list of the form <span class="math-container">$$x_1:A_1, \ldots, x_n:A_n$$</span> where the <span class="math-container">$x_i$</span> denote pairwise distinct <em>variables</em>. </p> <p>Now, on slide 17, he gives a standard example of a structural rule for the type theory, often called the substitution rule:</p> <p><span class="math-container">$$\frac{x : A, \Gamma \vdash J \quad a : A}{\Gamma[a / x] \vdash J[a / x]}$$</span> where <span class="math-container">$J$</span> denotes a consequent of a generic judgment. Note that <span class="math-container">$\Gamma$</span> is supposed to be a context in the premise.</p> <p><strong>But what exactly does <span class="math-container">$\Gamma[a / x]$</span> mean?</strong></p> <p>We need <span class="math-container">$\Gamma[a / x]$</span> to be a context for the conclusion of the rule to be a well-formed judgment, but just replacing the variable <span class="math-container">$x$</span> with the <em>term</em> <span class="math-container">$a$</span> may give <span class="math-container">$\Gamma[a / x]$</span> the wrong form since <span class="math-container">$a$</span> need not be a variable. Therefore, there seems to be an immediate issue here.</p> <p>Could someone clarify the definition of substituting a term for a variable in a context? </p>