Razonamiento formalizado en análisis numérico
Hoy se ha publicado en arXiv el artículo Formal Proof of a Wave Equation Resolution Scheme: the Method Error escrito por Sylvie Boldo (INRIA Saclay – Ile de France, LRI), Francois Clement (INRIA Rocquencourt), Jean-Christophe Filliâtre (INRIA Saclay – Ile de France, LRI), Micaela Mayero (LIPN, INRIA Rhône-Alpes / LIP Laboratoire de l’Informatique du Parallélisme), Guillaume Melquiond (INRIA Saclay – Ile de France, LRI) y Pierre Weis (INRIA Rocquencourt).
En este trabajo se presenta una formalización en Coq de una parte del conocimiento matemático más usado en las ingeniería: las ecuaciones diferenciales. Curiosamente las ecuaciones diferenciales apenas se han tratado dentro del razonamiento formalizado.
Uno de los objetivos del trabajo es favorecer el uso de los métodos formales en el análisis numérico. Aunque pueda parecer una quimera, es una necesidad en matemáticas aplicadas.
Entre las conclusiones del trabajo destaco las siguientes:
- Algunas demostraciones usuales son superficiles, ya que no precisan las hipótesis necesarias y suelen tener lagunas.
- Para llenar las lagunas hay que generalizar los teoremas y masajear las demostraciones.
- La formalización del razonamiento requiere mucho trabajo: la formalización del trabajo tiene 4.500 líneas de código, una demostración usual ocupa 10 páginas y una detallada ocupa 60 páginas. La formalizada es equivalente a la detallada.
- La mitad del trabajo forma librerías reutilizables en otras formalizaciones.
Un estudio detallado del este artículo y la formalización podría ser expuesto en el Seminario del Grupo de Lógica Computacional.
También sería interesante estudiar cómo formalizar el análisis numérico en los sistemas que utilizamos en nuestro grupo (ACL2, PVS, Isabelle/Isar).