Es la 1-tupla (x) = x?

Question

Basado en la siguiente frase

En el tipo de teoría, de uso común en los lenguajes de programación, una tupla tiene un tipo de producto; esto corrige no sólo la longitud, sino también el subyacente tipos de cada componente.

He llegado a la conclusión de que existen dos enfoques diferentes:

1. En la teoría de conjuntos de tuplas son "tuplas" y el 1-tupla $(x) \neq x$.
2. En teoría tipo tuplas tienen un tipo que se define por un producto Cartesiano. Así por ejemplo, la $(x_1,x_2)\in X\times X$$x_1,x_2\in X$. Así que por un 1-tupla debería ser$(x)\in X$$x\in X$. Debido a $x,(x)\in X$, creo que en esta teoría de la $(x) = x$.

Es cierto que hasta el momento? Si sí, también es $\{x\} = x$ en el tipo de teoría?

Answer 1

Creo que una respuesta correcta a tu pregunta es "depende de a qué te refieres por $1$-ary producto de tipos".

Una posible solución podría ser la identificación de cada tipo de $T$ con su unario producto: si ese es el caso,$(x) = x$.

Por supuesto que también podría decidir que el único producto de un tipo de $T$ no es el tipo de $T$ pero es un nuevo tipo de $\prod T$ que ha:

• un constructor $$(\_) \colon T \to \prod T$$
• un eliminador de $$\pi \colon \prod T \to T$$
• y computacionales reglas diciendo que $$\forall x \in T\; \pi((x))=x$$ $$\forall z \in \prod T\; (\pi(z))=z\ .$$

Sobre la última pregunta, si $\{x\}=x$ es cierto, la respuesta es claramente no en el tipo de teoría. Esto es debido al hecho de que $\{x\}$ $x$ tienen dos tipos diferentes, a saber: si $T$ es el tipo de $x$, por lo tanto $x \in T$,$\{x\} \in \mathcal P(T)$, $\mathcal P(T)$ me refiero al tipo de subtipos de $T$, que es diferente por $T$.

Espero que esto ayude.