Jaka jest dokładnie różnica semantyczna między zestawem a typem?

EDYCJA: Zadałem teraz podobne pytanie dotyczące różnicy między kategoriami i zestawami.

Za każdym razem czytam o teorii typów (co prawda jest raczej nieformalny), naprawdę nie mogę zrozumieć, jak różni się od teorii mnogości, konkretnie .

Rozumiem, że istnieje konceptualna różnica między powiedzeniem „x należy do zbioru X” a „x jest typu X”, ponieważ intuicyjnie zbiór jest tylko zbiorem obiektów, podczas gdy typ ma pewne „właściwości”. Niemniej jednak zestawy są często definiowane również według właściwości, a jeśli tak, to mam problem ze zrozumieniem, w jaki sposób to rozróżnienie ma jakiekolwiek znaczenie.

Więc w jak najbardziej konkretny sposób, co dokładnie oznacza, że $x$ mówi, że jest typu , w porównaniu do powiedzenia, że ​​jest elementem w zestawie S ?$T$$S$

(Możesz wybrać dowolny typ i zestaw, który sprawia, że ​​porównanie jest najbardziej klarowne).

Aby zrozumieć różnicę między zestawów i typów, te musi wrócić do pre -mathematical idee „zbieranie” oraz „budownictwo” i zobacz, jak zestawy i typy mathematize nich.

Istnieje wiele możliwości dotyczących matematyki. Dwa z nich to:

1. Myślimy o matematyce jako działaniu, w którym obiekty matematyczne są konstruowane zgodnie z pewnymi regułami (myślimy o geometrii jako o działaniu polegającym na konstruowaniu punktów, linii i okręgów za pomocą linijki i kompasu). W ten sposób obiekty matematyczne są zorganizowane zgodnie z tym, jak są skonstruowane , i istnieją różne typy konstrukcji. Matematyczny obiekt jest zawsze konstruowane w pewnym wyjątkowy sposób, co decyduje o jego unikalny rodzaj.

2. Myślimy o matematyce jako rozległym wszechświecie pełnym wcześniej istniejących obiektów matematycznych (pomyśl o płaszczyźnie geometrycznej podanej). Odkrywamy, analizujemy i myślimy o tych obiektach (obserwujemy, że na płaszczyźnie są punkty, linie i okręgi). My zbieramy je do zestawu . Zwykle zbieramy elementy, które mają coś wspólnego (na przykład wszystkie linie przechodzące przez dany punkt), ale w zasadzie zestaw może zawierać dowolną selekcję obiektów. Zestaw jest określony przez jego elementy i tylko przez jego elementy. Obiekt matematyczny może należeć do wielu zbiorów.

Nie twierdzimy, że powyższe możliwości są jedynymi dwiema, ani że jedna z nich całkowicie opisuje matematykę. Niemniej jednak każdy widok może służyć jako przydatny punkt wyjścia dla ogólnej teorii matematycznej, która użytecznie opisuje szeroki zakres działań matematycznych.

Jest rzeczą naturalną, aby wziąć typu i wyobrazić sobie zbiór wszystkich rzeczy, które można zbudować z wykorzystaniem zasad T . Jest to rozszerzenie z T , a to nie T sama. Na przykład tutaj są dwa typy, które mają różne reguły budowy, ale mają to samo rozszerzenie:$T$$T$$T$ $T$

1. Typ par których n jest konstruowany jako liczba naturalna, a p jest konstruowany jako dowód pokazujący, że n jest parzystą liczbą pierwszą większą niż$(n, p)$$n$$p$$n$$3$ .

2. Typ par którym m jest konstruowany jako liczba naturalna, a q jest konstruowany jako dowód pokazujący, że m jest nieparzystą liczbą pierwszą mniejszą niż 2 .$(m, q)$$m$$q$$m$$2$

Tak, są to głupie, trywialne przykłady, ale chodzi o to, że oba typy nie mają nic w swoim rozszerzeniu, ale mają różne reguły budowy. Natomiast zestawy a { m ∈ N ∣ m  to liczba nieparzysta mniejsza niż  2 } są równe, ponieważ mają te same elementy.

$$\{ n \in \mathbb{N} \mid \text{$n$ is an even prime larger than $3$} \}$$ $$\{ m \in \mathbb{N} \mid \text{$m$ is an odd prime smaller than $2$} \}$$

Note that type theory is not about syntax. It is a mathematical theory of constructions, just like set theory is a mathematical theory of collections. It just so happens that the usual presentations of type theory emphasize syntax, and consequently people end up thinking type theory is syntax. This is not the case. To confuse a mathematical object (construction) with a syntactic expression that represents it (a term former) is a basic category mistake that has puzzled logicians for a long time, but not anymore.

To start, sets and types aren't even in the same arena. Sets are the objects of a first-order theory, such as ZFC set theory. While types are like overgrown sorts. To put it a different way, a set theory is a first-order theory within first-order logic. A type theory is an extension of logic itself. Martin-Löf Type Theory, for example, is not presented as a first-order theory within first-order logic. It's not that common to talk about sets and types at the same time.

As Discrete lizard states, types (and sorts) serve a syntactic function. A sort/type behaves as a syntactic category. It lets us know what expressions are well-formed. For a simple example using sorts, let's say we described the theory of vector spaces over an arbitrary field as a 2-sorted theory. We have a sort for scalars, $\mathsf S$, and a sort for vectors, $\mathsf V$. Among many other things, we'd have an operation for scaling: $\mathsf{scale}:\mathsf S\times \mathsf V\to \mathsf V$. This lets us know that $\mathsf{scale}(\mathsf{scale}(s,v),v)$ is simply not a well-formed term. In a type theoretic context, an expression like $f(x)$ requires $f$ to have a type $X\to Y$ for some types $X$ and $Y$. If $f$ does not have the type of a function, then $f(x)$ is simply not a well-formed expression. Whether an expression is of some sort or has some type is a meta-logical statement. It makes no sense to write something like: $(x:X)\implies y=3$. First, $x : X$ is simply not a formula, and second, it doesn't even conceptually make sense as sorts/types are what let us know which formulas are well-formed. We only consider the truth value of well-formed formulas, so by the time we're considering whether some formula holds, we better already know that it is well-formed!

In set theory, and particularly ZFC, the only non-logical symbol at all is the relation symbol for set membership, $\in$. So $x\in y$ is a well-formed formula with a truth value. There are no terms other than variables. All the usual notation of set theory is a definitional extension to this. For example, a formula like $f(x)=y$ is often taken to be shorthand for $(x,y)\in f$ which itself may be taken as shorthand for $\exists p.p\in f\land p=(x,y)$

$$\exists p.p\in f\land(\forall z.z\in p\iff [z = x\lor(\forall w.w\in z\Leftrightarrow w = y)])$$ $f$$\pi(7)=3$ where $\pi$ is the real number is a completely legitimate and meaningful (and potentially even true) set theoretic expression. Basically, anything you write that parses in set theory can be given some meaning. It may be a completely spurious meaning, but it has one. Sets are also "first-class" objects in set theory. (They better be as they are the only objects usually.) A function like $$f(x)=\begin{cases}\mathbb N, &\text{if }x=1\\7,&\text{if }x=\mathbb Q\\x\cap \mathbb R^\mathbb R,&\text{if }x=(\mathbb Z,\mathbb N)\end{cases}$$ is a completely legitimate function in set theory. There is nothing even remotely analogous to this in type theory. The closest would be to use codes for a Tarskian universe. Sets are the objects of set theory; types are not the object of type theory.

A type is not a collection of things (neither is a set for that matter...), and it is not defined by a property. A type is a syntactic category that lets you know what operations are applicable to terms of that type and which expressions are well-formed. From a propositions-as-types perspective, what types are classifying are the valid proofs of the proposition to which the type corresponds. That is, the well-formed (i.e. well-typed) terms of a given type correspond to the valid proofs (which are also syntactic objects) of the corresponding proposition. Nothing like this is happening in set theory.

Set theory and type theory are really not anything alike.

In practice, claiming that $x$ being of type $T$ usually is used to describe syntax, while claiming that $x$ is in set $S$ is usually used to indicate a semantic property. I will give some examples to clarify this difference in usage of types and sets. For the difference in what types and sets actually are, I refer to Andrej Bauer's answer.

An example

To clarify this distinction, I will use the example given in Herman Geuvers' lecture notes. First, we look at an example of inhabiting a type:

$$3+(7*8)^5:\mathrm{Nat},$$ and an example of being member of a set: $$3\in \{n\in\mathbb{N}\mid \forall x,y,z\in\mathbb{N}^+ (x^n+y^n\neq z^n)\}$$

The main difference here is that to test whether the first expression is a natural number, we don't have to compute some semantic meaning, we merely have to 'read off' the fact that all literals are of type Nat and that all operators are closed on the type Nat.

However, for the second example of the set, we have to determine the semantic meaning of the $3$ in the context of the set. For this particular set, this is quite hard: the membership of $3$ for this set is equivalent to proving Fermat's last theorem! Do note that, as stated in the notes, the distinction between syntax and semantics cannot always be drawn that clearly. (and you might even argue that even this example is unclear, as Programmer2134 mentions in the comments)

Algorithms vs Proofs

To summarize, types are often used for 'simple' claims on the syntax of some expression, such that membership of a type can be checked by an algorithm, while to test membership of a set, we would in usually require a proof.

To see why this distinction is useful, consider a compiler of a typed programming language. If this compiler has to create a formal proof to 'check types', the compiler is asked to do an almost impossible task (automated theorem proving is, in general, hard). If on the other hand the compiler can simply run an (efficient) algorithm to check the types, then it can realistically perform the task.

A motivation for a strict(er) interpretation

There are multiple interpretations of the semantic meaning of sets and types. While under the distinction made here extensional types and types with undecidable type-checking (such as those used in NuPRL, as mentioned in the comments) would not be 'types', others are of course free to call them as such (just as free as they are as to call them something else, as long as their definitions fit).

However, we (Herman Geuvers and I), prefer to not throw this interpretation out of the window, for which I (not Herman, although he might agree) have the following motivation:

First of all, the intention of this interpretation isn't that far from that of Andrej Bauer. The intention of a syntax is usually to describe how to construct something and having an algorithm to actually construct it is generally useful. Furthermore, the features of a set are usually only needed when we want a semantic description, for which undecidability is allowed.

So, the advantage of our more stricter description is to keep the separation simpler, to get a distinction more directly related to common practical usage. This works well, as long as you don't need or want to loosen your usage, as you would for, e.g. NuPRL.

I believe that one of the most concrete differences about sets and types is the difference in the way the "things" in your mind are encoded into the formal language.

Both sets and types allow you to speak about things, and collections of things. The main difference is that with sets, you can ask any question you want about things and it will maybe be true, maybe not; while with types, you first have to prove that the question makes sense.

For example, if you have booleans $\mathbb B=\{\operatorname{true},\operatorname{false}\}$ and natural numbers $\mathbb N=\{0, 1,\dots \}$, with types, you can not ask if $\operatorname{true}=1$ which you can with sets.

One way to interpret this is that with sets, everything is encoded into a single collection: the collection of all sets. $0$ is encoded as $[0]=\{\}$, $n+1$ is encoded as $[n+1]=\{[n]\}\cup [n]$ and $\operatorname{true}$ and $\operatorname{false}$ can be encoded by any two distinct sets. So that it actually makes sense to ask if $\operatorname{true}=1$, as it can be understood as asking if "the encoding chosen for $\operatorname{true}$ is the same as the encoding chosen for $1$". But the answer to this question could change if we chose another encoding: it is about the encodings and not really about the things.

You can then think of types as describing the encoding of the things inside it. With types, to ask the question of whether $a=b$, you first have to show that $a$ and $b$ have the same type, i.e. that they were encoded in the same way, which prohibits questions such as $\operatorname{true}=1$. You could still want to have a big type $S$ in which both $\mathbb B$ and $\mathbb N$ could be encoded, and then given two encodings $\iota_\mathbb B:\mathbb B\to S$ and $\iota_\mathbb N:\mathbb N\to S$, you could ask whether $\iota_\mathbb B(\operatorname{true})=\iota_\mathbb N(1)$ but the fact that this question depends on the encodings (and the choice of encodings) is now explicit.

Note that in those cases, whether the question made sense was actually easy to see but it could be much harder as in, for example, $(\operatorname{if} \text{very_hard_question} \operatorname{then} 1 \operatorname{else} \operatorname{true})=1$.

In summary, sets let you ask any question you want, but types force you to make encodings explicit when the answer may depend on them.