Formalización de la teoría de conjuntos finitos en la teoría de tipos.

La mayoría de los asistentes de prueba tienen una formalización del concepto de "conjunto finito". Sin embargo, estas formalizaciones difieren enormemente (¡aunque uno espera que todas sean esencialmente equivalentes!). Lo que no entiendo en este momento es el espacio de diseño involucrado, y cuáles son los pros y los contras de cada formalización.

En particular, me gustaría entender lo siguiente:

• ¿Puedo axiomatizar conjuntos finitos (es decir, tipos habitados por un número finito de habitantes) en la teoría de tipos simple? Sistema F? ¿Cuáles son los inconvenientes de hacerlo de esta manera?
• Sé que se puede hacer 'elegantemente' en un sistema de tipo dependiente. Pero, desde un punto de vista clásico, las definiciones resultantes parecen extremadamente extrañas. [¡No digo que estén equivocados, ni mucho menos!]. Pero tampoco entiendo por qué tienen "razón". Entiendo que escogen el concepto correcto , pero la razón más profunda para "decirlo de esa manera" es lo que no entiendo completamente.

Básicamente, me gustaría una introducción razonada al espacio de diseño de formalizaciones del concepto de 'conjunto finito' en la teoría de tipos.

Sé que se puede hacer 'elegantemente' en un sistema de tipo dependiente. Pero, desde un punto de vista clásico, las definiciones resultantes parecen extremadamente extrañas.

¿Puedes explicar qué quieres decir con "extraterrestre"? Me parece que formalizas el concepto de conjunto finito exactamente de la misma manera en la teoría de tipos y en la teoría de conjuntos.

En la teoría de conjuntos, se procede definiendo el conjunto como Luego, define el predicado de finitud como: Donde significa isomorfismo de conjuntos.$Fin(n)$

$$\mathrm{Fin}(n) \triangleq \{ k \in \mathbb{N} \;|\; k < n \}$$ $$\mathrm{Finite}(X) \triangleq \exists n\in\mathbb{N}.\; X \simeq \mathrm{Fin}(n)$$ $A \simeq B$

En la teoría de tipos, ¡puedes hacer exactamente lo mismo! Tenga en cuenta que es un tipo con elementos (ya que el segundo componente del par es irrelevante para la prueba). Luego, puede definir el constructor de tipo de finitud como: Donde significa isomorfismo de tipos.

$$\mathrm{Fin}(n) \triangleq \Sigma k:\mathbb{N}.\; \mathsf{if}\; k < n\,\mathsf{then}\; \mathsf{Unit} \;\mathsf{else}\; \mathsf{Void}$$ $\mathrm{Fin}(n)$$n$ $$\mathrm{Finite}(X) \triangleq \Sigma n:\mathbb{N}.\; X \simeq \mathrm{Fin}(n)$$ $A \simeq B$

Déjame ver si puedo agregar algo útil a la respuesta de Neel. El "espacio de diseño" para conjuntos finitos es mucho más grande constructivamente que clásico porque varias definiciones de "finito" no necesitan coincidir constructivamente. Varias definiciones en la teoría de tipos dan conceptos ligeramente diferentes. Aquí hay algunas posibilidades.

Los conjuntos finitos de Kuratowski ( -finite) se pueden caracterizar como las redes libres -: dado un conjunto, tipo u objeto , los elementos de la red libre - pueden ser como subconjuntos finitos de . De hecho, cada elemento es generado por:$K$$\lor$$X$$\lor$$K(X)$$X$

• el elemento neutral , que corresponde al conjunto vacío, o$0$
• un generador , que corresponde al singleton , o$x \in X$$\lbrace x \rbrace$
• una unión de dos elementos, que corresponde a una unión.$S \lor T$

Una formulación equivalente de es: es -finite si, y solo si, existe y una suposición .$K(X)$$S \subseteq X$$K$$n \in \mathbb{N}$ $e : \lbrace 1, \ldots, n \rbrace \to S$

Si comparamos esto con la definición de Neel vemos que se requiere una biyección . Esto equivale a tomar esos subconjuntos -finitos que tienen igualdad decidible: . Usemos para la recogida de decidable subconjuntos -finite de .$e : \lbrace 1, \ldots, n \rbrace \to S$$K$$S \subseteq X$$\forall x, y \in S . x = y \lor x \neq y$$D(X)$$K$$X$

Obviamente, está cerrado bajo uniones finitas, pero no necesita cerrarse bajo intersecciones finitas. Y no está cerrado bajo ninguna operación. Dado que la gente espera que los conjuntos finitos se comporten un poco como una "aglebra booleana sin una parte superior", también se podría tratar de definirlos como el álgebra booleana generalizada libre ( , , y complementos relativos ), pero en realidad nunca Escuché de tal esfuerzo.$K(X)$$D(X)$$0$$\lor$$\land$$\setminus$

Al decidir cuál es la definición "correcta", debe prestar atención a lo que desea hacer con los conjuntos finitos. Y no hay una única definición correcta. Por ejemplo, ¿en qué sentido de "finito" es el conjunto de raíces complejas de un polinomio finito ?

Ver Constructivamente finito? por Thierry Coquand y Arnaud Spiwack para una discusión detallada de la finitud. La lección es que la finitud está lejos de ser obvia constructivamente.