codedot | Сильная редукция в комбинаторной логике

На вопрос о существовании эквивалента бета-эта-редукции для комбинаторной логики профессор Барендрегт ответил ссылкой на рассмотрение сильной редукции в работах Curry, Hindley, Seldin. В статье "Axioms for Strong Reduction in Combinatory Logic" (Roger Hindley) приводится, по сути, доказательство невозможности существования сильной редукции для CL-теории, а точнее, доказывается, что набор правил сильной редукции всегда бесконечен. Такое свойство, следовательно, оказывается и у комбинаторной логики с одноточечным базисом.

Это делает неприемлемым создание машины для сильной редукции на основе комбинаторной логики. Из известных теорий подходит для этой задачи лишь бестиповое лямбда-исчисление с бета-эта-редукцией, гарантирующее получение по четкому алгоритму (при использовании одной из нормализующих стратегий вычисления, например нормальной) так называемой бета-эта-нормальной формы, совпадающей для любых двух эктенсионально равных вычислимых выражений.