Каковы редексы в этом выражении Haskell?

Question

Я изучаю Haskell для университетского курса, и у меня есть вопрос о приводимых выражениях (редексах). Я понимаю концепцию, но у меня все еще есть некоторые вопросы, которые я не могу решить самостоятельно.

Допустим, вы хотите найти все приводимые выражения в выражении, например:

      head (map (+1) (3:repeat 3))

В этом выражении очевидным редексом будет map (+1) (3:repeat 3))потому что оно соответствует определению , поэтому Haskell «уменьшит» выражение и увеличит 3а также 4:map (+1) (repeat 3). в следующий раз будет уменьшено.

У меня есть вопрос:

Является head (map (+1) (3:repeat 3))уже редекс, до mapоценивается?

Поскольку «ввод» не соответствует конструктору списка (что и headищет), я смущен тем, является ли это все еще редексом, потому что логически он еще не может быть сокращен, но определения в Интернете, кажется, говорят, что это будет.

Answer 1

Вычисление в Haskell ленивое: оно действует по стратегии самого верхнего левого редекса (по крайней мере, концептуально): он сокращает самый левый среди самых верхних редексов.

Предположительно определяется как

      head xs = case xs of (x:_) -> x

таким образом, его применение к любому выражению действительно является редексом — выражением, нуждающимся в редукции. Что происходит в соответствии с определением ,

      head (map (+1) (3:repeat 3))
=
case (map (+1) (3:repeat 3)) of (x:_) -> x
=

(или мы могли бы сказать, что headсам по себе является самым верхним крайним левым редексом, который сводится к его определению, во-первых; и если бы мы написали выше как ((\xs -> case xs of (x:_) -> x) (map (+1) (3:repeat 3)))мы бы пришли к тому же результату, только немного более утомительно).

Основным принудительным примитивом является . Теперь ему нужно выполнить сопоставление с образцом, поэтому он должен узнать значение своего просматриваемого выражения (только в той степени, в которой совпадение с образцом становится возможным). Для этого он должен теперь работать в соответствии с определением mapчто предположительно

      map f xs = case xs of { (x:ys) -> f x : map f ys
                      ; [] -> [] }

так это становится

      case (map (+1) (3:repeat 3)) of (x:_) -> x
=
case (case (3:repeat 3) of 
         { (x:ys      ) -> (+1) x : map (+1) ys
                   ; [] -> [] } )
                             of (x:_) -> x
=

В этот момент внутреннее выражение может быть уменьшено,

      case (let { x=3 ; ys=repeat 3} in 
        (+1) x : map (+1) ys )
  of (x        : _                  ) -> x
=

а теперь внешний caseсопоставление с образцом становится возможным,

      case (let { x=3 } in 
        (+1) x               )
  of (x                             ) -> x
=
      let { x=3 } in 
        (+1) x 
=
        (+1) 3 
=
        4