Авторский контракт словаря вычислительной сложности Arxo

ru · unofficial · sha256:5b6dbb392297eec877fd4a9be3060e4757751c4c0d28373299ef1803bfd6e824RU

Авторский контракт словаря вычислительной сложности Arxo, версия 0.1.0. Language обозначает множество конечных строк над фиксированным конечным алфавитом. DecisionProblem обозначает неформально сформулированную задачу (например, Satisfiability, Clique, Hamiltonian Circuit) до её кодирования языком строк; has_language связывает задачу с её языком. TuringMachine обозначает (возможно, недетерминированную) машину Тьюринга — единственную формальную модель исполнителя в этом словаре, вслед за официальной постановкой CMI, которая определяет P и NP через L(M) для машины Тьюринга M, а не через неформальный алгоритм. Instance обозначает предъявленную строку входа. Certificate обозначает предъявленную строку-свидетеля y для проверочного отношения R(w, y). decides(m, l) — M решает L: L = L(M). runs_in_polynomial_time(m) — худшее время работы M ограничено фиксированным полиномом от длины входа. in_class_P(l) выводится только из decides и runs_in_polynomial_time вместе. checks_certificate(m, l) — M вычисляет проверочное отношение R для L: w принадлежит L тогда и только тогда, когда существует y с R(w, y). certificate_length_polynomial(m) — свидетель y ограничен полиномом от длины w. in_class_NP(l) выводится только из всех трёх фактов сразу: проверочная машина, её полиномиальное время и полиномиальная длина свидетеля. certificate_presented(y, i) фиксирует только предъявление свидетеля, не его проверку: проверка — отдельное исполнимое вычисление (calc.sat_certificates), не институциональный факт этого словаря. reduces_to_karp(from, to) — полиномиальное сведение "многие-к-одному" (Karp), Definition 3 официальной постановки CMI. reduces_to_cook(from, to) — полиномиальное сведение по Тьюрингу (оракульное), использованное Куком в 1971 году. Эти два отношения НИКОГДА не объединяются одним правилом: смешение видов сведения — прямая семантическая ошибка. reduces_to_karp транзитивно: композиция двух полиномиальных функций полиномиальна. is_np_hard_established_directly(l) — источник напрямую доказывает, что каждый язык из NP сводится к L, не опираясь на уже установленную NP-трудную задачу (случай Кука-Левина для SAT). is_np_hard(l) выводится либо из этого прямого доказательства, либо распространением: если `from` NP-труден и `from` сводится по Карпу к `to`, то `to` NP-труден (техника Карпа 1972 года) — is_np_hard никогда не утверждается напрямую как факт дела, только правилами. is_np_complete(l) выводится ТОЛЬКО из одновременного наличия in_class_NP(l) И is_np_hard(l) — союз двух оснований, не выбор одного из них. identifies_p_vs_np(c) — источник заявил claim c как формулировку вопроса P versus NP; соединяется со словарём arxo.math_claims так же, как identifies_riemann_hypothesis в arxo.zeta.

Referencing norms: Certificate, DecisionProblem, InClassNpByPolyTimeChecker, InClassPByPolyTimeDecider, Instance, IsNpCompleteRequiresBoth, IsNpHardFromDirectProof, IsNpHardPropagatesByKarpReduction, Language, ReducesToKarpComposes, TuringMachine, certificate_length_polynomial, certificate_presented, checks_certificate, decides, has_language, identifies_p_vs_np, in_class_NP, in_class_P, instance_of, is_np_complete, is_np_hard, is_np_hard_established_directly, reduces_to_cook, reduces_to_karp, runs_in_polynomial_time