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

[deniok]

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

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

Comments

[juan_gandhi]

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

[codedot]

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

Вопрос по ЛИ

[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 однозначно.

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