Entry tags:
Порядочность бета-редукции
(1) Является ли отношение многошаговой бета-редукции на термах бестипового лямбда-исчисления отношением порядка? Докажите или приведите контрпример.
(2) Верен ли ваш ответ для просто типизированной лямбды?
(1) Является ли отношение многошаговой бета-редукции на термах бестипового лямбда-исчисления отношением порядка? Докажите или приведите контрпример.
(2) Верен ли ваш ответ для просто типизированной лямбды?
no subject
no subject
no subject
no subject
no subject
no subject
Вопрос по ЛИ
Смотрю ваши лекции по ЛИ на лекториуме.
Во-первых хочется сказать большое спасибо за прекрасные лекции!
Возник вопрос, если найдётся минута.
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: Вопрос по ЛИ
Конструкция x M_1 ... M_k называется головной нормальной формой. Это не обычная нормальная форма (в Mi могут быть редексы), но тем не менее в некотором смысле содержательный результат вычислений. При дальнейших вычислениях структура терма в виде переменной x примененной к k аргументам уже не изменится. Более того, редукция в одном Mi совершенно никак не зависит от и не влияет на другой Mj.
Re: Вопрос по ЛИ