У меня есть два выражения с подстановкой:Почему не может быть заменен х
(+ x 1) [x -> 2]
результат является:
(+ 2 1)
Почему x здесь может быть заменителем? Это не функция.
Второе:
(λ x. + x 1) [x -> 2]
Почему мета переменная x не может быть заменить его?
У меня есть источник, из
https://www.youtube.com/watch?v=zg0UgCg7tZQ
Время вокруг 01:07:56.
x in (λ x. + x 1) является связанная переменная. Это не существует за пределами лямбда. Если вы заменили x -> 2, вы получите (λ 2. + 2 1) - и λ 2 - это нонсенс, так как 2 не является переменной.
В (+ x 1), x является свободной переменной, которую мы можем определить. Если мы знаем, что x - 2, мы можем заменить его и получить (+ 2 1).
Также '(λ x. F (x)) = (λ y. F (y))' для 'y' свежее имя, поэтому с учетом подстановки' s' вы ожидаете иметь '(λ x. F (x)) s = (λ y. f (y)) s' тоже, что было бы неверно, если бы оно работало, как думает OP. – Bakuriu
В чем разница между бета-редукцией и замещением. Для меня, похоже, одно и то же, но это не так. –
Бета-редукция - это замена лямбда-параметра внутри тела лямбда заданным значением (которое называется «оценивать» лямбда). Например. с учетом лямбда '(λ x. + x 1)' и значения параметра '2', лямбда-тело является' (+ x 1) ', и поэтому связанное бета-редукция составляет' (+ x 1) [x - > 2] ', который производит' (+ 2 1) '. Главное, чтобы иметь в виду, что тело лямбда не такое же, как лямбда. Бета-редукция - единственный процесс, который может избавиться от «обертки» лямбда и освободить тело внутри. – Amadan
Используйте тег 'lambda-calculus', а не тег' haskell'. – Olathe