Разница между бета-снижением и одноступенчатым бета-снижением?

Я просмотрел множество онлайн-источников по лямбда-исчислению в поисках разницы между бета-сокращением и одношаговым бета-сокращением. Но все, что я знаю до сих пор, это то, что бета-редукция определяется как:

(/x.L)M --> {M/x}L

и следующее определение 1-шагового сокращения бета-версии: введите здесь описание изображения

Может кто-нибудь, пожалуйста, проясните разницу между этими двумя вещами на каком-нибудь примере. Мне они кажутся эквивалентными. Кроме того, существует n-ступенчатое бета-снижение, которое я понял как индуктивно применяемое 1-ступенчатое бета-сокращение. Но поскольку разница между бета-снижением и одноэтапным бета-снижением не ясна, я чувствую себя беспомощным. Заранее спасибо.


person Ankit Shubham    schedule 13.03.2016    source источник


Ответы (1)


Я думаю, что бета-редукция может обозначать как одноступенчатую, так и многоступенчатую бета-редукции.

Я могу сказать, что бета-редукция может дать /z.a из (/x./y./z.x) a b, но я не могу сказать, что бета-редукция за один шаг может сделать это.

В остальном то, что вы сказали, верно.

person ZakC    schedule 14.03.2016