CEK і нумерали Чорча

[dmytrish]

CEK-машини взагалі уміють рахувати нумерали Чорча?

Прості приклади типу (λx.λy.x) 1 2 обчислюються, але коли я намагаюсь обчислити succ one, де succ = λn.λf.λx.f (n f x), one = λf.λx.f x, і мій доморощенний CEK-інтерпретатор, і я вручну упираємось у стан < clos(λf.λx.f (n f x), E1) | E1 | nil > де E1 = { n -> clos(λf.λx.f x, {}) }, хоча в ідеалі

Comments

[beroal]

Якщо не помиляюся, SECD реалізує call-by-value-редукцію. Call-by-value-редукція не чіпає редекси під абстракцією. Якби ви в λf.λx.f (n f x) замість n підставили λf.λx.f x, то отримали б редекс під абстракцією.

λf.λx.f ((λf.λx.f x) f x)

[dmytrish]

Да, логічно, дякую. Тобто ключова проблема тут call-by-value.

P.S. Машина тут CEK, але це той самий call-by-value.

[beroal]

Я підозрюю, що машина Кривіна має ту саму проблему.