Приоритет оператора лямбда-исчисления и стратегии сокращения

1.
В лямбда-исчислении приложения имеют более высокий приоритет, чем абстракции. Теперь в этом примере автор показывает два сокращения в нормальный и аппликативный порядок. Первый:

(λx.x^2 (λx.(x+1) 2))) → (λx.x^2 (2+1)) → (λx.x^2 (3)) → 3^2 → 9

Моя проблема заключается в 1-м и 3-м шаге. Почему он может так уменьшить

(λx.x^2 (3)) → 3^2

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

λx.x^2 (3) = λx.(x^2 (3))

и, следовательно, никакое сокращение не должно быть возможным? То, как он интерпретирует этот термин,

λx.x^2 (3) = (λx.x^2) (3)

что неверно.

2.

Afaik это определения 4 стратегий сокращения.

Normal Order:       Leftmost outermost redex reduced first
Applicative Order:  Leftmost innermost redex reduced first
Call by value:      Only outermost redex reduced                Reduction only if right-hand side has been reduced to a value (= variable or abstraction)
Call by name:       Leftmost outermost redex reduced first      No reductions inside abstractions

Согласно это самое внутреннее и самое внешнее относится только к абстракциям. Относится ли крайний левый (и крайний правый) только к приложениям?

3.

Так является ли это правильным рекурсивным алгоритмом аппликативного снижения порядка (в псевдокоде)?

evaluate(t : Term) {
    if (t is Abstraction) {
        evaluate(t.inside)
    } else if (t is Application) {
        evaluate(t.first)
        if (t.first is Abstraction) {
            t.first.apply(t.second)
        }
    } else if (t is Variable) {
        do nothing
    }
}

Абстракция, приложение и переменная являются дочерними классами Term. Функция «применить» применяет заданный терм к абстракции. Структуры данных выглядят примерно так (пожалуйста, игнорируйте синтаксис отсутствующего указателя):

class Abstraction {
    var : Variable
    inside : Term
}
class Variable {
    name : String
}
class Application {
    first : Term
    second : Term
}

4. В ссылке в 1. автор приводит пример термина, который можно привести к нормальной форме с нормальным порядком, но не с аппликативным порядком, потому что в последнем случае сокращение не будет прекращено. Существует ли термин, при котором редукция завершается, но дает разные результаты для обеих стратегий? Если да, то какой пример?

Извините за длинный вопрос, не хотел создавать для этого 4 разные темы.