Camino a los métodos formales

20

No es raro ver a los estudiantes comenzando sus doctorados con una formación limitada en matemáticas y los aspectos formales de la informática. Obviamente, será muy difícil para tales estudiantes convertirse en científicos teóricos de la computación, pero sería bueno si pudieran aprender a usar métodos formales y leer documentos que contienen métodos formales.

¿Cuál es un buen camino a corto plazo que los estudiantes principiantes de doctorado podrían seguir para obtener la exposición requerida para que lean documentos que involucren métodos formales y eventualmente escriban documentos que usen tales métodos formales?

En términos de contexto, estoy pensando más en términos de Teoría B y verificación formal como el tipo de cosas que deberían aprender, pero también temas clásicos de TCS como la teoría de autómatas.

Dave Clarke
fuente
99
“Joven, en matemáticas no entiendes las cosas. Simplemente te acostumbras a ellos. ”- John von Neumann Lamentablemente, acostumbrarse a esto lleva años, al menos en mi caso :)
uli
1
Me pregunto por qué algunas personas (no necesariamente usted, Dave) piensan que una educación integral de licenciatura / maestría en CS (unos cinco años) puede ser reemplazada por un par de créditos de curso.
Raphael
Por "Teoría B", ¿te refieres al "Método B"? en.wikipedia.org/wiki/B-Method
Steven Shaw
@StevenShaw: No. La teoría B cubre la semántica y demás, en contraste con los autómatas / complejidad.
Dave Clarke
No había oído hablar de la "Teoría B" antes. Pude encontrar esta útil respuesta en cstheory cstheory.stackexchange.com/a/1523/9552
Steven Shaw

Respuestas:

14

En el prefacio de su libro "Descubrimiento matemático, comprensión, aprendizaje y resolución de problemas de enseñanza", George Pólya escribe:

Resolver problemas es un arte práctico, como nadar, esquiar o tocar el piano: solo se puede aprender imitando y practicando. Este libro no puede ofrecerle una llave mágica que abra todas las puertas y resuelva todos los problemas, pero le ofrece buenos ejemplos de imitación y muchas oportunidades para practicar: si desea aprender a nadar, debe ir al agua, y si desea convertirse en un solucionador de problemas, tiene que resolverlos.

Creo que no hay un camino corto, especialmente para alcanzar el estado de escribir documentos. Requiere práctica, mucho.

Algunos punteros:

Si "antecedentes limitados en matemáticas y aspectos formales" significa "nunca ha concebido una prueba y la ha escrito", entonces algo como esto podría ser un comienzo.

Si algo en la Hoja de trucos de Ciencias de la Computación Teórica hace que el estudiante se sienta incómodo, entonces sería recomendable un curso de actualización de la rama correspondiente de las matemáticas.

Hay muchas fuentes para la escritura matemática: quizás las notas de la clase del curso CS209 de la Universidad de Stanford de 1978. O este artículo de Paul Halmos.

uli
fuente
3
No estoy pidiendo un atajo; más bien un camino (que es corto).
Dave Clarke
@JD La pregunta del OP dice "una formación limitada en matemáticas y los aspectos formales de la informática" y "se familiarizan con el uso de métodos formales y la lectura de documentos". Si un estudiante tiene una exposición limitada a los formalismos utilizados en matemáticas y tcs, no es bueno trabajar en un tema teórico. Primero tiene que trabajar en lo básico antes de dar el siguiente paso. Solo apuntaba al inicio del camino.
uli
9

Los métodos formales como Z, B, TLA, CafeObj dependen en gran medida de la teoría de conjuntos, la lógica, la teoría de categorías, el cálculo lambda y los autómatas para modelar los conceptos de tipos, datos y computación.

Puede saltar a una monografía completa como Lógicas de lenguajes de especificación, por Dines Bjørner y Martin C. Henson eds., Monografías en Ciencias de la Computación Teórica, Springer Verlag, 2008 y aprender de lo que necesita, y usar las referencias citadas allí. O aprende un tema a la vez:

  1. Teoría de conjuntos
  2. Lógica matemática
  3. Lógica temporal
  4. Álgebra Universal
  5. Cálculo lambda
  6. Teoría de la categoría

fuente
Buena sugerencia, aunque me preocupa si esa monografía es un poco demasiado densa para empezar. Ciertamente es pesado.
Dave Clarke
5

Realmente creo que los métodos "formales" no son una muy buena idea para fines educativos. Para el caso, programar una computadora es un método "formal". ¿Tiene éxito como herramienta educativa?

Lo que se necesita es comprensión, intuición y la capacidad de lidiar con la abstracción. Los métodos formales dificultan todo eso. Por el contrario, promueven prueba y error, piratería, coincidencia de patrones, imitación, centrándose en la sintaxis. La lista sigue y sigue.

Cualquier pieza de matemática rigurosa enseñará a las personas a razonar correctamente. Cuanto más simple es el dominio, mejor es. Todo lo que aprendí sobre el razonamiento lo aprendí en la escuela secundaria cuando hice en serio la geometría euclidiana. El cálculo y el álgebra lineal en la universidad hicieron el resto.

Otra alternativa atractiva es la lógica filosófica, donde enseñan a las personas cómo pensar sobre las declaraciones y comprender cuál es el contenido de la información y qué es una consecuencia de qué. Lo hacen sin ahogar a los estudiantes en símbolos.

Si hace un balance de todos los mejores informáticos, se sorprendería de cuántos de ellos tienen capacitación formal en filosofía. Estamos perdiendo todo eso ahora porque los estudiantes de filosofía ahora piensan en la informática como una materia mundana. Lograr que nuestros alumnos aprendan algo de filosofía podría contrarrestarlo hasta cierto punto. Haga que trabajen a través de la Historia de la filosofía occidental de Bertrand Russell . Eso hará maravillas.

Si trabajan en la teoría del lenguaje de programación, también puede hacer que lean a Quine, a quien considero como el "dios padre" de la semántica denotacional. (Quine esencialmente estaba haciendo una semántica denotativa del lenguaje natural en Word y Object , que fue una gran fuente de inspiración para Christopher Strachey. Pero este libro es bastante difícil.) La colección editada Quintessence es una buena fuente de ideas de Quine para un principiante.

[Nota agregada: Una ventaja de la filosofía sobre las matemáticas es que los estudiantes pueden ver debate , es decir, pueden ver el argumento "correcto" y el argumento "incorrecto" y ver a los expertos demoler los incorrectos. En matemáticas, uno nunca llega a ver un argumento equivocado, lo que limita su valor educativo.]

Uday Reddy
fuente
Tuve una respuesta ingeniosa, irónica a esto que involucra el cálculo de la duración y un juego de palabras con el nombre de Quine ... pero desafortunadamente lo olvido ...
Dave Clarke