Опровержение гипотезы об одношаговости стратегии Gyorgy Revesz

[codedot]

Наивная попытка показать, что функция revesz(), определяемая ниже на языке Python, являющаяся рекурсивной одношаговой стратегией, является эквивалентной рекурсивной многошаговой стратегии Gyorgy Revesz, введенной в его статье "Axioms for the Theory of Lambda-Conversion", провалилась. Стратегия Gyorgy Revesz действительно должна использовать больше информации, чем само вычисляемое выражение. Об этом, впрочем, говорится в "J. Klop's Ustica notes", но, к сожалению, без доказательств.

После написания небольшой библиотеки функций на языке 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$

Для библиотеки принято соглашение об именах, похожее на введенное в монографии Барендрегта: все свободные и связанные переменные должны называться по-разному. Стоит отметить, что во многих машинах, основанных на идее "Graph Reduction", это соглашение выполняется автоматически: вместо имен используются адреса блоков в памяти, и разные переменные представляются разными же блоками.

Переменные представляются строками - именами этих переменных. Абстракции - кортежами вида (':', VAR, BODY), где VAR - переменная, связанная с данной абстракцией, а BODY - тело функции. Наконец, аппликации представляются кортежами вида ('@', OP, ARG), где OP - левая часть аппликации, а ARG - правая ее часть. Также определены несколько элементарных функций:

• isabstr(term), isappl(term), isvar(term) и isredex(term) - является ли term абстракцией, аппликацией, переменной или бата-редексом, соответственно;
• op(term), arg(term), var(term) и body(term) - левая часть аппликации term, правая часть аппликации term, переменная, связанная с абстракцией term, и тело функции term, соответственно;
• redexbody(term) и redexvar(term) - тело функции в редексе и переменная, связанная с абстракцией в редексе, соответственно;
• betamu(term) - один шаг редукции, определяемой в "Micro Lambda Calculus".

С помощью базовых функций, перечисленных выше, можно определить revesz(term) следующим образом:

def ltrace(term):
	if isredex(term):
		return betamu(term)
	elif isabstr(term) and ltrace(body(term)):
		return (':',
				var(term),
				ltrace(body(term)))
	else:
		return None

def reduce(term):
	if ltrace(redexbody(term)):
		return ('@',
				(':',
					redexvar(term),
					ltrace(redexbody(term))),
				arg(term))
	else:
		return betamu(term)

def revesz(term):
	if isredex(term):
		return reduce(term)
	elif isabstr(term):
		if revesz(body(term)):
			return (':',
					var(term),
					revesz(body(term)))
		else:
			return None
	elif isappl(term):
		if revesz(op(term)):
			return ('@',
					revesz(op(term)),
					arg(term))
		elif revesz(arg(term)):
			return ('@',
					op(term),
					revesz(arg(term)))
		else:
			return None
	else:
		return None

Таким образом, пока вопрос о том, существует ли одношаговая стратегия для "Micro Lambda Calculus", остается открытым.