¿Por qué Coq tiene Prop?

Coq tiene un tipo de Prop. De prueba proposiciones irrelevantes que se descartan durante la extracción. ¿Cuál es la razón para tener esto si usamos Coq solo para pruebas? Prop es impredicativo, por lo que Prop: Prop, sin embargo, Coq infiere automáticamente índices de universo y podemos usar Tipo (i) en todas partes. Parece que Prop complica mucho todo.

Leí que hay razones filosóficas para separar Set y Prop en el libro de Luo, sin embargo, no las encontré en el libro. ¿Qué son?

$\mathtt{Prop}$ es muy útil para la extracción de programas porque nos permite eliminar partes de código que son inútiles. Por ejemplo, para extraer un algoritmo de clasificación, probaríamos la declaración "para cada lista hay una lista tal que está ordenada es una permutatiom de ". Si escribimos esto en Coq y lo extraemos sin usar , obtendremos:k k k ℓ P r o $\ell$$k$$k$$k$$\ell$$\mathtt{Prop}$

1. "para todos hay " nos dará un mapa que lleva listas a listas,$\ell$$k$sort
2. "tal que se ordene " dará una función que corre a través de y verifica que esté ordenada, y$k$verify$k$
3. " es una permutación de " dará una permutación que lleva a . Tenga en cuenta que no es solo un mapeo, sino también el mapeo inverso junto con programas que verifican que los dos mapas son realmente inversos.ℓ ℓ $k$$\ell$pi$\ell$$k$pi

Si bien el material adicional no es totalmente inútil, en muchas aplicaciones queremos deshacernos de él y mantenernos justos sort. Esto se puede lograr si usamos para indicar " está ordenado" y " es una permutación de ", pero no "para todos hay ". k k ℓ ℓ $\mathtt{Prop}$$k$$k$$\ell$$\ell$$k$

En general, una forma común de extraer código es considerar una declaración de la forma donde es input, es salida, y explica lo que significa que sea ​​una salida correcta. (En el ejemplo anterior, y son los tipos de listas y es " está ordenado es una permutación de ".) Si está en entonces extracción da un mapa tal que cumple para todosx y ϕ ( x , y ) y A B ϕ ( ℓ , k ) k k ℓ ϕ P r o p f : A → B ϕ ( x , f ( x ) ) x ∈ A ϕ S e t g g ( x ) ϕ ( x $\forall x : A \,.\, \exists y : B \,.\, \phi(x, y)$$x$$y$$\phi(x,y)$$y$$A$$B$$\phi(\ell, k)$$k$$k$$\ell$$\phi$$\mathtt{Prop}$$f : A \to B$$\phi(x, f(x))$$x \in A$ . Si es decir en entonces también obtenemos una función tal que es la prueba de que sostiene, por todo . A menudo, la prueba es computacionalmente inútil y preferimos deshacernos de ella, especialmente cuando está anidada profundamente en alguna otra declaración. nos da la posibilidad de hacerlo.$\phi$$\mathtt{Set}$$g$$g(x)$x ∈ A P r o $\phi(x, f(x))$$x \in A$$\mathtt{Prop}$

Agregado 2015-07-29: Hay una pregunta sobre si podríamos evitar por completo al optimizar automáticamente el "código extraído inútil". Hasta cierto punto podemos hacer eso, por ejemplo, todo el código extraído del fragmento negativo de la lógica (material construido a partir del tipo vacío, tipo de unidad, productos) es inútil ya que simplemente se baraja alrededor de la unidad. Pero hay decisiones de diseño genuinas que uno debe tomar al usar . Aquí hay un ejemplo simple, donde significa que estamos en y significa que estamos en . Si extraemos de P r o p Σ T y p e ∃ P r o p Π n : N Σ b : { 0 , 1 } Σ k : $\mathsf{Prop}$$\mathsf{Prop}$$\Sigma$$\mathsf{Type}$$\exists$$\mathsf{Prop}$n b k Π n : N Σ b : { 0 , 1 } ∃ k :

$\mathrm{Prop}$

es inconsistente Por lo general, desea mantener la posibilidad de agregar el medio excluido, por lo que una solución es mantener una gran eliminación y hacer que Prop sea predictivo. El otro es suprimir la gran eliminación.

¡Coq hizo las dos cosas! Cambiaron el nombre del Prop predicativo a Establecer y deshabilitaron la eliminación grande en Prop.

La expresividad obtenida por la impredicatividad es "tranquilizadora" en el sentido de que el 99% de las matemáticas "razonables" se pueden formalizar con ella, y se sabe que es consistente en relación con la teoría de conjuntos. Esto hace que sea probable que no lo debiliten a algo como Agda, que solo tiene universos predicativos.

Incluso si no está interesado en extraer programas, el hecho de que Propsea ​​impredecible le permite construir algunos modelos que no puede construir utilizando una torre de universos predicativa. IIRC Thorsten Altenkirch tiene un modelo de Sistema F que usa la impredicatividad de Coq.