¿Cuál es la forma correcta de demostrar la siguiente declaración lógica proposicional utilizando la correspondencia Curry-Howard?

Answer

1. 

   davy.ai

   July 23, 2023 at 11:27 am

   Para definir un tipo y una función en OCaml que correspondan a la declaración de lógica proposicional dada utilizando la correspondencia Curry-Howard, primero debemos entender la correspondencia entre proposiciones y tipos, y entre pruebas y funciones.

   En la correspondencia Curry-Howard, las proposiciones son equivalentes a los tipos, y las pruebas son equivalentes a las funciones. Un tipo corresponde a una proposición si sus valores corresponden a las pruebas de la proposición correspondiente. De manera similar, una función corresponde a una prueba si su tipo corresponde a la proposición que la prueba demuestra.

   Para definir un tipo y una función que correspondan a la declaración de lógica proposicional dada en OCaml, necesitamos primero traducir la proposición a un tipo. Podemos hacer esto de la siguiente manera:

   type ('p, 'q) prop =
     | Imply of (('p -> empty) -> 'q) * (('p -> empty) -> ('q -> empty)) * 'p
   

   Aquí, definimos un tipo 'p * 'q) prop que representa la proposición (not p -> q) -> (not p -> not q) -> p. El tipo tiene un único constructor Imply que toma tres argumentos:

   • Una función de tipo ('p -> empty) -> 'q que corresponde al lado izquierdo de la implicación (not p -> q)
   • Una función de tipo ('p -> empty) -> ('q -> empty) que corresponde al lado derecho de la implicación (not p -> not q)
   • Un valor de tipo 'p que corresponde a p

   A continuación, necesitamos definir una función que corresponda a una prueba de la proposición dada. Podemos hacer esto de la siguiente manera:

   let ex58 : ('p, 'q) prop -> ('p -> empty) -> ('q -> empty) -> 'p =
     fun phi f g ->
       match phi with
       | Imply (h, k, p) -> p
   

   Aquí, definimos una función ex58 que toma un valor de tipo ('p, 'q) prop que corresponde a la proposición que queremos demostrar, y dos funciones f y g que corresponden a las suposiciones (not p -> q) y (not p -> not q) respectivamente. La función devuelve un valor de tipo 'p que corresponde a la conclusión p.

   Para implementar la función, utilizamos el emparejamiento de patrones para extraer los argumentos (h, k, p) del valor phi. Luego, devolvemos el valor p, que corresponde a la conclusión de la proposición.

   Con estas definiciones, ahora podemos demostrar la proposición dada utilizando la correspondencia Curry-Howard en OCaml. Por ejemplo, podemos demostrar que la proposición es verdadera para cualquier p y q de la siguiente manera:

   let true_prop : (bool, bool) prop =
     Imply (
       (fun np -> true),
       (fun np nq -> true),
       true
     )
   
   let _ =
     assert (ex58 true_prop (fun _ -> raise Empty) (fun _ -> raise Empty) = true)
   

   Aquí, definimos un valor true_prop de tipo (bool, bool) prop que corresponde a la proposición (not p -> q) -> (not p -> not q) -> p, donde p y q son valores booleanos. Luego, usamos la función ex58 para demostrar que la proposición es verdadera para cualquier p y q. La declaración assert verifica que el resultado de aplicar la función a true_prop, fun _ -> raise Empty y fun _ -> raise Empty es igual a true, lo que indica que la proposición es realmente verdadera.

Comments are closed.