Я потратил неделю или две программирование на простой логический решатель. Построив его, я подумал, не решает ли язык, который он решает, является ли Тьюринг полным или нет. Поэтому я закодировал небольшую совокупность уравнений, которые принимают любое допустимое выражение в исчислении комбинаторов SKI и создают набор результатов, который содержит нормальную форму этого выражения. Поскольку SKI является Turing-complete, доказывая, что мой язык может выполнять SKI, он продемонстрировал бы свою полноту Turing.
Однако есть сбой. Решатель не уменьшает выражение в нормальном порядке. Фактически, что он делает, это попробовать все возможные порядки сокращения. Это означает, что набор решений обычно огромен. Если нормальная форма существует, она будет где-то там, но трудно сказать, где.
Это приводит меня к двум вопросам:
-
Является ли мой язык Тьюрингом полным? Или мне нужно найти лучшее доказательство?
-
Является ли число решений вычислимой функцией ввода?
(Сначала я предположил, что размер набора решений был экспоненциальным или факториальным по размеру ввода. Но при ближайшем рассмотрении это неверно. Вы можете написать огромные выражения, которые уже находятся в нормальной форме, и крошечные выражения, которые я не чувствую, что определение размера набора решений может быть равнозначным решению проблемы остановки, но я не совсем уверен...)
