Эквивалентность заикания - Stuttering equivalence

В теоретическая информатика, эквивалентность заикания,^[1] отношение, записанное как

Пути ${\displaystyle \pi }$ и ${\displaystyle \pi '}$ эквивалентны заиканию.

${\displaystyle \pi \sim _{st}\pi '}$,

можно рассматривать как разделение пути ${\displaystyle \pi }$ и ${\displaystyle \pi '}$ в блоки, так что состояния в ${\displaystyle k^{\mathrm {th} }}$ блоки одного пути помечены (${\displaystyle L(\cdot )}$) так же, как и в ${\displaystyle k^{\mathrm {th} }}$ блок другого пути. Соответствующие блоки могут иметь разную длину.

Формально это можно выразить как два бесконечных пути ${\displaystyle \pi =s_{0},s_{1},\ldots }$ и ${\displaystyle \pi '=r_{0},r_{1},\ldots }$ которые эквивалентны заиканию (${\displaystyle \pi \sim _{st}\pi '}$), если есть две бесконечные последовательности целых чисел ${\displaystyle 0=i_{0}<i_{1}<i_{2}<\ldots }$ и ${\displaystyle 0=j_{0}<j_{1}<j_{2}<\ldots }$ так что для каждого блока ${\displaystyle k\geq 0}$ держит ${\displaystyle L(s_{i_{k}})=L(s_{i_{k}+1})=\ldots =L(s_{i_{k+1}-1})=L(r_{j_{k}})=L(r_{j_{k}+1})=\ldots =L(r_{j_{k+1}-1})}$.

Эквивалентность заикания - это не то же самое, что бисимуляция, поскольку бисимуляция не может уловить семантику оператора «в конечном итоге» (или «наконец»), найденного в линейный временной /логика дерева вычислений (логика времени ветвления) (модальная логика ). Так называемый бистимуляция ветвления должен использоваться.^{[нужна цитата ]}

Рекомендации

1. Грут, Ян Фризо; Ваандрагер, Фриц В. (1990). «Эффективный алгоритм для двойного моделирования ветвления и эквивалентности заикания». В Патерсоне, Майкл С. (ред.). Материалы 17-го Международного коллоквиума по автоматам, языкам и программированию. Конспект лекций по информатике. 443. Springer-Verlag. стр.626–638. Дои:10.1007 / BFb0032063. ISBN  0-387-52826-1.