sobre - ¿Puedo extraer una prueba de Coq como una función de Haskell?

multiplicar haskell

Question

• Desde que aprendí un poco de Coq, quería aprender a escribir una prueba de Coq del llamado algoritmo de división que en realidad es una proposición lógica: para todos forall nm : nat, exists q : nat, exists r : nat, n = q * m + r
• Recientemente realicé esa tarea usando lo que aprendí de Software Foundations .
• Siendo el Coq un sistema para desarrollar pruebas constructivas, mi prueba es en efecto un método para construir los valores q y r adecuados a partir de los valores n .
• Coq tiene una facilidad intrigante para "extraer" un algoritmo en el lenguaje de algoritmo de Coq (Gallina) a lenguajes de programación funcionales de propósito general, incluido Haskell.
• Por separado, he logrado escribir la operación divmod como un punto de Fixpoint Gallina y extraerla. Quiero señalar cuidadosamente que esa tarea no es lo que estoy considerando aquí.
• Adam Chlipala ha escrito en Programación certificada con tipos de dependientes que "Muchos fanáticos de la correspondencia de Curry-Howard apoyan la idea de extraer programas de pruebas. En realidad, pocos usuarios de Coq y herramientas relacionadas hacen algo así".

¿Es posible extraer el algoritmo implícito en mi prueba a Haskell? Si es posible, ¿cómo se haría?

Answer 1

Gracias al video del verano de 2012 del Prof. Pierce, como sugirió Dan Feltey , vemos que la clave es que el teorema que se va a extraer debe proporcionar un miembro de Type lugar del tipo de proposiciones habitual, que es la Prop .

Para el teorema particular, el constructo afectado es el Prop ex inductivo y su notación exists . De forma similar a lo que ha hecho el profesor Pierce, podemos establecer nuestras propias definiciones alternativas ex_t y exists_t que reemplazan las apariciones de Prop con las ocurrencias de Type .

Esta es la redefinición habitual de ex y exists manera similar a como se definen en la biblioteca estándar de Coq.

Inductive ex (X:Type) (P : X->Prop) : Prop :=
ex_intro : forall (witness:X), P witness -> ex X P.

Notation "''exists'' x : X , p" := (ex _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.

Aquí están las definiciones alternativas.

Inductive ex_t (X:Type) (P : X->Type) : Type :=
ex_t_intro : forall (witness:X), P witness -> ex_t X P.

Notation "''exists_t'' x : X , p" := (ex_t _ (fun x:X => p))
(at level 200, x ident, right associativity) : type_scope.

Ahora, algo desafortunadamente, es necesario repetir tanto la declaración como la prueba del teorema usando estas nuevas definiciones.

¿Qué en el mundo?

¿Por qué es necesario hacer una declaración reiterada del teorema y una prueba reiterada del teorema, que difieran solo al usar una definición alternativa del cuantificador?

Esperaba usar el teorema existente en Prop para probar el teorema nuevamente en Type . Esa estrategia falla cuando Coq rechaza la inversion táctica de prueba para una Prop en el entorno cuando esa Prop exists y la meta es un Type que usa exists_t . Coq informa "Error: la inversión requeriría un análisis de caso en el conjunto de ordenación, lo que no está permitido para la definición inductiva" Este comportamiento ocurrió en la Coq 8.3. No estoy seguro de que todavía ocurra en Coq 8.4.

Creo que la necesidad de repetir la prueba es realmente profunda, aunque dudo que, personalmente, logre percibir su profundidad. Se trata de los hechos de que la Prop es "impredicativa" y el Type no es impredicativo, sino tácitamente "estratificado". La predicción es (si comprendo correctamente) la vulnerabilidad a la paradoja de Russell de que el conjunto S de conjuntos que no son miembros de sí mismos no puede ser un miembro de S, ni un no miembro de S. Type evita la paradoja de Russell al crear tácitamente una secuencia de Tipos más altos que contienen tipos más bajos. Debido a que Coq está empapado en la interpretación de fórmulas-como-tipos de la correspondencia de Curry-Howard, y si lo estoy haciendo bien, incluso podemos entender la estratificación de tipos en Coq como una manera de evitar la incompletitud de Gödel, el fenómeno que expresan ciertas fórmulas. las restricciones en fórmulas como ellas mismas y, por lo tanto, se vuelven desconocidas en cuanto a su verdad o falsedad

De vuelta en el planeta Tierra, aquí está la declaración repetida del teorema usando "existir_t".

Theorem divalg_t : forall n m : nat, exists_t q : nat,
  exists_t r : nat, n = plus (mult q m) r.

Como omití la prueba de divalg , también omitiré la prueba de divalg_t . Solo mencionaré que tenemos la suerte de que las tácticas de prueba que incluyen "existe" e "inversión" funcionan de la misma manera con nuestras nuevas definiciones "ex_t" y "existir_t".

Finalmente, la extracción en sí se realiza fácilmente.

Extraction Language Haskell.

Extraction "divalg.hs" divalg_t.

El archivo de Haskell resultante contiene una serie de definiciones, cuyo núcleo es el código razonablemente bueno que se encuentra a continuación. Y solo estuve un poco obstaculizado por mi casi total ignorancia del lenguaje de programación Haskell. Tenga en cuenta que Ex_t_intro crea un resultado cuyo tipo es Ex_t ; O y S son el cero y la función sucesora de la aritmética de Peano; beq_nat prueba los números de Peano para la igualdad; nat_rec es una función de orden superior que se repite sobre la función entre sus argumentos. La definición de nat_rec no se muestra aquí. En cualquier caso, es generado por Coq de acuerdo con el tipo inductivo "nat" que se definió en Coq.

divalg :: Nat -> Nat -> Ex_t Nat (Ex_t Nat ())
divalg n m =
  case m of {
   O -> Ex_t_intro O (Ex_t_intro n __);
   S m'' ->
    nat_rec (Ex_t_intro O (Ex_t_intro O __)) (/n'' iHn'' ->
      case iHn'' of {
       Ex_t_intro q'' hq'' ->
        case hq'' of {
         Ex_t_intro r'' _ ->
          let {k = beq_nat r'' m''} in
          case k of {
           True -> Ex_t_intro (S q'') (Ex_t_intro O __);
           False -> Ex_t_intro q'' (Ex_t_intro (S r'') __)}}}) n}

Actualización 2013-04-24: Sé un poco más de Haskell ahora. Para ayudar a otros a leer el código extraído arriba, presento el siguiente código reescrito a mano que afirmo es equivalente y más legible. También estoy presentando las definiciones extraídas Nat, O, S y nat_rec que no eliminé.

-- Extracted: Natural numbers (non-negative integers)
-- in the manner in which Peano defined them.
data Nat =
   O
 | S Nat
   deriving (Eq, Show)

-- Extracted: General recursion over natural numbers,
-- an interpretation of Nat in the manner of higher-order abstract syntax.
nat_rec :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
nat_rec f f0 n =
  case n of {
   O -> f;
   S n0 -> f0 n0 (nat_rec f f0 n0)}

-- Given non-negative integers n and m, produce (q, r) with n = q * m + r.
divalg_t :: Nat -> Nat -> (Nat, Nat)
divalg_t n      O = (O, n)      -- n/0: Define quotient 0, remainder n.
divalg_t n (S m'') = divpos n m'' -- n/(S m'')
  where
        -- Given non-negative integers  n and m'',
        -- and defining m = m'' + 1,
        -- produce (q, r) with n = q * m + r
        -- so that q = floor (n / m) and r = n % m.
        divpos :: Nat -> Nat -> (Nat, Nat)
        divpos n m'' = nat_rec (O, O) (incrDivMod m'') n
        -- Given a non-negative integer m'' and
        -- a pair of non-negative integers (q'', r'') with r <= m'',
        -- and defining m = m'' + 1,
        -- produce (q, r) with q*m + r = q''*m + r'' + 1 and r <= m''.
        incrDivMod :: Nat -> Nat -> (Nat, Nat) -> (Nat, Nat)
        incrDivMod m'' _ (q'', r'')
          | r'' == m''  = (S q'', O)
          | otherwise = (q'', S r'')

Answer 2

La copia actual de Software Foundations del 25 de julio de 2012, responde esto de manera bastante concisa en el último capítulo " Extraction2 ". La respuesta es que ciertamente se puede hacer, así:

Extraction Language Haskell
Extraction "divalg.hs" divalg

Un truco más es necesario. En lugar de una Prop , divalg debe ser un Type . De lo contrario se borrará en el proceso de extracción.

Oh, oh, @Anthill tiene razón, no he respondido la pregunta porque no sé cómo explicar cómo el Prof. Pierce logró eso en su variante NormInType.v de su Norm.v y MoreStlc.v.

OK, aquí está el resto de mi respuesta parcial de todos modos.

Donde aparece "divalg" arriba, será necesario proporcionar una lista separada por espacios de todas las proposiciones (las cuales deben ser redefinidas como un Type lugar de una Prop ) en las que se basa el divalg. Para un ejemplo exhaustivo, interesante y funcional de una extracción de prueba, se puede consultar el capítulo Extraction2 mencionado anteriormente. Ese ejemplo se extrae a OCaml, pero adaptarlo a Haskell es simplemente una cuestión de usar Extraction Language Haskell como se Extraction Language Haskell anteriormente.

En parte, la razón por la que pasé un tiempo sin saber la respuesta anterior es que he estado usando la copia de Software Foundations del 14 de octubre de 2010, que descargué en 2011.