p
Про term rewriting.
Какое это имеет отношение к типам
Size: a a a
2020 October 29
s
Так, похоже мне надо рассказывать базовый курс математической логики.
p
Ну реально, термы существуют без типов вполне спокойно
s
Ну реально, термы существуют без типов вполне спокойно
Разумеется, существуют.
p
Поэтому говорить что типы низкоуровневые это странно
MP
На словах ты Лев толстой, а по факту сколько PR сделал в растланг для победы коммунизма?
p
Обычно низкоуровневым называют то, что является основой для чего-то
p
Mag Pie
На словах ты Лев толстой, а по факту сколько PR сделал в растланг для победы коммунизма?
Фу
H
Mag Pie
На словах ты Лев толстой, а по факту сколько PR сделал в растланг для победы коммунизма?
это про кого
s
Низкоуровневый тут в довольно специфическом смысле — непосредственно выражается как переписывание термов.
MP
это про кого
Это обращение к ноосфере
H
понял
s
Конкретнее, в логике подобное переписывание зовётся sequent calculus.
p
Низкоуровневый тут в довольно специфическом смысле — непосредственно выражается как переписывание термов.
Не понял, кто выражается?
T1
Ну реально, термы существуют без типов вполне спокойно
Ну зависит от языка
p
Ну зависит от языка
Мы говорим про теорию
s
Вот у тебя есть терм, и есть sequent calculus, позволяющий выражать синтаксические доказательства.
T1
Мы говорим про теорию
Тем более
p
Тем более
Что тем более
p
Теория одна