Libros sobre semántica del lenguaje de programación

31

He estado leyendo " Semántica con aplicaciones " de Nielson & Nielson , y realmente me gusta el tema. Me gustaría tener un libro más sobre semántica del lenguaje de programación, pero realmente solo puedo obtener uno.

Eché un vistazo al libro de Turbak / Gifford , pero es demasiado largo; Pensé que Winskel estaría bien, pero no tengo acceso a él (no está en nuestra biblioteca de la Universidad, y tengo poco dinero), y ni siquiera estoy seguro de si no está fechado. Slonneger parece estar bien, pero la parte práctica lo hace demasiado largo, y no estoy muy cómodo con su estilo.

Entonces mi pregunta es: ¿es Winskel un buen libro? ¿Y está anticuado?

Además, ¿hay otros libros concisos sobre el tema?

reference-request pl.programming-languages semantics denotational-semantics books Arrendajo
fuente
55
enlaces agregados a las páginas del editor para todos los libros. podría ser útil para otras personas que buscan navegar.
Suresh Venkat
2
¿Qué tipo de semántica le interesa? Denotacional? ¿Operacional? ¿Una visión general?
Ohad Kammar
@Ohad Kammar: Estoy interesado en ambos.
Jay

Respuestas:

31

Todo depende de qué tan profundo quieras llegar y cuánto ya sabes. Para un principiante, el libro de Winksel es realmente agradable, pero sí, no te está presentando el estado de la semántica tal como se escribió hace unos 20 años. Sin embargo, sigue siendo una buena primera introducción al tema. También podría valer la pena señalar que T. Nipkow ha formalizado una parte sustancial del libro de Winskel en Isabelle / HOL, ver aquí . Entonces, si desea aprender utilizando asistentes de prueba interactivos junto con la comprensión de la semántica de los lenguajes de programación, tiene mucho material coherente para aprovechar.

Otros libros que son más avanzados son:

  • Gunter, Semántica de lenguajes de programación , un libro más avanzado que se centra en la semántica denotacional, un enfoque de la semántica, que no ha estado a la altura de las expectativas. Se centra en lanugages puramente funcionales e ignora la concurrencia. Este es el libro del que me enseñé semántica cuando era estudiante y, en retrospectiva, desearía haber usado el libro de Winksel. Gunter no es una lectura fácil para un principiante.

  • Dominios y cálculos lambda de Amadio y Curien. Otro libro que viene escrito más en la tradición teórica del dominio, aunque discute los cálculos del proceso.

  • Los libros de John Mitchell que ya se han mencionado anteriormente. También son principalmente sobre computación secuencial.

Los libros como TAPL de Pierce son muy agradables, pero se centran estrechamente en un aspecto de los lenguajes de programación, a saber, los tipos, tan importantes como eso. No lo recomendaría como una primera introducción al área general de lenguajes de programación, pero es obligatorio leer para cualquiera que quiera aprender sobre tipos.

A decir verdad, creo que actualmente no hay un libro introductorio actualizado sobre semántica del lenguaje que refleje el progreso sustancial que ha visto la última década, con su cambio decisivo de los métodos denotacionales y el cálculo secuencial a la concurrencia (cálculo de procesos y semántica de juegos) , semántica axiomática y el uso de asistentes de prueba interactivos en la verificación.

Actualización 22. Abril 2014: Tobias Nipkow y Gerwin Klein han publicado un nuevo libro

que se puede ver como 'Winskel en Isabelle / HOL'. Es una introducción a la semántica de los lenguajes de programación (principalmente operativos y axiomáticos), pero a diferencia de los enfoques anteriores basados ​​en lápiz y papel, este libro expresa todas sus matemáticas en Isabelle / HOL. En otras palabras, es al mismo tiempo un libro sobre demostración de teoremas.

El libro es completamente nuevo, así que no lo he usado para enseñar, pero parece realmente adecuado como una introducción que se presenta en un nivel más bajo que Software Foundations de Pierce et al.

Martin Berger
fuente
2
¿Hay un cambio de los métodos denotacionales? Me parece más como el tipo de personas que anteriormente usarían pruebas onduladas a mano, hoy en día se espera que produzcan pruebas formales. Como los métodos denotacionales aún no pueden modelar fácilmente todo lo que hacemos, y requieren muchos más requisitos previos, esos investigadores usan métodos más accesibles, como juegos, cálculos de procesos, asistentes de pruebas. No estoy seguro de si hay una disminución en los métodos de denotación.
Ohad Kammar el
44
No confunda la semántica denotacional con la teoría de dominios . La semántica del juego puede ser, y generalmente es, perfectamente denotacional, es decir, el significado de un programa es una función de los significados de sus partes.
Andrej Bauer
2
He abierto un nuevo hilo sobre este comentario. Pero incluso si no estoy seguro de estar de acuerdo con su definición, la semántica del juego es de naturaleza denotacional. Creo que debería reemplazar "juegos" con "semántica operativa" en mi comentario, e incluir la semántica de juegos como posiblemente otra forma de investigación semántica denotacional. cstheory.stackexchange.com/questions/3577/…
Ohad Kammar
1
No estoy convencido de que haya un cambio. Vea mi primer comentario, a la luz del comentario de Andrej.
Ohad Kammar, el
1
¿Hay un cambio? Una pregunta interesante ¿Cómo podemos medir un turno? Hay tantos criterios que podríamos aplicar, desde los relativamente concretos como la cantidad de subvenciones de investigación otorgadas a diferentes enfoques, hasta ideas vagas como compartir la mente. Dado lo involucrados que somos, como investigadores, como empleados, como solicitantes de subvenciones, estamos en el resultado de tal pregunta, es poco probable que estemos de acuerdo con una respuesta.
Martin Berger, el
20

Aquí hay una muestra aleatoria de materiales disponibles gratis en línea:

  • Winskel, La semántica formal de los lenguajes de programación , vista previa de Google Books . No sé nada sobre este libro. Está en la lista porque la pregunta se refiere específicamente a su contenido, que está en línea, principalmente.
  • Morgan, Programación desde la especificación , lista de archivos ps . El tema es el refinamiento, que es el proceso de comenzar con descripciones no ejecutables de alto nivel y luego transformarse sistemáticamente en algo ejecutable. Por supuesto, cada paso de refinamiento debe preservar la semántica, por lo que también se analiza un cierto tipo de semántica (basada principalmente en formadores de predicados).
  • Harper, Fundamentos prácticos de lenguajes de programación , pdf del borrador . Vea el comentario de Dave Clarke a continuación.
  • Remy, uso, comprensión y desentrañando el lenguaje OCaml , pdf . Este es el libro del que aprendí programación funcional (OCaml, más precisamente) y me gustó mucho . Presenta la semántica de las características básicas del lenguaje de una manera muy agradable y en el proceso presenta el cálculo lambda y la teoría de tipos sobre la base de `` necesita saber ''.
  • Peyton Jones, La implementación de lenguajes de programación funcional , djvu . Los primeros capítulos describen el cálculo lambda (y su 'semántica operativa') y cómo las características del lenguaje de nivel superior se eliminan en el cálculo lambda. En este sentido, el documento ofrece una semántica operativa para lenguajes funcionales.
  • Pierce (ed), Temas avanzados en tipos y lenguajes de programación , vista previa de Google Books .
  • Slonneger, sintaxis y semántica de lenguajes de programación , lista de archivos pdf . Lo miré brevemente hace mucho tiempo y no me gustó mucho. Está en la lista porque se menciona en la pregunta.
  • Brookes, Una semántica para la lógica de separación concurrente , pdf . Este es un gran artículo (80 páginas), no un libro. Lo incluí porque es un desarrollo bastante reciente que me parece interesante.
Radu GRIGore
fuente
1
eso es un montón de enlaces :)
Suresh Venkat
3
Esto sería más útil si se hubiera presentado como una lista. De todos modos, recomendaría el libro de Harper: haga clic en "podría".
Dave Clarke
Estoy de acuerdo. Radu, ¿podrías enumerar los libros para que sepamos en qué estamos haciendo clic? Este sería un excelente recurso.
Suresh Venkat
Es una lista ahora. (La primera versión fue publicada alrededor de las 2am, después de dormir alrededor de las 5h la noche anterior.: P)
Radu GRIGore
16

Dividiría los libros sobre semántica del lenguaje de programación en dos clases: los que se centran en modelar conceptos de lenguaje de programación y los que se centran en los aspectos fundamentales de la semántica. No hay razón para que un libro no pueda hacer ambas cosas. Pero, por lo general, solo hay mucho que puedes poner en un libro, y los autores también tienen sus propias predisposiciones sobre lo que es importante.

El libro de Winskel, ya mencionado, hace un poco de ambos aspectos. Y, es un buen libro para principiantes. Un libro igualmente bueno, tal vez incluso mejor, es con el que comencé: la descripción denotacional de Gordon de los lenguajes de programación . Este fue mi primer libro sobre semántica, que leí poco después de terminar mi trabajo de pregrado. Tengo que decir que me dio una base sólida en semántica y nunca tuve que preguntarme cómo la semántica denotacional difiere de la semántica operativa o semántica axiomática, etc. Este libro seguirá siendo mi favorito de todos los tiempos en semántica denotacional.

Otros libros que se centran en aspectos de modelado en lugar de aspectos fundamentales son los siguientes:

  • La semántica de Tennent de los lenguajes de programación , que es un libro más o menos actualizado sobre la semántica de los lenguajes de programación imperativos. Es facil de leer. Sin embargo, tiende a ser abstracto en partes posteriores del libro y es posible que tenga que luchar para ver por qué las cosas se están haciendo de una manera particular.

  • Teorías de Reynolds sobre lenguajes de programación . Cualquiera que se especialice en semántica definitivamente debería leer este libro. Después de todo, es de Reynolds. (David Schmidt me comentó una vez, "incluso si Reynolds te está leyendo el periódico de la mañana, ¡quieres escuchar con atención, porque podrías aprender algo importante"!) Tiene una buena cobertura tanto de los aspectos de modelado como de los aspectos fundamentales.

Los mejores libros sobre aspectos fundamentales son el de Gunter (que considero un libro de texto de posgrado) y el de Mitchell (que es un buen libro de referencia para tener en su estantería porque es bastante completo).

Uday Reddy
fuente
¡Es muy agradable tenerte aquí, Uday!
Radu GRIGore
Me alegro de estar aquí también. Este es un recurso muy bueno!
Uday Reddy
Qué tal: Transiciones y árboles: una introducción a la semántica operacional estructural de Hans Hüttel 2010. Parece tener buenas críticas, pero nadie lo menciona aquí.
Arturo Hernández
1
@Uday: Gracias por la respuesta. ¿Qué significa "modelar conceptos de lenguaje de programación" y "los aspectos fundamentales de la semántica"? ¿Cuáles son sus diferencias y relaciones?
Tim
1
@Tim: Para dar la semántica de un lenguaje de programación, necesita formar estructuras matemáticas, por ejemplo, conjuntos en el caso más simple, pero estructuras sofisticadas como dominios, categorías, coalgebras, etc. para problemas que los conjuntos no pueden manejar. Por "aspectos fundamentales", me refiero a la teoría de estas estructuras más sofisticadas. En el primer caso, el foco está en los lenguajes de programación y, en el último caso, está en los fundamentos matemáticos.
Uday Reddy
8

Realmente disfruté leyendo Winskel cuando estaba tomando el curso de pregrado sobre semántica. Sin embargo, no puedo decir si está anticuado, ya que no investigo en este campo. Una ventaja de Winskel es que puedes encontrarlo traducido en otros idiomas además del inglés.

Para una lectura adicional, más a nivel de posgrado, sugeriría los libros de John Mitchell, Fundamentos para lenguajes de programación y Conceptos en lenguajes de programación . Si lees solo los primeros capítulos, supongo que también cumplen con tu requisito de concisión.

No encontrará borradores gratuitos de estos libros, así que si tiene un presupuesto restringido, busque el "poder" en la respuesta de Radu.

Alessandro Cosentino
fuente
6

Bueno, no soy un experto en el tema, pero hay algunos consejos generales que puedo dar.

Primero, hay algunas personas que ya han leído el libro y han proporcionado reseñas sobre él. Por ejemplo, para el libro de Winskel La semántica formal de los lenguajes de programación (ver [1] y [2] ) encontré reseñas en Amazon.

Parte de una revisión dice:

Este libro confunde entre sintaxis y semántica desde el principio, como separar los literales de sus valores. No se utilizaron anotaciones especiales para diferenciarlos. Este es un tema crucial que el autor debe abordar en un tema como este. Además, algunas otras anotaciones que utilizó son bastante confusas, como mostrar las premisas y conclusiones.

El autor pareció suponer que tiene TODOS los requisitos previos necesarios, ya que explicó los materiales de fondo en los primeros capítulos (es decir, teoría de conjuntos, semántica operativa, inducciones, definiciones inductivas) muy brevemente. El estilo que el autor usó en la introducción es poner dos o tres párrafos de textos y poner algunas fórmulas y luego hacer ejercicios. Lo cual es, para mí, bastante frustrante ...

A 18/20 personas les parece útil la reseña. Puede buscar Amazon (u otras fuentes) para ver más reseñas.

En segundo lugar, Amazon ofrece tipos y lenguajes de programación y teoría de categorías básicas para informáticos junto con este libro. En otro tema, Dave Clarke ofrece estos libros como excelentes sobre "Sistemas de tipos y semántica de lenguaje de programación". De nuevo, no soy un experto, pero podrían ser útiles para usted.

MS Dousti
fuente
TaPL va demasiado lento para mi gusto. Es un buen libro, pero lo mencioné porque la persona que pregunta parece preocupada por los libros "largos".
Radu GRIGore
@Radu: Ciertamente, TAPL es lento, pero es una buena introducción. El libro de Harper que mencionó en sus enlaces va mucho más rápido y cubre mucho más terreno, aunque aún no se ha completado.
Dave Clarke
44
Tome esa revisión de Amazon del libro de Winskel con una pizca de sal. A menudo se usa como texto recomendado en cursos de semántica de pregrado y posiblemente atrae a estudiantes descontentos. Leí el libro y encontré los capítulos introductorios más que suficientes. Su notación también parecía ser completamente estándar.
Dominic Mulligan el