Приведение члена лямбда-исчисления к нормальной форме

Это для домашнего задания, прежде чем кто-нибудь спросит, я просто ищу руководство.

Вот первый вопросительный термин:

(λx.λy.x y)(λx.x y)
=(λx.λz.x z)(λx.x y)         α-renaming 
=(λz.(λx.x y)  z) 
=(λx.x y)

Я хотел бы убедиться, что я правильно думаю об этом. Термин справа — это значение, помещенное в параметр x, верно? Затем каждый экземпляр x заменяется термином справа. Я переименовал y, чтобы не было путаницы со свободным y и ограниченным y. Теперь я не понимаю вторую строку, начинающуюся с =. Передается ли крайний правый z в качестве параметра для переменной z? Или он передается в x? В любом случае, я думаю, что ответ один и тот же, но я хотел бы знать, какой метод правильный.

Вот второй термин вопроса

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

Из-за круглых скобок термин (λx.x) заменяется параметром x? Или у заменяется на х?

Я надеюсь это имеет смысл. Заранее благодарю за любую помощь.


computer-science lambda-calculus
person Chris    schedule 23.03.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Лямбда-исчисление состоит из контекстно-свободной грамматики

E ::= v        Variable
   |  λ v. E   Abstraction
   |  E E      Application

где v охватывает переменные вместе с правилами бета- и эта-редукции.

(λ x. B) E  ->  B   where every occurrence of x in B in substituted by E
  λ x. E x  ->  E   if x doesn't occur free in E

a бесплатно в λ b. b a, но не в λ a. λ b. b a. Выражение, к которому не применяется ни одно из двух правил редукции, находится в нормальной форме.

Сокращение крайних левых редексов имеет приоритет. Аппликативный порядок нормализует аргументы перед заменой, нормальный порядок — нет.

Правильная бета- и эта-нормализация двух выражений нормального порядка:

   (λ x. (λ y. x y)) (λ a. a b)
=  (λ x. x) (λ a. a b)            Eta-reduction
=  λ a. a b                       Beta-reduction

   ((λ x. (λ y. x y)) (λ a. a)) f
=  ((λ x. x) (λ a. a)) f
=  (λ a. a) f
=  f
person Community    schedule 23.03.2017