deniok: (Default)
deniok ([personal profile] deniok) wrote2017-09-24 02:45 pm

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

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

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

juan_gandhi: (Default)

[personal profile] juan_gandhi 2017-09-24 03:55 pm (UTC)(link)
О блин. Надо думать...
juan_gandhi: (Default)

[personal profile] juan_gandhi 2017-09-24 09:08 pm (UTC)(link)
А, вот и ответ. Я что-то такое задумывал было, но...

[personal profile] codedot 2017-09-24 06:44 pm (UTC)(link)
M M M, где M = λxy.y x x.

[personal profile] codedot 2019-04-23 05:02 am (UTC)(link)
Кстати, а есть ли какое-то специальное название для бинарного отношения, которое одновременно является отношением порядка и обладает свойством Черча-Россера?

Вопрос по ЛИ

[personal profile] andrey83 2018-02-23 11:38 pm (UTC)(link)
Здравствуйте, Денис.

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

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

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: Вопрос по ЛИ

[personal profile] andrey83 2018-02-24 03:16 pm (UTC)(link)
спасибо большое!