Лямбда-исчисление (547599), страница 3
Текст из файла (страница 3)
Следствие 1 (теоремы 5).
Множество -термов, имеющих нормальную форму, не рекурсивно.
Доказательство. Достаточно рассмотреть множество
-термов, имеющих нормальную форму, и его дополнение
до множества всех
-термов. Пара этих множеств удовлетворяет условиям теоремы 5. Если бы множество
было бы рекурсивно, то это противоречило бы утверждению теоремы (в качестве множества
можно было бы взять само
).
Аналогичным образом можно получить и другие результаты. Например,
Следствие 2 (теоремы 5).
Множество -термов, находящихся с заданным термом в отношении
-конверсии, не рекурсивно.
Следствие 3 (теоремы 5).
Любое нетривиальное подмножество -термов, замкнутое относительно отношения
-конверсии, не рекурсивно.
И так далее…
Доказательства аналогичны доказательству следствия 1.
-
Комбинаторное исчисление.
При более внимательном рассмотрении -исчисления, прежде всего, правила
-редукции, возникает мысль о реализации идей декомпозиции
-термов и построения формальной системы, обладающей теми же возможностями как математической модели вычислимости, что и
-исчисление, но без явного введения на синтаксическом уровне
-оператора, а вследствие этого, и без использования понятия связанной переменной,
-конверсии и т.д.
Введем три «комбинатора» – три замкнутых, т.е. не содержащих свободных вхождений переменных, -терма в нормальной форме:
Определим специальное представление -термов, как будет показано далее, экстенсионально эквивалентное: