¿Cuál es exactamente la diferencia semántica entre conjunto y tipo?

33

EDITAR: ahora he hecho una pregunta similar sobre la diferencia entre categorías y conjuntos.

Cada vez que leo acerca de la teoría de tipos (que ciertamente es bastante informal), no puedo entender realmente en qué se diferencia de la teoría de conjuntos, concretamente .

Entiendo que hay una diferencia conceptual entre decir "x pertenece a un conjunto X" y "x es de tipo X", porque intuitivamente, un conjunto es solo una colección de objetos, mientras que un tipo tiene ciertas "propiedades". Sin embargo, los conjuntos a menudo también se definen de acuerdo con las propiedades, y si lo son, entonces tengo problemas para comprender cómo esta distinción es importante de alguna manera.

Así, en el más concreto manera posible, lo que hace exactamente lo que implica sobre X decir que es de tipo T , en comparación con decir que es un elemento del conjunto S ?

(Puede elegir cualquier tipo y conjunto que haga que la comparación sea más clara).

usuario56834
fuente
¿Cuál es el contexto en el que estás usando / escuchando la palabra "tipo"? ¿Es, como su nombre indica, lenguajes de programación? Porque creo que las respuestas a continuación suponen lo contrario.
einpoklum - reinstalar a Mónica el
@einpoklum, no estoy 100% seguro de cómo describir el "contexto", pero básicamente algo así como: estoy tratando de entender el papel de los tipos en las matemáticas. Esencialmente, los conjuntos (como lo veo) tienen dos contextos: en primer lugar, se usan como colecciones de objetos para hacer las matemáticas cotidianas. En segundo lugar, son objetos en la teoría de conjuntos axiomáticos, donde se usan principalmente como una herramienta muy extraña pero útil para Hable acerca de las matemáticas en la lógica de primer orden, dejando que los conjuntos correspondan a funciones y números, etc. Me interesa principalmente la relación entre "conjunto" en el primer sentido y "tipo".
user56834
¿El papel de qué tipos? ¿Los tipos que ves en los documentos de matemáticas / libros de texto, o los tipos de variables en los programas de computadora?
einpoklum - reinstalar a Mónica el
1
@einpoklum, esta pregunta es sobre las de los documentos de matemáticas. (Aunque en realidad también estoy interesado en saber la diferencia fundamental entre los tipos en matemáticas y los tipos en lenguajes de programación, si hay alguno. Pero de eso no se trata esta pregunta).
user56834

Respuestas:

29

Para comprender la diferencia entre conjuntos y tipos, hay que volver a las ideas prematemáticas de "colección" y "construcción", y ver cómo los conjuntos y tipos los matematizan .

Hay un espectro de posibilidades sobre lo que se trata la matemática. Dos de estos son:

  1. Pensamos en las matemáticas como una actividad en la que los objetos matemáticos se construyen de acuerdo con algunas reglas (piense en la geometría como la actividad de construir puntos, líneas y círculos con una regla y una brújula). Por lo tanto, los objetos matemáticos se organizan de acuerdo con cómo se construyen , y hay diferentes tipos de construcción. Un objeto matemático siempre se construye de una manera única, que determina su tipo único.

  2. Pensamos en las matemáticas como un vasto universo lleno de objetos matemáticos preexistentes (pensemos en el plano geométrico como se da). Descubrimos, analizamos y pensamos en estos objetos (observamos que hay puntos, líneas y círculos en el plano). Los recogemos en conjunto . Por lo general, recopilamos elementos que tienen algo en común (por ejemplo, todas las líneas que pasan por un punto dado), pero en principio un conjunto puede mantener una selección arbitraria de objetos. Un conjunto se especifica por sus elementos, y solo por sus elementos. Un objeto matemático puede pertenecer a muchos conjuntos.

No estamos diciendo que las posibilidades anteriores son las únicas dos, o que cualquiera de ellas describe completamente lo que son las matemáticas. Sin embargo, cada vista puede servir como un punto de partida útil para una teoría matemática general que describe útilmente una amplia gama de actividades matemáticas.

Es natural tener un tipo e imaginar la colección de todas las cosas que podemos construir utilizando las reglas de la T . Esta es la extensión de T , y es no t sí. Por ejemplo, aquí hay dos tipos que tienen diferentes reglas de construcción, pero tienen la misma extensión:TTT T

  1. El tipo de pares donde n se construye como un número natural, y p se construye como una prueba que demuestra que n es un número primo par mayor que 3 .(n,p)npn3

  2. El tipo de pares donde m se construye como un número natural, y q se construye como una prueba que demuestra que m es un primo impar menor que 2 .(m,q)mqm2

Sí, estos son ejemplos triviales tontos, pero el punto se destaca: ambos tipos no tienen nada en su extensión, pero tienen diferentes reglas de construcción. En contraste, los conjuntos y { m Nm  es un primo impar menor que  2 } son iguales porque tienen los mismos elementos.

{nNn is an even prime larger than 3}
{mNm is an odd prime smaller than 2}

Tenga en cuenta que la teoría de tipos no se trata de sintaxis. Es una teoría matemática de las construcciones, al igual que la teoría de conjuntos es una teoría matemática de las colecciones. Sucede que las presentaciones habituales de la teoría de tipos enfatizan la sintaxis y, en consecuencia, las personas terminan pensando que la teoría de tipos es la sintaxis. Este no es el caso. Confundir un objeto matemático (construcción) con una expresión sintáctica que lo representa (un término anterior) es un error de categoría básica que ha intrigado a los lógicos durante mucho tiempo, pero ya no.

Andrej Bauer
fuente
1
¡Hermoso gracias! ¿Podría aclarar un detalle? cuando enumera los dos tipos cuya extensión está vacía, dice que "el tipo cuyos elementos son ...". Por pura claridad, ¿es esta una forma 100% correcta de decirlo? Usted dijo en la oración anterior que un tipo no es una colección, por lo que parece que no puede tener "elementos" (que asocio con conjuntos). Esencialmente, la forma en que lo ha escrito ahora, es como si estuviera definiendo el Tipo de acuerdo con el conjunto que es su extensión. Si no pretendía esto, ¿podría reformularlos con mayor precisión para capturar su idea como tipos?
user56834
La extensión de un tipo es un concepto muy útil, y dado que es un tipo de colección, podemos decir "elemento de la extensión de un tipo". Esto es engorroso, por lo que a menudo se abrevia como "elemento de un tipo". Eliminé las frases para disminuir la posibilidad de confusión, pero cuidado, es una terminología común.
Andrej Bauer
Gracias, esto aclara. Entonces, para seguir, ¿es correcto decir lo siguiente? Decir que un objeto es "de tipo T" significa lo mismo que, el objeto es "un elemento de la extensión de T", de modo que hay una suposición natural de tipos a conjuntos. Pero lo contrario no se cumple, porque cualquier conjunto se puede construir de múltiples maneras. Esencialmente, la diferencia entre conjunto y tipo no es importante desde la perspectiva de un objeto particular , en el sentido de que x : T y x X T (donde X T es la extensión de T ) nos dan exactamente la misma información sobre x . Sin embargo,xx:TxXTXTTx
user56834
The difference is relevant when we want to talk about types and sets, and their properties and relations. So in other words, the information that we lose when we say xXT rather than x:T does not tell us anything relevant about x, but the same may not hold if we e.g. want to talk about superset-subset or type-subtype relations? Is that correct?
user56834
4
Yeah, one wonders where these books are. Someone should write them.
Andrej Bauer
11

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, S, and a sort for vectors, V. Among many other things, we'd have an operation for scaling: scale:S×VV. This lets us know that scale(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 XY 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)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, . So xy 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)f which itself may be taken as shorthand for p.pfp=(x,y) which is shorthand for

p.pf(z.zp[z=x(w.wzw=y)])
At any rate, any set can take the place of f and everything is a set! As I pointed out in a different question recently, π(7)=3 where π 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)={N,if x=17,if x=QxRR,if x=(Z,N)
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.

Derek Elkins
fuente
1
It is false that types are only syntactic entities.
Andrej Bauer
1
This is very helpful, but one main point in your answer bugs me. It seems to me that it is a mistake (which many people make, or alternatively it is not a mistake and I'm wrong), to say that "a set is not a collection of things". I would say that a set IS a collection of things. That is the most basic essential property of a set. In fact, how would we possibly know that e.g. ZFC are the right axioms to choose (rather than completely arbitrary formulas), without being able to tell that they are true given that sets are collections of objects? Of course, I understand that ...
user56834
Axiomatic set theory treats sets as objects, and as just a symbol, because axiomatic set theory is not a mathematical structure in the mathematical logic sense.
user56834
1
@Programmer2134 To answer that, we would have to get into the semantic meaning of the word "collection." We can't be sure they are "right" unless you take the time to precisely define what "right" means. However, what we can say is that "set" is the result of over a hundred years of mathematicians beating on the concept of a collection, seeking a consistent system which matches the intuitive concept of a collection. To achieve that consistency, they had to make decisions. For example, sets aren't the only collection in mathematics. A "class" also describes a collection.
Cort Ammon - Reinstate Monica
1
@AndrejBauer I'm taking a (mostly) non-philosophical stance and not trying to explain what types "really" are but more how they're used. (I say "serves as" and "behaves as" at the beginning but I did slip into an "is" at the end.) There is a risk of thinking that a variable x being of type T means that the only "values" that x can "take" are the (presumably closed) terms of type T. This isn't true and is not implied by anything I say above. I agree that you can see types as more than syntactic entities, but I think the different syntactic role types play makes a clear contrast to sets.
Derek Elkins
9

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 78)5 5:norteunat,
3{nortenorteX,y,znorte+(Xnorte+ynorteznorte)}

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).

Sin embargo, nosotros (Herman Geuvers y yo) preferimos no tirar esta interpretación por la ventana, por lo que yo (no Herman, aunque podría estar de acuerdo) tenemos la siguiente motivación:

En primer lugar, la intención de esta interpretación no está muy lejos de la de Andrej Bauer. La intención de una sintaxis generalmente es describir cómo construir algo y generalmente es útil tener un algoritmo para construirlo. Además, las características de un conjunto generalmente solo se necesitan cuando queremos una descripción semántica, para lo cual se permite la indecidibilidad.

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.

Discrete lizard
fuente
3
Type checking doesn't need to be decidable (though it is certainly desirable). NuPRL, for instance, does require the user to provide a proof that a term inhabits a type.
Derek Elkins
3
Gracias. Las cosas se están volviendo más claras. He aquí lo que aún me pregunto: ¿no hay un elemento semántico para escribir teoría y un elemento sintáctico para establecer teoría? Por ejemplo, podemos en lugar de ver su "3..."enunciado como enunciado semántico, verlo como una proposición en la teoría de conjuntos axiomáticos, ¿no? Además, ¿el tipo" Nat "no tiene un significado semántico, es decir, que lo que precede es un número natural? Por lo tanto, todavía me confunde dicen conjuntos RHAT son propiedades sintácticas y semánticas tipos.
user56834
1
@DerekElkins I'm not familiar with NuPRL, but e.g. the proof assistant Coq most certainly does type checking by itself (i.e, is the provided term of the 'type of my theorem'). How does NuPRL verify the proof if the user has to 'prove' the fact that a term of a certain type? (in other words, this sounds like NuPRL doesn't use the Curry-Howard correspondence, so what does it use?)
Discrete lizard
1
@Discretelizard I'm not saying NuPRL is typical. It is definitely the usual case for type checking to be decidable. I highly recommend becoming familiar with it just because it takes a fairly different path. NuPRL is a Curry-style rather than Church-style calculus which makes it more of a type refinement system. At any rate, instead of just writing terms (or tactics that produce terms), you have essentially an LCF-style proof system for typing derivations themselves. Arguably, the derivations are what's important, and it's a bit of a "fluke" that we can infer them from terms.
Derek Elkins
3
I elaborated in my answer why it is detrimental to think of type theory as "syntactic". Your first sentence is the offeding one, when you say that "inhabiting a type is a syntactic property". There's as much truth in that as in saying that "being an element of a set is to stand on the left of the symbol ".
Andrej Bauer
4

Creo que una de las diferencias más concretas sobre conjuntos y tipos es la diferencia en la forma en que las "cosas" en su mente están codificadas en el lenguaje formal.

Tanto los conjuntos como los tipos le permiten hablar sobre cosas y colecciones de cosas. La principal diferencia es que con los conjuntos, puede hacer cualquier pregunta que desee sobre las cosas y tal vez sea cierto, tal vez no; mientras que con los tipos, primero tienes que demostrar que la pregunta tiene sentido.

Por ejemplo, si tienes booleanos si={cierto,falso} y números naturales norte={0 0,1,...}, con tipos, no puedes preguntar si cierto=1 que puedes con conjuntos.

Una forma de interpretar esto es que con los conjuntos, todo está codificado en una sola colección: la colección de todos los conjuntos. 0 0 está codificado como [0 0]={}, norte+1 está codificado como [norte+1]={[norte]}[norte] y cierto y falsopuede ser codificado por dos conjuntos distintos. Para que tenga sentido preguntar sicierto=1, ya que puede entenderse como preguntar si "la codificación elegida para cierto es lo mismo que la codificación elegida para 1". Pero la respuesta a esta pregunta podría cambiar si elegimos otra codificación: se trata de las codificaciones y no de las cosas.

Luego puede pensar en los tipos como una descripción de la codificación de las cosas que contiene. Con tipos, hacer la pregunta de siuna=si, primero tienes que demostrar que una y si tienen el mismo tipo, es decir, se codificaron de la misma manera, lo que prohíbe preguntas como cierto=1. Todavía podrías querer tener un tipo grandeS en el que ambos si y norte podría codificarse y luego recibir dos codificaciones ιsi:siS y ιnorte:norteS, podrías preguntar si ιsi(cierto)=ιnorte(1) pero el hecho de que esta pregunta depende de las codificaciones (y la elección de las codificaciones) ahora es explícito.

Tenga en cuenta que en esos casos, si la pregunta tenía sentido era realmente fácil de ver, pero podría ser mucho más difícil como, por ejemplo, (ifvery_hard_questionthen1elsetrue)=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.

xavierm02
fuente
Probablemente esté pensando en un tipo específico de teoría de conjuntos (algo a lo largo de una teoría de un solo orden a la ZFC). Sin embargo, hay otros tipos de teoría de conjuntos que requieren mucha comprobación de que tiene sentido. Y la forma en que se usa la teoría de conjuntos en la práctica está mucho más cerca de estas otras teorías de conjuntos. ¿Crees que un estudiante podría preguntar "EsR un elemento de pecado(2)? "sin ser regañado? La distinción entre la teoría de tipos y la teoría de conjuntos no está en el formalismo, sino en el significado.
Andrej Bauer
@AndrejBauer Derecha. ¿Estaría de acuerdo en que esta respuesta ofrece diferencias entre las teorías de clasificación única (incluidas la mayoría de las teorías establecidas, o al menos las más comunes) y las teorías de clasificación múltiple (incluidas todas las teorías de tipo (?))?
xavierm02
Incluso en una teoría de un solo orden hay que distinguir los términos de las fórmulas ...
Andrej Bauer
@AndrejBauer No entiendo tu segundo comentario.
xavierm02
Una teoría de primer orden de un solo orden tiene dos categorías sintácticas: fórmulas lógicas y términos . Uno tiene que asegurarse de que no estén mezclados, de lo contrario, podría terminar escribiendo "(XX.ϕ(X))norte".
Andrej Bauer