Уменьшить лямбда-выражения в WHNF
Я должен сократить следующее лямбда-выражение в WHNF, но я не совсем уверен, как это сделать:
(λx y. x 3) (+ 4) (+ 6 7)
Итак, как мне это сделать? Сокращение числа обращений по имени?
Это выражение (другой пример) (λz x. (λx. x) z) x в WHNF еще нет?
1 ответ
WHNF (Weak Head Normal Form) означает, что у вас либо есть значение (например, целое число), либо выражение имеет вид (λx . e(x)) где e(x) это выражение, которое может содержать ссылки на xТаким образом, в основном у вас есть, что результат является функцией.
В вашем случае выражение, которое вы имеете, содержит несколько приложений, которые нужно уменьшить:
(λx . λy. x 3) (+ 4) (+ 6 7) = (λy . (+ 4) 3) (+ 6 7)
= (+ 4) 3
= 7
Обратите внимание, что в этом случае y не появляется в теле функции, и, следовательно, + 6 7 "исчезает" во время сокращения.
Нет, (λz x. (λx. x) z) x не в WHNF, потому что "главный оператор" по-прежнему является приложением. Обратите внимание, что сокращение в этом случае немного сложно, потому что у вас есть свободная переменная x снаружи и λ также связывает x, Однако мы можем сначала сделать некоторое переименование: (λz k. (λt. t) z) x а теперь выполним сокращение: (λk. (λt. t) x) и это сейчас в WHNF. Обратите внимание, что мы не сокращаем приложение (λt. t) x потому что это внутри λ,
чтобы проверить, находится ли выражение в WHNF, вы должны рассматривать его как синтаксическое дерево. Давайте рассмотрим два примера выше, и давайте обозначим приложение явно $, Помните, что приложение f x y эквивалентно (f x) y,
В первом случае выражение было:
|
+-------------$-----------+
| |
+---- $ ---- +---(+)---+
| | | |
λx λt 6 7
| |
λy +-(+)-+
| | |
+---$---+ t 4
| |
x 3
Как вы можете видеть, корень дерева $Итак, мы должны выполнить заявку. Чтобы сделать это, мы должны сначала уменьшить левую сторону, которая снова $ так что это должно быть уменьшено в первую очередь, получив:
|
+-------------$-----------+
| |
| +---(+)---+
| | |
| 6 7
|
λy
|
+---$---+
| |
λt 3
|
+-(+)-+
| |
t 4
Теперь слева у нас есть λ так что мы можем уменьшить внешнее применение $:
|
+---$---+
| |
λt 3
|
+-(+)-+
| |
t 4
И теперь корень все еще $ поэтому мы должны уменьшить это тоже:
|
+-(+)-+
| |
3 4
Корень +Итак, мы снова уменьшаем получение:
|
7
И теперь мы закончили.
Во втором случае мы имеем выражение (λz . λk. ((λt. t) z)) x который становится деревом:
|
+-------$-----------------+
| |
λz x
|
λk
|
+----$----+
| |
λt z
|
t
Опять корень $ поэтому мы должны уменьшить его:
λk
|
+----$----+
| |
λt x
|
t
Теперь у нас есть дерево, корень которого λ, и это означает, что выражение находится в WHNF, поэтому мы остановимся.