Как применить только одну бета-редукцию к λy. (Λx.λy.yx) yz?

Я не понимаю, как получить правильный ответ, который равен λy. (Λw.wy) z

Переименование разрешено только в случае необходимости, и из ответа очевидно, что использовалось переименование.


beta parsing rename reduction lambda-calculus
person Sajid Sarkar    schedule 18.11.2020    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Давайте сначала добавим скобки, чтобы сделать структуру более очевидной, потому что, возможно, вы запутались именно в этом:

λy.(λx.λy.yx)yz = λy.(((λx.λy.(yx))y)z)

На внешнем уровне ничего не поделаешь. Но мы можем сделать бета-сокращение внутри λy, но сначала нам нужно переименовать альфа, чтобы избежать захвата y:

    (λx.λy.(yx))y
--> (λx.λw.(wx))y   (alpha renaming y to w)
--> λw.wy           (beta)

Теперь поместим это в общий контекст:

    λy.(λx.λy.yx)yz
--> λy.(λx.λw.(wx))yz   (alpha renaming y to w)
--> λy.(λw.wy)z         (beta)
person Mo B.    schedule 18.11.2020
comment
Спасибо! Следовательно, ключ состоит в том, чтобы назначить круглые скобки, следуя правилам Left-Left & λx. (Насколько это возможно), до начала бета-редукции. - person Sajid Sarkar; 19.11.2020