Editing Type theory (section)

=== Inference Rules ===

==== Function application ====
The power of type theories is in specifying how terms may be combined by way of [[Rule of inference|inference rules]].<ref name="church" /> Type theories which have functions also have the inference rule of [[function application]]: if <math>t</math> is a term of type <math>\sigma\to\tau</math>, and <math>s</math> is a term of type <math>\sigma</math>, then the application of <math>t</math> to <math>s</math>, often written <math>(t\,s)</math>, has type <math>\tau</math>. For example, if one knows the type notations <math>0:\textsf{nat}</math>, <math>1:\textsf{nat}</math>, and <math>2:\textsf{nat}</math>, then the following type notations can be [[Deduction system|deduced]] from function application.<ref name=":1" />
* <math>  (\mathrm{add}\,1): \textsf{nat}\to\textsf{nat}</math>
* <math>   ((\mathrm{add}\,2)\,0): \textsf{nat}</math>
* <math>   ((\mathrm{add}\,1)((\mathrm{add}\,2)\,0)): \textsf{nat}</math>

Parentheses indicate the [[order of operations]]; however, by convention, function application is [[left associative]], so parentheses can be dropped where appropriate.<ref name=":1" /> In the case of the three examples above, all parentheses could be omitted from the first two, and the third may simplified to <math>   \mathrm{add}\,1\, (\mathrm{add}\,2\,0): \textsf{nat}</math>.

==== Reductions ====
Type theories that allow for lambda terms also include inference rules known as <math>\beta</math>-reduction and <math>\eta</math>-reduction. They generalize the notion of function application to lambda terms. Symbolically, they are written

* <math>(\lambda v. t)\,s\rightarrow t[v \colon= s]</math> (<math>\beta</math>-reduction).
* <math>(\lambda v. t\, v)\rightarrow t</math>, if <math>   v</math> is not a [[Free variables and bound variables|free variable]] in <math>t</math> (<math>\eta</math>-reduction).

The first reduction describes how to evaluate a lambda term: if a lambda expression <math>(\lambda v .t)</math> is applied to a term <math>s</math>, one replaces every occurrence of <math>v</math> in <math>t</math> with <math>s</math>. The second reduction makes explicit the relationship between lambda expressions and function types: if <math>(\lambda v. t\, v)</math> is a lambda term, then it must be that <math>t</math> is a function term because it is being applied to <math>v</math>. Therefore, the lambda expression is equivalent to just <math>t</math>, as both take in one argument and apply <math>t</math> to it.<ref name="church" />

For example, the following term may be <math>\beta</math>-reduced.

<math>(\lambda x.\mathrm{add}\,x\,x)\,2\rightarrow \mathrm{add}\,2\,2</math>

In type theories that also establish notions of [[Equality (mathematics)|equality]] for types and terms, there are corresponding inference rules of <math>\beta</math>-equality and <math>\eta</math>-equality.<ref name=":1" />