Взять JavaScript: система типов есть, но динамическая. И типы не назначены до выполнения.
Не-а, нету там системы типов. Вся соль типов, что они назначаются до выполнения, так что нам не надо выполнять программу, чтобы узнать, будут ли в ней ошибки выполнения. Ну вот смотрите, простенький язык:
t ::= TRUE | FALSE | IF t THEN t ELSE t | 0 | SUCC t | PRED t | ISZERO t
v ::= TRUE | FALSE | nv
nv ::= 0 | SUCC nvА вот его семантика:
(Оффтоп)
Мда, что-то \text{} уродливо работает...
Правило E-PredZero можете при желании выбросить. Так вот, как вы видите,
succ false или
if 0 then ... else ... являются несводимыми выражениями — к ним неприменимо ни одно правило вычисления, но эти выражения не являются значениями (продукциями символа
v), они "застряли". Это — обычный способ выражения семантики ошибки времени выполнения. Но этот язык является нетипизированным. В нем нету системы типов, просто не все выражения имеют нормальную форму.