Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
product_type [2014/03/30 19:41] nikolaj |
product_type [2014/03/30 20:09] nikolaj |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Product type ===== | ===== Product type ===== | ||
==== Type ==== | ==== Type ==== | ||
- | | @#55CCEE: context | @#55CCEE: $X, Y, Z$ ... type | | + | | @#55CCEE: context | @#55CCEE: $X, Y$ ... type | |
| @#FF8866: rule | @#FF8866: ${\large\frac{a\ :\ X\hspace{1cm}b\ :\ Y}{\langle a,b\rangle\ :\ X\times Y}}(\times\mathcal I)$ | | | @#FF8866: rule | @#FF8866: ${\large\frac{a\ :\ X\hspace{1cm}b\ :\ Y}{\langle a,b\rangle\ :\ X\times Y}}(\times\mathcal I)$ | | ||
| @#FF8866: rule | @#FF8866: ${\large\frac{p :\ X\times Y}{\pi_{\mathcal l}(p)\ :\ X\hspace{1cm}\pi_{\mathcal r}(p)\ :\ Y}}(\times\mathcal E)$ | | | @#FF8866: rule | @#FF8866: ${\large\frac{p :\ X\times Y}{\pi_{\mathcal l}(p)\ :\ X\hspace{1cm}\pi_{\mathcal r}(p)\ :\ Y}}(\times\mathcal E)$ | | ||
Line 15: | Line 15: | ||
Depending on what we want to do with the type system, we might just replace expressions of computational equivalence $\rightsquigarrow$ by equality '$=$'. This symbol denotes a term rewriting, i.e. a computations alla | Depending on what we want to do with the type system, we might just replace expressions of computational equivalence $\rightsquigarrow$ by equality '$=$'. This symbol denotes a term rewriting, i.e. a computations alla | ||
- | $\lambda x.\,\sin\,x\ \rightsquigarrow_\eta\ \sin,$ | + | $\left(\lambda x.\,3+x\right)\,4\ \rightsquigarrow_\beta\ 3+4,$ |
or | or | ||
- | $\left(\lambda x.\,3+x\right)\,4\ \rightsquigarrow_\beta\ 3+4.$ | + | $\lambda x.\,\sin\,x\ \rightsquigarrow_\eta\ \sin$ |
+ | == Logic == | ||
+ | |||
+ | Note how the rules reflect the logical "and". | ||
==== Parents ==== | ==== Parents ==== | ||
=== Related === | === Related === | ||
[[Type theory]] | [[Type theory]] |