1) Какова связь между статической типизацией и формальными грамматиками, если таковые имеются?
2) В частности, возможно ли, чтобы линейный ограниченный автомат проверял, хорошо ли, например, написана программа на C ++ или SML? Вложенный стек?
3) Есть ли естественный способ выразить статические правила типизации в терминах формальной грамматики?
Для линейных ограниченных автоматов невозможно проверить, являются ли программы на C ++, и LBA вряд ли сможет проверить, хорошо ли типизированы программы на SML. C ++ имеет систему типов, полную по Тьюрингу, поскольку вы можете кодировать произвольные программы в качестве шаблонных метапрограмм.
SML интереснее. У него есть проверяемая проверка типов, но проблема является EXPTIME-полной. Следовательно, маловероятно, что LBA сможет это проверить, если только не произойдет очень неожиданный коллапс в иерархии сложности. Причина этого заключается в том, что SML требует вывода типов, и существуют семейства программ, размер которых растет гораздо быстрее, чем размер программы. В качестве примера рассмотрим следующую программу:
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 *)
Для систем более простых типов, таких как C или Pascal, я считаю, что LBA может проверить это.
В первые дни исследования языков программирования люди иногда использовали грамматики Ван Вингардена (или двухуровневые грамматики) для определения систем типов для языков программирования. Я считаю, что Алгол 68 был указан таким образом. Тем не менее, мне сказали, что от этой техники отказались по существу по прагматическим причинам: людям оказалось довольно сложно писать грамматики, в которых указывалось, что, по их мнению, они указывали! (Как правило, написанные грамматики генерируют языки большего размера, чем предполагалось.)
В наши дни люди используют правила схематического вывода для определения систем типов, что по сути является способом указания предикатов в качестве наименее фиксированной точки совокупности предложений Хорна. Удовлетворенность для теорий Рога первого порядка вообще неразрешима, поэтому, если вы хотите охватить все, что делают теоретики типов, то любой выбранный вами грамматический формализм будет сильнее, чем это действительно удобно.
Я знаю, что была проделана определенная работа по использованию грамматик атрибутов для реализации систем типов. Они утверждают, что для этого выбора есть некоторые преимущества разработки программного обеспечения: а именно, грамматики атрибутов очень строго управляют потоком информации, и мне сказали, что это облегчает понимание программы.
Насколько я знаю, правильность типов, как правило, неразрешима для интересных случаев, поэтому ясно, что формальные грамматики не могут охватить каждую систему типов, о которой вы только можете подумать.
Я знаю, что основные генераторы компилятора допускают произвольные предикаты для правил, которые препятствуют выполнению правила, если предикат не оценивается true, например
{ type(e1) == type(e2) } (expression e1) '+' (expression e2). Эта концепция может быть легко формализована; соответствующие ограничения на разрешенные предикаты могут привести к разрешимости LBA.
Выбор таких предикатов, по крайней мере, труден в отношении времени выполнения, поэтому я думаю, что люди склонны выполнять итеративный анализ, собирая информацию на этапе , чтобы проверить выполнимость на этапе . Например, вы можете создать таблицу имен за один проход, а затем проверить, что все используемые переменные (видимо) объявлены во втором запуске.