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

[deniok]

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

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

Comments

[juan_gandhi]

О блин. Надо думать...

[codedot]

См. также упр. 3.5.2 (iii).

[juan_gandhi]

А, вот и ответ. Я что-то такое задумывал было, но...

[codedot]

M M M, где M = λxy.y x x.

[codedot]

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

[deniok]

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

Вопрос по ЛИ

[andrey83]

Здравствуйте, Денис.

Смотрю ваши лекции по ЛИ на лекториуме.
Во-первых хочется сказать большое спасибо за прекрасные лекции!

Возник вопрос, если найдётся минута.

https://www.lektorium.tv/sites/lektorium.tv/files/additional_files/20110313_systems_of_typed_lambda_calculi_moskvin_lecture06.pdf

стр 14, лемма 1, случай 1. доказываем для альфа (базовый случай индукции).

Написано "тривиально". Но я не понимаю этого момента. Т.е. доказатльество в целом понятно. Но вот этот базовый случай я не понимаю.

У Барендрегта LCWT, Oxford University Press, 1993
стр 62, лемма 4.3.3, случай 1 SN принадлежит SAT. точно то же в док-ве, только там не сказано что дан тип альфа. Просто R1,...,Rn принадлежат SN из чего тривиально следует что xR1..Rn тоже принадлежит SN.

Очевидно, ход мысли в обоих случаях один и тот же. Но второй случай "незамутнён" типами. Однако, как показать что xR1..Rn принадлежит SN я совсем не понимаю. Более того, (пример из лекции, + икс спереди) x(\у.уу)(\у.уу) явно не принадлежит SN хотя x и \у.уу принадлежат SN однозначно.

Когда/если будет время, прокомментируйте, пожалуйста, если найдёте возможным.

Re: Вопрос по ЛИ

[deniok]

Ваш контрпример x(\у.уу)(\у.уу) не работает, потому что аппликация ассоциативна влево, и читается он так (x(\у.уу))(\у.уу).

Конструкция x M_1 ... M_k называется головной нормальной формой. Это не обычная нормальная форма (в Mi могут быть редексы), но тем не менее в некотором смысле содержательный результат вычислений. При дальнейших вычислениях структура терма в виде переменной x примененной к k аргументам уже не изменится. Более того, редукция в одном Mi совершенно никак не зависит от и не влияет на другой Mj.

Re: Вопрос по ЛИ

[andrey83]

спасибо большое!