Experiencias comunitarias de redacción de pruebas estructuradas de Lamport

Question

Hace unos dos años, me encontré con este documento de Lamport

http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf

sobre la escritura de las pruebas de forma jerárquica. Cambió mi forma de escribir todas las pruebas durante unos seis meses e identificó muy bien las lagunas en mi comprensión y conocimiento. Hoy en día, no lo utilizo para las pruebas más sencillas, pero me resulta indispensable cuando quiero comprender a fondo las más largas y complejas.

Creo que esto es potencialmente una herramienta pedagógica maravillosa, en el sentido de que todos los pasos y supuestos están organizados y se pueden consultar fácilmente, y también es útil para la autocomprobación. En el blog se ha debatido sobre la supuesta prueba de Deolalikar de $P\neq NP$ Para dar un ejemplo, el profesor Tao observaciones oportunas sobre la necesidad de precisión, (15 de agosto de 2010, 15:05 - Espero que no le importe que le cite)

Una cosa que esto ilustra es la importancia de establecer definiciones definiciones. Creo que si Deolalikar hubiera escrito una definición precisa de lo que significa que un espacio de solución sea polilógicamente parametrizable, el dificultades se habrían encontrado mucho antes mucho antes, y en particular probablemente por el propio Deolalikar, mucho antes de que de que terminara el preprint para compartirlo con otros.

me recordó el ensayo de Lamport. Lamport comenta algo similar a partir de su propia experiencia:

El estilo se aplicó por primera vez a las pruebas de teoremas ordinarios en un artículo que escribí con Martín Abadi. Tenía ya había escrito pruebas convencionales pruebas convencionales que eran lo suficientemente buenas para convencernos a nosotros y, presumiblemente, a los árbitros. Reescribiendo las pruebas en un estilo estilo estructurado, descubrimos que casi todas tenían errores graves errores, aunque los teoremas eran correctos. Cualquier esperanza de que las pruebas incorrectas no condujeran a teoremas incorrectos teoremas incorrectos fue destruida en nuestra siguiente colaboración. Una y otra vez, hacíamos una conjetura y escribíamos un un esbozo de prueba en la pizarra, un un esbozo que podría haberse convertido convertirse en una prueba convencional convincente convencional convincente, para luego descubrir, al intentar de escribir una prueba estructurada, que la conjetura era falsa. Desde entonces, nunca nunca he creído en un resultado sin una una prueba estructurada y cuidadosa. Mi escepticismo ha ayudado a evitar numerosos errores.

¿Alguien ha tenido experiencia con este estilo de redacción de pruebas?

Answer 1

Desde el punto de vista de la teoría de la prueba, Lamport sugiere esencialmente escribir pruebas en estilo de deducción natural, junto con un sistema de convenciones para estructurar las pruebas según el nivel de detalle pertinente. (Sería muy interesante estudiar cómo formalizar este tipo de convenciones -- es algo común en la práctica matemática que falta en la teoría de las pruebas).

He escrito pruebas en este estilo, y una vez lo enseñé a los estudiantes. Me parece que este sistema -o cualquier variante de la deducción natural- es extremadamente valioso para la enseñanza de la demostración a los alumnos, porque asocia a cada conectivo lógico el lenguaje matemático exacto necesario para utilizarlo y construirlo. Esto es especialmente útil cuando se enseña a los alumnos a manipular cuantificadores y a utilizar el axioma de inducción.

Cuando hago pruebas yo mismo, encuentro que este tipo de prueba estructurada funciona fantásticamente bien, excepto cuando se trabaja con cocientes, es decir, modulo una relación de equivalencia. La razón es que las reglas de deducción natural para los tipos de cociente son bastante complicadas. Introducir elementos de un conjunto módulo una relación de equivalencia es bastante natural:

$$\frac{\Gamma \vdash e \in A \qquad R \;\mathrm{equivalence\;relation}} {\Gamma \vdash [e]_R \in A/R}$$

Es decir, sólo tenemos que producir un elemento de $A$ y luego decir que estamos hablando de la clase de equivalencia de la que es miembro.

Pero utilizar este hecho es bastante doloroso:

$$\frac{\Gamma \vdash e \in A/R \qquad \Gamma, x\in A \vdash t \in B \qquad \Gamma \vdash \forall y,z:A, (y,z) \in R.\;t[y/x] = t[z/x]}{\Gamma \vdash \mbox{choose}\;[x]_R\;\mbox{from}\;e\;\mbox{in}\;t \in B}$$

Esta regla dice que si usted sabe que

• $e$ es un elemento de $A/R$ y
• $t$ es algún elemento de $B$ con una variable libre $x$ en conjunto $A$ y
• si se puede demostrar que para cualquier $x$ y $y$ en $R$ que $t(y) = t(z)$ (es decir, $t$ no distingue entre elementos de la misma clase de equivalencia)

Entonces puede formar un elemento de $B$ eligiendo un elemento de la clase de equivalencia y sustituyéndolo por $x$ . (Esto funciona porque $t$ no le importa la elección concreta del representante).

Lo que hace que esta regla sea tan desgarbada es la premisa de la igualdad: requiere demostrar algo sobre toda la subderivación que utiliza el miembro del conjunto cociente. Es tan doloroso que tiendo a evitar las pruebas estructuradas cuando trabajo con cocientes, aunque es cuando más los necesito (ya que es muy fácil olvidarse de trabajar mod la relación de equivalencia en un pequeño rincón de la prueba).

Pagaría dinero por una mejor regla de eliminación de cocientes, y tampoco estoy seguro de que lo diga como una figura retórica.