Mar. 15th, 2008

Наивная попытка показать, что функция 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$

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

Profile

Anton Salikhmetov

November 2018

S M T W T F S
    123
45678 910
11121314151617
18192021222324
252627282930 

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Aug. 9th, 2025 12:26 am
Powered by Dreamwidth Studios