¿Alguien realmente publica "pruebas estructuradas"?

En 1995, Leslie Lamport publicó un ensayo en el American Mathematical Monthly titulado "Cómo escribir una prueba". En el ensayo, Lamport introdujo el concepto de prueba estructurada , en el que la prueba tradicional de alto nivel se complementa con una secuencia de niveles inferiores. Cada nivel de prueba expande cada paso del nivel superior en subpasos. La cantidad de detalles en el nivel más bajo es bastante extrema: la prueba de Lamport de la irracionalidad de la raíz cuadrada de 2 se extiende a 1,5 páginas.

El ensayo tiene más de 250 citas según Google Scholar, pero nunca he visto una prueba publicada en este formato. En un PDF o en papel, el detalle extremo puede ser abrumador; pero creo que las plataformas de publicación web modernas podrían acomodarlo muy bien (con subsecciones plegables jerárquicas para cada parte de la prueba).

En todo caso, ¿existen ejemplos de pruebas publicadas en el formato sugerido por Lamport ?

Me gusta la idea plegable! ¿Ha preguntado sobre esto en matheducators.stackexchange.com ? Parece que esto sería especialmente útil para los estudiantes.
No es exactamente el mismo formato, pero mira el trabajo de Roland Backhouse o Richard Bird.
Conozco algunos libros de texto que funcionan de esa manera. Aunque, en lugar de incluir subpruebas, se presentaron como teoremas/lemas separados.
Aparece una prueba estructurada en el artículo de Lamport sobre Paxos research.microsoft.com/en-us/um/people/lamport/pubs/… (§2.1). Dicho esto, no estoy seguro de si esta prueba exhibe las ventajas que generalmente se supone que tiene una prueba estructurada, como una mayor legibilidad y falta de lógica implícita... (Creo que su Paso 4 en la Prueba del lema necesita más justificación, y El paso 5 dice algo diferente de lo que quiere decir).
En algún lugar de Internet hay un libro completo lleno de pruebas estructuradas (a la Lamport, y tal vez incluso con su coautoría). Por lo que recuerdo, su objetivo es probar la corrección de algún software, pero una buena parte son matemáticas básicas; ¿alguien puede encontrarlo?
Por cierto: esto debería ser una pregunta de mathoverflow o math.stackexchange.
¡Ah, encontré ese libro! Thomas L. Rodeheffer, El protocolo de reloj Naiad: especificación, verificación de modelo y prueba de corrección , research.microsoft.com/apps/pubs/?id=183826 .
Aparentemente, research.microsoft.com/en-us/um/people/lamport/tla/… es una buena introducción a las pruebas estructuradas, con muchos ejemplos.
Todo hasta ahora en los comentarios y la única respuesta actual indica que puede encontrar muchas pruebas estructuradas, y cada una de ellas tiene la mano de Lamport. Entonces, aparentemente, nadie más que Lamport y sus compañeros de trabajo en MS lo usan.
También está la prueba para el sistema Memoir (390 páginas).
pf2htmles un latex2htmlestilo que implementa pruebas estructuradas jerárquicas contraíbles para el pf.sty.

Respuestas (1)

Si bien la mayoría de la gente usa estilos de prueba más tradicionales, el estilo de prueba estructurada más exhaustivo que propone Lamport parece ser adoptado, al menos en espíritu, por sistemas de prueba asistidos por máquina como Coq y el propio TLA + de Lamport . Al traer un jugador muy poco intuitivo al bucle (la máquina), estos sistemas obligan al matemático a ser mucho más explícito sobre cada paso y suposición, y fomentan la estructura jerárquica mediante el uso de la sintaxis del estilo del lenguaje de programación.

Estos sistemas de prueba suelen ser bastante caros de usar y, por lo general, no querrá poner sus largas pruebas en medio de un documento; adjuntar información complementaria es más el camino a seguir. Sin embargo, están demostrando ser bastante valiosos en aplicaciones críticas donde es importante tratar todos los casos extremos posibles, como en el diseño de microprocesadores o protocolos criptográficos.

Las pruebas modernas de Coq escritas en ssreflect (p. ej., github.com/hivert/Coq-Combi ) ¡en realidad no son tan largas! Los problemas, por lo que puedo discernir (desafortunadamente) desde lejos, son (1) que el formato Coq no admite fácilmente la legibilidad humana (es muy difícil seguir una prueba Coq en lápiz y papel), (2) que la falta de extensionalidad de funciones y (falta de) buen soporte para setoides hacen que muchas construcciones matemáticas sean increíblemente difíciles de manejar (olvídese de codificar una tupla de elementos de $A$ como un mapa $\left\{1,2,\ldots ,n\derecha\} \a A$; el...
... ssreflect personas, por el contrario, parecen definir mapas entre conjuntos finitos como tuplas con ciertas propiedades, ¡solo porque las tuplas saben cómo ser iguales!), y (3) que la infraestructura todavía está en constante cambio y las pruebas podrían romperse con la próxima actualización de Coq o ssreflect. Pero esto es absolutamente algo que funcionará algún día.
Y yo estaba como "¿por qué diablos no funciona mi LaTeX?". Esta pregunta realmente debería estar en mathoverflow.
¡Gracias! Esto es interesante, aunque no creo que estos sean ejemplos de exactamente lo que pedí.
¿Alguien realmente publica "pruebas estructuradas"?
RespuestasAquíPolítica de privacidad1y, 0v