Очень интересно и многообещающе выглядит, но возникает множество вопросов:
> ...into which simpler axiomatic theories... are submerged
Не очень понял что здесь имеется в виду под submerged. Любой результат из simpler axiomatic применим к теории множеств? Любой результат из теории множеств применим к simpler axiomatic? Что-то другое?
> classical first order logic is the default
Для кого она default? Для теории множеств или для simpler axiomatic выше?
> elegant and well-understood model theory
Тут я как-то совсем потерялся - model theory это что такое и как оно соотносится с axiomatic theory и algebraic theory?
> both single-sorted or multisorted
Эта сортировка связана с well-ordering? Или это вообще про другое?
Любопытно будет почитать продолжение. Давно хотелось лучше во всех эти теориях разобраться. Тут вот и алгебраические, и аксиоматические, и теории с зависимыми типами упоминаются - интересно понять что из этого друг с другом связано и как.
теория моделей это такой раздел матлогики, про связь математических объектов с логическими сигнатурами описываемые в посте алгебраические теории это один из её основных инструментов
А что это будет, обзор? Вы пробовали бредокодогенерацию для llvm? Если пробовали, подскажите, что почитать. Я нашёл свежую статью про кодогенерацию на Хаскеле, но это всё тот же "Калейдоскоп", что они давно в пример приводят.
Comments 6
Reply
Reply
> ...into which simpler axiomatic theories... are submerged
Не очень понял что здесь имеется в виду под submerged. Любой результат из simpler axiomatic применим к теории множеств? Любой результат из теории множеств применим к simpler axiomatic? Что-то другое?
> classical first order logic is the default
Для кого она default? Для теории множеств или для simpler axiomatic выше?
> elegant and well-understood model theory
Тут я как-то совсем потерялся - model theory это что такое и как оно соотносится с axiomatic theory и algebraic theory?
> both single-sorted or multisorted
Эта сортировка связана с well-ordering? Или это вообще про другое?
Любопытно будет почитать продолжение. Давно хотелось лучше во всех эти теориях разобраться. Тут вот и алгебраические, и аксиоматические, и теории с зависимыми типами упоминаются - интересно понять что из этого друг с другом связано и как.
Reply
описываемые в посте алгебраические теории это один из её основных инструментов
Reply
Как Вы думаете, должны ли в этом языке быть такие термины, как
1) Процесс
2) Результат процесса
?
Что произойдёт, если их ввести?
Reply
Вы пробовали бредокодогенерацию для llvm? Если пробовали, подскажите, что почитать. Я нашёл свежую статью про кодогенерацию на Хаскеле, но это всё тот же "Калейдоскоп", что они давно в пример приводят.
Reply
Leave a comment