«Аппликативный порядок» и «Нормальный порядок» в лямбда-исчислении

14

Аппликативный порядок: всегда полностью оценивайте аргументы функции перед оценкой самой функции, например:

(λx.x2(λx.(x+1)  2)))(λx.x2(2+1)) (λx.x2(3)) 32  9

Нормальный порядок: выражение будет уменьшено извне, как -

(λx.x2(λx.(x+1) 2)) (λx.(x+1)   2)2 (2+1)2 32  9

Пусть M=(λx.y (λx.(x  x) λx.(x  x)))

Почему при аппликативном порядке бесконечный цикл, а при нормальном порядке M y ?M
My

URL87
источник
1
Вы пытались оценить их вообще? Это первый или второй случай, который неясен?
Каролис Юоделе
@ KarolisJuodelė: 1-й
URL87
1
Не следует ли писать лямбда-выражения в скобках, чтобы отметить конец первого лямбда-выражения и начало аргумента, например:Let M = (λx.y) ((λx.(x x)) λx.(x x))
mattgately

Ответы:

7

- бесконечный цикл, потому что λ x . ( x x ) λ x . ( x x ) λ x . ( x x ) λ x . ( x x ) Обратите внимание, что λ x . ( х(λИкс,Y (λИкс,(Икс  Икс) λИкс,(Икс  Икс)))

λИкс,(Икс  Икс) λИкс,(Икс  Икс)λИкс,(Икс  Икс) λИкс,(Икс  Икс)
просто пишет свой аргумент дважды.λИкс,(Икс  Икс)
Каролис Юоделе
источник
15

(КYΩ)КYλИкс,YYΩзнак равно(λИкс,(ИксИкс)λИкс,(ИксИкс))ΩΩΩ, (Удостоверьтесь, чтобы это было на бумаге хотя бы раз в жизни.)

Аппликативное уменьшение порядка должно привести аргумент функции к нормальной форме, прежде чем он сможет оценить переопределение верхнего уровня. Поскольку аргументΩне имеет нормальной формы, аппликативное уменьшение порядка зацикливается бесконечно. В целом, на любой срокM, MΩMΩи это сокращение, выбранное стратегией аппликативного заказа.

Снижение нормального порядка начинается с уменьшения переопределения верхнего уровня (потому что функция КYуже в нормальной форме). посколькуКY игнорирует его аргумент, (КYΩ)Yв один шаг. В более общем смысле,КYNY на любой срок Nи это сокращение, выбранное обычной стратегией заказа.

Этот случай иллюстрирует более общее явление: аппликативное уменьшение порядка только когда-либо находит нормальную форму, если термин сильно нормализует, тогда как нормальное уменьшение порядка всегда находит нормальную форму, если он есть. Это происходит потому, что аппликативный порядок всегда сначала полностью оценивает аргументы, и поэтому упускает возможность для аргумента оказаться неиспользованным; тогда как нормальный порядок оценивает аргументы как можно позже и поэтому всегда побеждает, если аргумент оказывается неиспользованным.

(Обратной стороной является то, что на практике аппликативный порядок имеет тенденцию быть более быстрым, поскольку аргумент редко используется, а аргумент используется несколько раз, а при аппликативном порядке аргумент оценивается только один раз. Порядок оценивает аргумент так часто, как он используется, будь то 0, 1 или много раз.)

Жиль "ТАК - перестань быть злым"
источник
Я полагаю, вы сделали опечатку в пункте 3. КYNN должно быть Y, право? Независимо от +1.
Каролис Юоделе