ser - ¿Cuáles son las fortalezas y debilidades del asistente de pruebas Isabelle en comparación con Coq?

test de fortalezas y debilidades profesionales

Question

¿El asistente de prueba Isabelle / HOL tiene debilidades y fortalezas en comparación con Coq?

Answer 1

Como "Isabelle / HOL" se precisa en la pregunta, hablaré sobre la lógica HOL utilizada en Isabelle, que creo que es la mejor para comparar con Coq. No soy un experto en sistemas de tipos y lógicas, pero creo que lo que digo aquí es correcto, al menos aproximadamente. Esto también es sin duda una cuestión de gustos ;-) y mi respuesta puede ser subjetiva.

Las diferencias más profundas radican en los sistemas de tipos y la lógica.

Diría que la fortaleza es ser más natural para alguien que conoce un lenguaje funcional de la familia ML (y aún más para alguien que conoce SML) y utiliza un enfoque pragmático para resolver problemas como, por ejemplo, el uso de una lógica clásica como una base Su sistema de tipos es cercano al de Hindley Milner y termina de manera predeterminada (si el usuario no lo modifica).

Por otro lado, Coq es más estricto y utiliza una lógica intuicionista. Tiene un sistema de tipos especializado con varias órdenes y permite dependencias de tipos que pueden ser más difíciles de manejar y pueden no terminar en algunas circunstancias. También permite extraer programas de pruebas (que pueden ser relativamente ineficientes) que no es directamente posible en Isabelle.

Answer 2

Estoy familiarizado con Coq, y no tengo mucha experiencia con Isabelle / HOL, pero podría ayudarlo un poco. Quizás otros con más experiencia en Isabelle / HOL puedan ayudar a mejorar esto.

Hay dos grandes puntos de divergencia entre los dos sistemas: las teorías subyacentes y el estilo de interacción . Trataré de dar una breve descripción de las principales diferencias en cada caso.

Teorías

Tanto Coq como Isabelle / HOL se basan en lógicas de orden superior potentes y muy expresivas. Estas lógicas, sin embargo, difieren en algunas características:

Tipos dependientes

La lógica de Coq es una teoría de tipo dependiente, conocida como el cálculo de construcciones inductivas ( CIC para abreviar). "Tipo dependiente" aquí significa que los tipos en Coq pueden referirse a valores ordinarios. Por ejemplo, uno puede escribir una función de multiplicación de matrices mult con tipo

mult : forall (n m p : nat), matrix n m -> matrix m p -> matrix n p

El tipo de esta función dice que toma dos matrices como entradas, una de dimensión nxm y otra de dimensión mxp , y devuelve una matriz de dimensión nxp . La teoría de Isabelle / HOL, por otro lado, no posee tipos dependientes; por lo tanto, no se puede escribir una función mult con el mismo tipo que la anterior. En cambio, uno tendría que escribir una función que funcione para cualquier tipo de matriz, y demostrar a posteriori ciertas propiedades de esta función cuando recibe argumentos del tipo correcto. En otras palabras, ciertas propiedades que se manifiestan en los tipos Coq deben afirmarse como teoremas separados cuando se trabaja en Isabelle / HOL.

Si bien los tipos dependientes son interesantes para algunas cosas, no está claro qué tan útiles son en general. Mi impresión es que algunos sienten que son muy complicados de usar, y que el beneficio de tener ciertas propiedades expresadas a nivel de tipo frente a tenerlas como teoremas separados no vale esta complejidad adicional. Personalmente, me gusta usar tipos dependientes en algunos casos, cuando hay una razón clara para hacerlo.

Principios básicos de razonamiento

La teoría de Coq por defecto carece de muchos principios de razonamiento que son comunes en la práctica matemática, como la ley del medio excluido (es decir, la capacidad de razonar de manera no constructiva), la extensionalidad (por ejemplo, poder decir que funciones que producen resultados iguales) son iguales) y el axioma de elección. En Isabelle / HOL, por otro lado, tales principios están incorporados.

En teoría, este no es un gran problema, porque la lógica de Coq fue diseñada para permitir a las personas agregar de manera segura estos principios de razonamiento como axiomas adicionales. Sin embargo, tengo la impresión de que es más fácil hacer este tipo de razonamiento en Isabelle / HOL, ya que la lógica se construyó desde cero para apoyarlos.

(Quizás se pregunte cuál es la razón para dejar tales principios básicos fuera de la lógica de Coq. La motivación es filosófica: en la lógica central de Coq, las pruebas pueden verse como programas ejecutables, lo que le da a la lógica un sabor constructivo. La razón para rechazar a los excluidos el medio, por ejemplo, es que la prueba de una disyunción A // B corresponde a un programa que devuelve un bit que indica cuál de A o B es verdadero; por lo tanto, el medio excluido correspondería a un programa que decidió cada pregunta matemática, que no puede existir. Esta pregunta discute el tema un poco más).

Estilo de interacción

Tanto Coq como Isabelle / HOL son probadores de teoremas interactivos . Son idiomas para escribir definiciones y pruebas sobre ellos; Estas pruebas son verificadas por una computadora para asegurarse de que no tengan errores. En ambos sistemas, uno escribe una prueba dando comandos que explican cómo probar algo. Sin embargo, la forma en que esto sucede en cada sistema varía.

Isabelle / HOL en general tiene un soporte más maduro para la automatización a prueba de "botones". Por ejemplo, viene con la famosa táctica de sledgehammer , que invoca varios probadores y solucionadores de teoremas automáticos externos para tratar de probar un teorema. Coq también viene con muchos potentes procedimientos de automatización de pruebas, como omega o congruence , pero no son tan aplicables en general, y muchos teoremas que se pueden resolver con un solo comando en Isabelle / HOL requieren pruebas más explícitas en Coq.

Por supuesto, esta conveniencia tiene un precio. Me han dicho que es más difícil tener control sobre la prueba en Isabelle / HOL porque el sistema intenta hacer mucho por sí mismo. Esto no es un problema cuando se prueban teoremas simples, pero se convierte en un problema cuando la automatización de pruebas no es lo suficientemente poderosa y necesita decirle al probador de teoremas cómo proceder con mayor detalle.

La situación es un poco diferente cuando se admiten procedimientos de automatización de pruebas definidos por el usuario. Coq viene con un lenguaje táctico para escribir pruebas, conocido como Ltac, que es un lenguaje de programación por derecho propio. Aunque Ltac tiene algunos problemas de diseño, sí permite a los usuarios codificar procedimientos de automatización de pruebas bastante complicados de una manera ligera. Para tareas más pesadas, Coq también permite a los usuarios escribir complementos en el lenguaje de implementación de Coq, OCaml. En Isabelle / HOL, por el contrario, no existe un lenguaje de automatización de nivel superior como Ltac, y la única forma en que el usuario puede programar procedimientos de automatización de prueba personalizados es con complementos.

Answer 3

Un aspecto, que ilustraré, de la eficacia de "pulsador" de Isabelle / HOL es su automation del clásico argumento de "diagonalización" de Cantor (recuerde que esto afirma que no hay un rechazo de los naturales a su poder, o más generalmente cualquier conjunto a su conjunto de potencia).

theorem Cantor: "∄f :: ''a ⇒ ''a set. ∀A. ∃x. A = f x"
proof
  assume "∃f :: ''a ⇒ ''a set. ∀A. ∃x. A = f x"
  then obtain f :: "''a ⇒ ''a set" where *: "∀A. ∃x. A = f x" ..
  let ?D = "{x. x ∉ f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a ∈ ?D ⟷ a ∉ f a" by blast
  ultimately show False by blast
qed

Lo que les acabo de presentar sería la traducción del argumento clásico de Cantor al Isabelle / HOL. Sin duda, ingenioso! Sin embargo, Isabelle / HOL puede automatizar el conocimiento incluso de esta prueba:

theorem "∄f :: ''a ⇒ ''a set. ∀A. ∃x. f x = A"
  by best

theorem "∄f :: ''a ⇒ ''a set. ∀A. ∃x. f x = A"
  by force

El sistema de prueba puede probar automáticamente la declaración de Cantor. Para un investigador, por un lado, esto es útil, pero hay un sentido en el que se trata de una espada de doble filo. Puedo encontrar útil que se pueda confiar internamente en las declaraciones verdaderas tan complejas como un argumento de diagonalización ante Isabelle / HOL, ya que mis teoremas son más sofisticados. Por otro lado, cuanto más avanzo en mi investigación impulsada por el progreso automatizable de la computadora, puedo explicar cada vez menos por qué o por qué principio el teorema es verdadero. ¡Solo la computadora sabe por qué, si solo podemos preguntarlo!