¿Cómo demostrar que estos son los únicos habitantes de tipo?

Question

Considere un tipo $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$ con sus dos habitantes \begin {align} \mathrm {tt} &= \lambda x.\ \lambda y.\N- x \\ \mathrm {ff} &= \lambda x.\ \lambda y.y \end {alinear} o utilizando la notación System-F \begin {align} \mathrm {tt} &= \Lambda \alpha.\ \lambda x: \alpha.\ \lambda y: \alpha.\ x \\ \mathrm {ff} &= \Lambda \alpha.\ \lambda x: \alpha.\ \lambda y: \alpha.\ y \end {align}

Me gustaría demostrar que estos son los únicos habitantes de $\mathsf{Boolean}$ . Por supuesto, tiene que haber algunos supuestos adicionales que excluyan funciones como $$\mathrm{if\_boolean} = \Lambda \alpha.\ \lambda x:\alpha.\ \lambda y:\alpha.\ \begin{cases} x& \text{ if }\alpha = \mathsf{Boolean}\\y &\text{ otherwise}\end{cases}$$

pero no sé cómo formalizarlo.

¿Sabes cómo formalizarlo y demostrarlo? Agradecería cualquier ayuda, idea o referencia.

Answer 1

Esto es una consecuencia del teorema de parametricidad. Al final de esta respuesta hay dos referencias para obtener más información, pero de manera informal, el teorema de la parametricidad establece que las sustituciones de tipo conmutan con las funciones polimórficas.

En su caso, el teorema de parametricidad establece que cualquier función con este tipo

$$\hbox{boolean} : \forall \alpha. \alpha \rightarrow \alpha \rightarrow \alpha$$

debe satisfacer el siguiente teorema. Si $A$ y $B$ son tipos, y $R$ es cualquier relación entre elementos de $A$ y $B$ entonces:

$$\forall (x,p) \in R, (y,q) \in R. (\hbox{boolean}\,A\,x\,y,\hbox{boolean}\,B\,p\,q) \in R$$

Esto tiene una serie de consecuencias útiles. Por ejemplo, si $R$ es una función, dice que para todos los tipos $A$ y $B$ :

$$\forall f : A \rightarrow B. \forall x, y : A. f\,(\hbox{boolean}\,A\,x\,y) = \hbox{boolean}\,B\,(f\,x)\,(f\,y)$$

Pero en nuestro caso, es aún más sencillo. Dejemos que $A$ sea el conjunto $\{\mathbf{a}_1, \mathbf{a}_2\}$ y $B$ sea el conjunto $\{\mathbf{b}_1, \mathbf{b}_2\}$ . Definir una relación $R$ para ser $\{(\mathbf{a}_1,\mathbf{b}_1), (\mathbf{a}_2,\mathbf{b}_2)\}$ . Entonces esto significa que:

$$(\hbox{boolean}\,A\,\mathbf{a}_1\,\mathbf{a}_2, \hbox{boolean}\,B\,\mathbf{b}_1\,\mathbf{b}_2) \in R$$

Pero sólo hay dos elementos de $R$ . Por lo tanto, o bien:

$$\hbox{boolean}\,A\,\mathbf{a}_1\,\mathbf{a}_2 = \mathbf{a}_1 \wedge \hbox{boolean}\,B\,\mathbf{b}_1\,\mathbf{b}_2 = \mathbf{b}_1$$

o:

$$\hbox{boolean}\,A\,\mathbf{a}_1\,\mathbf{a}_2 = \mathbf{a}_2 \wedge \hbox{boolean}\,B\,\mathbf{b}_1\,\mathbf{b}_2 = \mathbf{b}_2$$

De ello se desprende que $\hbox{boolean}$ debe ser $\hbox{tt}$ o $\hbox{ff}$ .

No lo he probado, pero también podrías considerar el uso del isomorfismo de Girard-Reynolds, y mostrar que sólo hay dos pruebas normalizadas de la incrustación de Reynolds del tipo de $\hbox{boolean}$ .

---

Reynolds, J.C. (1983). "Types, abstraction, and parametric polymorphism". Information Processing. North Holland, Amsterdam. pp. 513-523. http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types/Reynolds_typesabpara.pdf

Wadler, Philip (septiembre de 1989). "¡Teoremas gratis!". 4th Int'l Conf. on Functional Programming and Computer Architecture. London. http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875