Наивная попытка показать, что функция revesz(), определяемая ниже на языке Python, являющаяся рекурсивной одношаговой стратегией, является эквивалентной рекурсивной многошаговой стратегии Gyorgy Revesz, введенной в его статье "Axioms for the Theory of Lambda-Conversion", провалилась. Стратегия Gyorgy Revesz действительно должна использовать больше информации, чем само вычисляемое выражение. Об этом, впрочем, говорится в "J. Klop's Ustica notes", но, к сожалению, без доказательств.
После написания небольшой библиотеки функций на языке Python попытка вычислить выражение (1 - 1) в арифметике Черча привела к зацикливанию и переполнению стека из-за рекурсивной природы комбинатора PRED:
Таким образом, пока вопрос о том, существует ли одношаговая стратегия для "Micro Lambda Calculus", остается открытым.
После написания небольшой библиотеки функций на языке Python попытка вычислить выражение (1 - 1) в арифметике Черча привела к зацикливанию и переполнению стека из-за рекурсивной природы комбинатора PRED:
alexo@codedot:~/Projects/micro$ python
Python 2.5.2 (r252:60911, Mar 12 2008, 13:39:09)
[GCC 4.2.3 (Ubuntu 4.2.3-2ubuntu4)] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from micro import *
>>> term = ('@', pred, one)
>>> normal(term)
[...]
RuntimeError: maximum recursion depth exceeded
>>>
alexo@codedot:~/Projects/micro$
Таким образом, пока вопрос о том, существует ли одношаговая стратегия для "Micro Lambda Calculus", остается открытым.