стратегии бета-сокращения в Haskell

Question

Я впервые изучаю функциональное программирование. Я понимаю, как работает простое бета-сокращение.

, например:

(\x->2*x)5

означает, что вы заменяете x на 5.

2*5=10

Однако другие примеры приводят в замешательство me

(\f->f(f 0))(\x->x+1)

Мы узнали о некоторых стратегиях оценки, нормальной форме головы и слабых нормальных формах головы.

из моих заметок, я понимаю, что нормальная форма головы означает отсутствие выражения redex, в то время как слабая Нормальная форма головы означает, что есть лямбда-абстракция.

Это не имеет никакого смысла для меня. Относится ли один из двух к этому последнему примеру? Если это так, что будет примером другой стратегии?

Answer 1

Термин

(\f -> f (f 0)) (\x -> x+1)

не относится ни к нормальной форме головы, ни к нормальной форме слабой головы. Этот термин является применением лямбды (в частности, \f -> f (f 0)) к термину (в частности, \x -> x+1), и поэтому:

1. Существует переопределение. Напомним, что переопределение определяется как применение лямбда к термину. Поскольку в выражении есть выражение где-то - и, в частности, на самом верхнем уровне, в данном случае - это не в обычной форме.
2. Верхний уровень этот термин является приложением, а не лямбда-выражением, поэтому речь идет не о нормальной форме слабой головы.

Ни «нормальная форма головы», ни «нормальная форма слабой головы» не является стратегией оценки. Формы являются прилагательными, которые описывают термины; Стратегии оценки, как правило, представляют собой глаголы, которые описывают, как заменить один термин на другой термин.