Лялецкий А. А.
Новые доказательства важных теорем бестипового экстенсионального –исчисления

Построены новые доказательства двух теорем бестипового экстенсионального <$E lambda>-исчисления: теоремы Карри о том, что произвольный <$E lambda>-терм имеет <$E beta eta>-нормальную форму тогда и только тогда, когда он имеет <$E beta>-нормальную форму, и теоремы нормализации для <$E beta eta>-редукции. Приведенный подход базируется на двух широко известных результатах: теореме об откладывании <$E eta>-редукции и свойстве сильной нормализуемости <$E eta>-редукции, которые позволяют естественным образом распространить некоторые утверждения с обычного <$E lambda>-исчисления на экстенсиональный случай.

PDF

Бібліографічний опис:
Лялецкий А. А.  Новые доказательства важных теорем бестипового экстенсионального –исчисления. Кибернетика и системный анализ. 2014. Т. 50, № 4. С. 53-63. URL: http://jnas.nbuv.gov.ua/article/UJRN-0000412697