Порядочность бета-редукции

[deniok]

(1) Является ли отношение многошаговой бета-редукции на термах бестипового лямбда-исчисления отношением порядка? Докажите или приведите контрпример.

(2) Верен ли ваш ответ для просто типизированной лямбды?

Comments

[codedot]

Кстати, а есть ли какое-то специальное название для бинарного отношения, которое одновременно является отношением порядка и обладает свойством Черча-Россера?

[deniok]

Я бы сказал конфлюентный порядок, это достаточно коротко. (Мы где-то договорились говорить по-русски соборный вместо конфлюентный, но это была шутка). Хотя "соборный порядок" - это звучит!