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

  Повний текст PDF - 150.181 Kb    Зміст випуску     Цитування публікації

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"