B
Это просто то, чем занимаются логики-математики
Size: a a a
2021 April 28
B
Вот открываешь ты статью по темпоральной логике (которая возникла из tense logic логика-философа Прайора)
B
А там ничего специально интересного ни для философов, ни для компьютерщиков, ни для кого-то ещё, кроме типичных математиков
AG
что касается связи этого богатства с компиляторами, то мой тезис в том что теория доказательств связана с ними напрямую (грубо говоря, это формальная теория IR - все эти SSA и ANF это предмет её изучения), а теория моделей через статический анализ
B
Там просто человек исследует темпоральную логику, исходя из того, что интересно математикам, как если бы это была очередная математическая теория
B
Вот это как раз — то, что делает Рогозин в отрыве от компьютерных логик
o⭐
редкий пример апофатического определения
o⭐
как же. для компьютерщиков есть TLA+, темпоральная тоже
B
Забыл, ещё металогику добавить
B
Ты не понял
B
Вот берёшь ты некоторую статью
B
по темпоральной логике
B
А там не TLA+
B
Не tense в лингвистике
B
Не что-то ещё
DV
Хмм .. не уверен, что понял аббревиатуры правильно, но вот связь теории моделей и статического анализа - не понятно мне это
DV
IR - intermediate representation?
AG
классический пример модели - автомат
DV
Ssa - single static assignment?
B
А просто вот кто-то взял и исследует либо некоторую готовую темпоральную логику, как будто это что-то в духе теории полей или функционального анализа, либо только что придуманную темпоральную логику, которая создана чисто из-за математического интереса