MIPS, сильная редукция и дальнейшие планы
Системы, основанные на MIPS, имеют очень лаконичный и простой ассемблер и могли бы быть по праву названы идеальными императивными вычислительными системами. Как известно, на основе MIPS работает множество бытовой аппаратуры, сетевое оборудование, а также игровые приставки Playstation и Playstation 2, и такие системы отличаются низким энергопотреблением и отличной масштабируемостью. К сожалению, корпорации Intel и Microsoft сделали достаточно, чтобы практически полностью вытеснить MIPS с рынка персональных компьютеров.

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

К сожалению, в комбинаторной логике сильная редукция требует бесконечного набора аксиом, поэтому создание машины для сильной редукции на основе комбинаторной логики теряет смысл - гораздо легче при решении этой задачи обратиться к обычному лямбда-исчислению. С другой стороны, прямое примененение эта-конверсии в машинах для редукции графов является крайне неэффективным, так как требует прохода по дереву для проверки на свободное вхождение переменной в подвыражение. В свою очередь, попытки применить подход "Micro Lambda Calculus" (который, кстати, показал себя особенно неэффективным, по крайней мере, при выборе стратегии Gyorgy Revesz) к эта-редукции пока не увенчались успехом.

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