Является ли моя программа полной по Тьюрингу?

Я потратил неделю или две на программирование простого логического решателя. Построив его, я задался вопросом, является ли язык, который он решает, полным по Тьюрингу или нет. Поэтому я написал небольшой набор уравнений, которые принимают любое допустимое выражение в комбинаторном исчислении SKI и создают результирующий набор, содержащий нормальную форму этого выражения. Поскольку SKI является полным по Тьюрингу, доказательство того, что мой язык может выполнять SKI, продемонстрирует его полноту по Тьюрингу.

Однако есть ошибка. Решатель не уменьшает выражение в обычном порядке. На самом деле он пробует каждый возможный порядок редукции. Это означает, что набор решений обычно огромен. Если нормальная форма существует, она будет там где-то, но трудно сказать где.

Это подводит меня к двум вопросам:

• Является ли мой язык полным по Тьюрингу? Или мне нужно найти лучшее доказательство?

• Является ли число решений вычислимой функцией входных данных?

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