pattern matching - language - ¿Qué es el axioma K?

clean programming language

Question

He notado que la discusión de "Axiom K" aparece más a menudo desde HoTT. Creo que está relacionado con la coincidencia de patrones. Me sorprende que no pueda encontrar una referencia en TAPL, ATTAPL o PFPL.

• ¿Qué es el axioma K?
• ¿Se utiliza para la coincidencia de patrones de estilo ML como en SML (o solo para la coincidencia de patrones dependiente)?
• ¿Cuál es una referencia apropiada para Axiom K?

Answer 1

Axiom K también se conoce como el principio de la singularidad de las pruebas de identidad , y es un axioma sobre la naturaleza del tipo de identidad en la teoría de tipos dependiente de Martin-Löf. Este tipo no existe (y, de hecho, no se puede definir) en teorías de tipos más simples como el Sistema F, por lo que probablemente sea la razón por la que no lo ha encontrado en los libros que menciona.

El tipo de identidad se escribe como Id(A,x,y) o también x = y y codifica la propiedad de que x e y son iguales (bajo la correspondencia de Curry-Howard ). Hay una forma básica de dar una prueba del tipo de identidad, y es refl : Id(A,x,x) , es decir, la prueba de que x es igual a sí mismo.

Cuando investigó el tipo de identidad en su thesis , Thomas Streicher introdujo un nuevo eliminador para el tipo de identidad al que llamó K (como la siguiente letra en el alfabeto después de J, el eliminador estándar para el tipo de identidad). Afirma que cualquier prueba p de una igualdad de la forma x = x es en sí misma igual a la prueba trivial refl . De esto, se deduce que cualquiera de las dos pruebas p y q de cualquier ecuación x = y son iguales, de ahí el nombre alternativo "unicidad de las pruebas de identidad". Lo que es notable es que demostró que esto no se sigue de las reglas estándar de la teoría de tipos. Recomiendo leer el artículo de Dan Licata en el blog de homotopy type theory si quieres entender por qué no, él lo explica mucho mejor que yo.

Para responder a la segunda parte de su pregunta: la coincidencia de patrones de estilo ML no está relacionada con K, ya que ML no tiene un tipo de identidad y, por lo tanto, ni siquiera puede formular el axioma K. Por otro lado, K es necesario para la coincidencia de patrones dependientes tal como lo introdujo Thierry Coquand en "Coincidencia de patrones con tipos dependientes (1992)". La razón de esto es que es muy fácil probar K mediante la coincidencia de patrones en el refl del constructor del tipo de identidad:

K : (p : x = x) -> p = refl
K refl = refl

De hecho, Conor McBride demostró en su tesis ("Programas funcionales dependientes de tipos y sus pruebas (2000)") que K es la única cosa que la coincidencia de patrones dependiente realmente agrega a la teoría de tipos dependientes.

Mi propio interés en este tema es comprender exactamente por qué la coincidencia de patrones dependiente requiere K y cómo puede restringirse, por lo que ya no lo es. El resultado fue un paper y una nueva implementación de la opción --without-K en Agda. La idea básica es que el algoritmo de unificación utilizado para el análisis de casos durante la coincidencia de patrones dependientes no debe eliminar las ecuaciones de la forma x = x , ya que hacerlo requiere K. Le recomiendo que lea la (introducción de) el documento si desea saberlo. Más.