1) ¿Cuál es, si la hay, la relación entre la escritura estática y las gramáticas formales?
2) En particular, ¿sería posible que un autómata lineal limitado verificara si, por ejemplo, un programa C ++ o SML estaba bien escrito? ¿Un autómata apilado anidado?
3) ¿Existe una forma natural de expresar reglas de escritura estática en términos gramaticales formales?
No es posible que los autómatas lineales limitados verifiquen si los programas C ++, y es poco probable que LBA verifique si los programas SML están bien escritos. C ++ tiene un sistema de tipo Turing-complete, ya que puede codificar programas arbitrarios como metaprogramas de plantilla.
SML es más interesante. Tiene una verificación de tipo decidible, pero el problema es EXPTIME-complete. Por lo tanto, es poco probable que un LBA pueda verificarlo, a menos que haya un colapso muy sorprendente en la jerarquía de complejidad. La razón de esto es que SML requiere inferencia de tipos, y hay familias de programas cuyo tamaño crece mucho más rápido que el tamaño del programa. Como ejemplo, considere el siguiente programa:
fun delta x = (x, x) (* this has type 'a -> ('a * 'a), so its return value
has a type double the size of its argument *)
fun f1 x = delta (delta x) (* Now we use functions to iterate this process *)
fun f2 x = f1 (f1 x)
fun f3 x = f2 (f2 x) (* This function has a HUGE type *)
Para sistemas de tipo más simple, como C o Pascal, creo que es posible que un LBA lo verifique.
En los primeros días de la investigación de lenguajes de programación, las personas a veces usaban gramáticas de van Wingaarden (también conocidas como gramáticas de dos niveles) para especificar sistemas de tipos para lenguajes de programación. Creo que Algol 68 se especificó de esta manera. Sin embargo, me dijeron que esta técnica fue abandonada por razones esencialmente pragmáticas: ¡resultó ser bastante difícil para las personas escribir gramáticas que especificaban lo que pensaban que estaban especificando! (Por lo general, las gramáticas que la gente escribía generaban idiomas más grandes de lo que pretendían).
En estos días, las personas usan reglas de inferencia esquemáticas para especificar sistemas de tipos, que es esencialmente una forma de especificar predicados como el punto menos fijo de una colección de cláusulas Horn. La satisfacción de las teorías de Horn de primer orden es indecidible en general, por lo que si desea capturar todo lo que hacen los teóricos del tipo, entonces cualquier formalismo gramatical que elija será más fuerte de lo que realmente es conveniente.
Sé que se ha trabajado en el uso de gramáticas de atributos para implementar sistemas de tipos. Afirman que hay algunos beneficios de ingeniería de software para esta elección: a saber, las gramáticas de atributos controlan el flujo de información de manera muy estricta, y me han dicho que esto facilita la comprensión del programa.
Hasta donde sé, la corrección de tipo tiende a ser indecidible para casos interesantes, por lo que las gramáticas formales claramente no pueden capturar todos los sistemas de tipos que se te ocurran.
Sé que los principales generadores de compiladores permiten predicados arbitrarios para reglas que evitan que se ejecute una regla si el predicado no evalúa true, por ejemplo
{ type(e1) == type(e2) } (expression e1) '+' (expression e2). Este concepto se puede formalizar fácilmente; las restricciones apropiadas sobre los predicados permitidos pueden generar la capacidad de decisión de los LBA