Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
type_theory [2015/10/07 19:30] nikolaj |
type_theory [2016/04/14 11:58] nikolaj |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Type theory ===== | ===== Type theory ===== | ||
- | ==== Framework ==== | + | ==== Note ==== |
- | >todo: introduce in a chain of entries more and more expressible type theories. the guideline being that each entry is a "faithful subset" of the next. | + | ----- |
- | > | + | |
- | >remark: with the Framework entries, I go up in complexity - then with the entries with mathematical content, I start with abstract and go to concrete. | + | |
- | === Introduction === | + | === Reference === |
- | In this entry, we elaborate on the $\frac{foo}{bar}$ scheme to specify well formed syntactic expressions. | + | http://www.cs.cmu.edu/~rwh/plbook/book.pdf |
- | In a type theory, in particular, we reason about systems of syntactical constructions. | + | ----- |
- | + | ||
- | * The declaration of variables is completely formalized: If $\sigma$ is a sort (called //type//) and we want to fix the variable $x$ (called //term//) to be of this sort, we write $x:\sigma$. | + | |
- | * Rules (one level up in the metalanguage if you will) are written down vertically. The rules "If $A$ and $B$ are syntactically correct sequents, then so is $C$" is written | + | |
- | $$\frac{A\hspace{.5cm}B}{C}$$ | + | |
- | This two dimensional notation initially comes from calculi in [[Logic]]. | + | |
- | == Examples == | + | |
- | So for example, if $\mathrm{Type}$ is the most generic type in our system, and we want a theory with the rule that if $\sigma$ and $\tau$ are of type $\mathrm{Type}$, that then the symbols $\sigma\to\tau$ and $\sigma\times\tau$ also denote types, then we write this is | + | |
- | $$\frac{\sigma:\mathrm{Type}\hspace{1cm}\tau:\mathrm{Type}}{\sigma\to\tau:\mathrm{Type}}$$ | + | |
- | and | + | |
- | $$\frac{\sigma:\mathrm{Type}\hspace{1cm}\tau:\mathrm{Type}}{\sigma\times\tau:\mathrm{Type}}$$ | + | |
- | A merit of this formalization is that makes it hard to end up with wrong expression syntax like '$\land\land P$'. We can use typing systems to define syntax for computer programs, or logic, of cookie recipes. For example, if $P$ and $Q$ are propositions and $\land$ means "and", then we could introduce a type of propositions $\mathrm{Prop}$ and formally express a rule how to form more propositions using these symbols: | + | |
- | $$\frac{P:\mathrm{Prop}\hspace{1cm}Q:\mathrm{Prop}}{P\land Q:\mathrm{Prop}}$$ | + | |
- | + | ||
- | * Often, we study sequents expressing "Within the type declarations $\Gamma$ (called //context//) from $\Theta$ we can form $\Psi$" and this is written $\Gamma|\Theta\vdash\Psi$. Theta can be any formula and if we don't need any other formula than such a typing judgment $\Gamma=x:\sigma$, then we just have $\Gamma\vdash\Psi$. | + | |
- | == More examples == | + | |
- | The following certainly give sensible expression in arithmetic: | + | |
- | $$\frac{n:\mathbb{N}\hspace{1cm}m:\mathbb{N}}{n\cdot m:\mathbb{N}}$$ | + | |
- | $$\frac{n:\mathbb{N}}{n+1:\mathbb{N}}$$ | + | |
- | Or consider | + | |
- | $$\frac{A=B:\mathrm{Prop}}{B=A:\mathrm{Prop}}$$ | + | |
- | Note, again, that the above is about what constitutes as syntactically correct expression in a logic, while e.g. the statement $(A=B)\implies (A=B)$ is a statement within the logic itself. Indeed, we will hve $\left((A=B)\implies (A=B)\right):\mathrm{Prop}$. | + | |
- | == Even more examples == | + | |
- | Here is an example for a derivation rule in proof theory. It expresses that if $p$ is a proof for the proposition $A\implies B$ and if $x$ is a proof for the proposition $A$, then we can proof that $B$ holds - and this proof is denoted by $p\,x$ | + | |
- | $$\frac{p:(A\implies B)\hspace{1cm}x:A}{p\,x:B}$$ | + | |
- | + | ||
- | Here is an example from category theory. | + | |
- | The following rule expresses that if $g$ is an arrow in the Hom-class ${\bf C}[A,B]$, and if $f$ is an arrow in the Hom-class ${\bf C}[B,C]$, then $f\circ g$ is an arrow in the Hom-class ${\bf C}[A,C]$. | + | |
- | $$\frac{g:{\bf C}[A,B]\hspace{1cm}f:{\bf C}[B,C]}{f\circ g:{\bf C}[A,C]}$$ | + | |
- | + | ||
- | Here is an example of the theory //simply type lambda calculus//. | + | |
- | The following rule expresses that if $f$ is a function from $D$ in $C$, then for all $x$ in $D$, then $f$ applied to $x$ is in $C$: | + | |
- | $$\frac{f:(D\to C)\hspace{1cm}x:D}{f\,x:C}$$ | + | |
- | + | ||
- | Or more formally still, the following assumes that from a context $\Gamma$ we can define spaces $D$ and $C$ and $D\to C$ and the first two are indeed viewed as domain and codomain. | + | |
- | $$\frac{\Gamma\vdash f:(D\to C)\hspace{1cm}\Gamma\vdash x:D}{\Gamma\vdash f\ x:C}$$ | + | |
- | + | ||
- | ==== Discussion ==== | + | |
- | There are type theory with types and terms completely seperated. If we let types have a type (like in the example with $\mathrm{Type}$ above), then types are also terms. If types functionally vary over terms we call the system dependently types and if the types vary over other types we have polymorphic types. | + | |
- | + | ||
- | The most heavily studied type systems are those for computation. If you define the type former $\to$ and the associated term constructor (lambda-terms) and rewriting rules, you soon get a Turing complete system. | + | |
- | + | ||
- | The first lambda-calculus was untyped (just ad hoc constructors for terms) and this can be seen as simple type theory with $(\sigma\to\sigma)\overset{!}{=}\sigma$. | + | |
- | + | ||
- | The first thing one naturally adds after function types are product types $\times$ and unit type $1$. This lets you form lists and choose element. The natural categorical model is a [[http://en.wikipedia.org/wiki/Cartesian_closed_category|cartesian closed category]]. | + | |
- | + | ||
- | And then you might add sum types $+$ and the empty type $0$. This way you can merge types and code if-statements. | + | |
- | + | ||
- | >== Curry Howard correspondence == | + | |
- | >If capital letters like X are proposition (or types), low case letters like x are arguments (or terms of the type) and x:X means x is an argument for X (or x is a term of type X), then e.g. | + | |
- | > | + | |
- | >(A and B) implies A | + | |
- | >means „given two arguments a and b for A and B, you have an argument a for A.“ | + | |
- | > | + | |
- | >It can be proven and this exactly corresponds with the fact that there is indeed the program, a function f, that you’ll pass the list [a,b] and it returns the first entry. The proposition | + | |
- | > | + | |
- | >A implies (A and B) | + | |
- | > | + | |
- | >is not true, because you have no argument for B. | + | |
- | >And indeed, you can’t possibly tell me a program f which takes an argument a for A and spits out a pair [a,b]. | + | |
- | > | + | |
- | >If „not X“ or „X is not the case“ is read as type of a function that you pass an x and it loops forever, then you can e.g. make sense of | + | |
- | > | + | |
- | >(not A and not B) implies not (A or B) | + | |
- | >which means „if A is not the case and B is no the case, then it’s not the care that ‚either A or B is true‚ is true.“ | + | |
- | >The program f must be constructed to take as input a pair [h,g] of ever-looping (i.e. never halting) functions h and g, and return function which can either take a term a or a term b, but in any case never halts. The function is | + | |
- | >if you get a, apply the first entry h or the list [h,g] you got to it, and if you get a b, you apply the second entry g of the list [h,g] you got to it | + | |
- | > | + | |
- | >Further, you can proof (try it) | + | |
- | >A implies not(not A) | + | |
- | > | + | |
- | >but you can’t proof | + | |
- | >not(not A) implies A | + | |
- | >(which is equivalent to the law of excluded middle) | + | |
- | > | + | |
- | >The above goes as Curry-Howard correspondence and that’s how automated theorem proving works. | + | |
- | > | + | |
- | + | ||
- | ==== Parents ==== | + | |
=== Related === | === Related === | ||
- | [[About]] | + | [[About]], [[Specifying syntax]] |