s
Как ты запишешь какое-либо утверждение о терме?
Size: a a a
2020 October 29
p
Как ты запишешь какое-либо утверждение о терме?
Есть много разных способов
p
Смотря какое утверждение ты хочешь
s
Ну в логике это какое-то отношение.
s
foo(X, ...), типа такого.p
Дык какое утверждение то
s
Ну допустим, нам интересно знать, вычисляется ли терм в примитивное значение, в функцию, в функцию, возвращающую функцию, и так далее.
p
Записываешь в виде последовательности редукций
s
Последовательность редукций это уже вычисление терма.
H
а о чем спор вообще
H
я потерял нить
p
Последовательность редукций это уже вычисление терма.
Ну и чем не нравится?
p
Ты же сам спросил про вычисление
s
Но мы ходим сначала выразить утверждение.
p
Но мы ходим сначала выразить утверждение.
Выражай в виде последовательности редукций
s
Утверждение можно записать, например, как
evaluates_to(E, lam(_)), для терма E, который вычисляется в lam(_).s
Просто отношение между E и чем-то, показывающее общий вид того, во что E вычислится.
s
Имея подобное отношение, мы можем записать утверждение для составного терма.
s
evaluates_to(app(Ex, Ey), _) :- evaluates_to(Ex, lam(_)), evaluates_to(Ey, _).