На вопрос о корректности построения одношаговой стратегии для "Micro Lambda Calculus" профессор Клоп, к сожалению, не ответил. В письме предлагалась стратегия, определяемая в виде библиотеки языка Python с использованием лишь цепочек if-elif-else и рекурсии.
Коротко стратегию можно определить следующим образом. Если тело функции в самом левом ("leftmost outermost") редексе имеет форму \a. \b. ... \z. M, где M - редекс, то выбирать для редукции следует редекс M. В противном случае, выбирать для редукции самый левый редекс.
Стратегия была построена похожей на многошаговую стратегию, описанную в статье "Axioms for the Theory of Lambda-Conversion" (Gyorgy Revesz). Полученный алгоритм был проанализирован очень поверхностно, причем рассмотривалась эквивалентность оригинальному алгоритму Gyorgy Revesz, так что вопросы о корректности построения и нормализующего свойства тогда не были разрешены. Был бы признателен за помощь в определении корректности построения одношаговой стратегии и доказательстве или опровержении еe нормализующего свойства.
Коротко стратегию можно определить следующим образом. Если тело функции в самом левом ("leftmost outermost") редексе имеет форму \a. \b. ... \z. M, где M - редекс, то выбирать для редукции следует редекс M. В противном случае, выбирать для редукции самый левый редекс.
Стратегия была построена похожей на многошаговую стратегию, описанную в статье "Axioms for the Theory of Lambda-Conversion" (Gyorgy Revesz). Полученный алгоритм был проанализирован очень поверхностно, причем рассмотривалась эквивалентность оригинальному алгоритму Gyorgy Revesz, так что вопросы о корректности построения и нормализующего свойства тогда не были разрешены. Был бы признателен за помощь в определении корректности построения одношаговой стратегии и доказательстве или опровержении еe нормализующего свойства.
