Lambda Calculus Сокращение/оценочные выражения

Question

Я читал эти notes на исчислении лямбда, и у меня возникают некоторые проблемы с уменьшением/оценкой одного из выражений в начале.

В частности, функция (λf.λx.f (f (x))) (λy.y^2) (5).

Как именно я начинаю это? Он говорит, что ответ получается 625. Моя математическая интуиция говорит, что мы продолжаем так: (λf.λx.f (f (x))) (5 ​​^ 2), и он сказал ранее, что f (x) является карта

х | -> х^2

так е (е (х)) является композицией, которая будет ФОФ = (е)^2 = х^4

таким образом дальнейшее сокращение нашей лямбды выражение мы получаем

(λf.λx.x^4)) (5 ​​^ 2)

Но тогда мы бы подключить 25 в х^4, что дает нам 2 5 * 25 * 25 * 25 = 390,625.

(λf. (390.625))

тогда, когда мы здесь, я совершенно не знаю, что представляет это выражение?

Какую часть исчисления лямбда я неправильно понял? Является ли способ сокращения выражений правильным?

Answer 1

Я ничего не знаю об исчислении лямбда, так что не стесняйтесь меня забвять, если я ошибаюсь :) Плюс моя терминология отключится, поэтому, надеюсь, кто-то испытает ответ на вопрос. Вероятно, это должно быть отправлено в math.stackexchange.com в любом случае.

был дан ранее в качестве примера и не должен был перенести на последующие проблемы.

Прежде всего, похоже, что вы не скопировали это выражение правильно. В соответствии с PDF, это:

Теперь порядок вопросов операций (скобки первого!).

Мы начинаем с:

Мы предоставляем термин лямбда на левой с аргументом . Это означает, что f заменяется квадратичной функцией.

Так что теперь мы имеем:

Edit:

Причина приводится в качестве аргумента является то, что мы могли бы написать целое выражение, как:

Если мы посмотрим на первую часть, это легче увидеть, что относится к первому аргументу:

Answer 2

Correct нормального порядка (крайний левый первый) бета-редукции к нормальной форме:

(λ f. (λ x. f (f x))) (λ y. y^2) 5 
= (λ x. (λ y. y^2) ((λ y. y^2) x)) 5 
= (λ x. ((λ y. y^2) x)^2) 5 
= (λ x. (x^2)^2) 5 
= (5^2)^2 
= 25^2 
= 625 

Численные примитивы, такие как 2, 5 и ^, хотя encodable, не являются частью грамматики. Интуитивные обычные правила алгебраической редукции, такие как умножение экспоненты, не применяются; только бета- и, возможно, эта-сокращение.