стр 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 однозначно.
Когда/если будет время, прокомментируйте, пожалуйста, если найдёте возможным.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Вопрос по ЛИ
Date: 2018-02-23 11:38 pm (UTC)Смотрю ваши лекции по ЛИ на лекториуме.
Во-первых хочется сказать большое спасибо за прекрасные лекции!
Возник вопрос, если найдётся минута.
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 однозначно.
Когда/если будет время, прокомментируйте, пожалуйста, если найдёте возможным.