lawref.evaluator.whynot

§185 why_not(P) — blocker graph вида «тело правила не выполнено».

Почему это отдельный запрос, а не поле ответа. В движке несработавшего правила не существует как события: solve() перечисляет подстановки, удовлетворяющие телу, и правило, которое не сработало, просто даёт ПУСТОЕ перечисление. Точки, где кто-то говорит «правило R не применилось, потому что второй конъюнкт не установлен», в фикспойнте нет и быть не должно. §185 это и предполагает: why_not(P) строит blocker graph — то есть считает отдельно, уже по готовому store, а не сопровождает каждый вывод.

Главное правило модуля — не соврать в сторону «ложно». §185: «Why-not не должен утверждать, что отсутствующее условие ложно». В открытом мире §61–§63 это различие уже есть и его не надо изобретать: у пары опор четыре значения, и NEITHER («опор нет ни за, ни против») — не то же самое, что FALSE_ONLY («есть опора против»). Разметка конъюнктов ложится на них один в один:

TRUE_ONLY  → SATISFIED       конъюнкт выполнен
FALSE_ONLY → NOT_SATISFIED   есть опора ПРОТИВ — это и есть «refuted»
BOTH       → CONFLICTED      опоры с обеих сторон [§112](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#112-ambiguity-policy)
NEITHER    → UNDETERMINED    ничего не известно; «ложно» здесь запрещено

Несвязанная переменная даёт UNDETERMINED по той же причине: про конъюнкт с неизвестным аргументом нельзя сказать ничего, кроме «не определено».

Словарь нормативен и до сих пор не заполнялся. ApplicabilityStatus и TriggerStatus объявлены схемой (§174.1: RULE_APPLICATION обязан нести оба), но во всём дереве из них эмитировалось ровно одно зашитое значение. Здесь они получают смысл, ради которого заводились.

Границы v1 названы, а не обойдены. Диагностируются правила, чья голова — Literal и унифицируется с целью. Норм-шаблоны §122–§124 (голова norm_template_ref), правила вне среза strict_closure (нетривиальный scope, негативная голова) и defeasible-механика §104–§115 в разбор не входят: у них своя причина несрабатывания, и приписывать им конъюнктную было бы неверно. Каждое такое правило попадает в отчёт со статусом UNDETERMINED и причиной — молча пропущенное правило неотличимо от разобранного.

Attributes

Name	Description
CONJUNCT_STATUS	No description.
FOLD_GOAL_KINDS	No description.
HEAD_ARGUMENT_DETAIL	No description.
JUDGMENT_ENUM_CAP	No description.
TERM_ERROR_PRECEDENCE	No description.
TERM_ERROR_SILENT	No description.
TERM_ERROR_STATUS	No description.

Functions

Name	Description
candidate_rules	Кандидаты по цели: корзина её предиката (пусто — правил нет вовсе).
computed_head_arguments	Вычисляемые аргументы головы правила-кандидата (E-0164) — по записи
defeater_judgment_blockers	E-0100, носитель «условие дефитера» (клауза unless §149, правило
fold_blockers	§185 над предикатами свёртки §164.1 (DECISION-0156 §2.9).
fold_goal	Узел procedure §201.1 и вид цели, если цель — предикат свёртки.
head_compatible	Подстановка, при которой голова правила МОЖЕТ совпасть с целью (E-0105).
judgment_blockers	§47.3 + §185 (DECISION-0025, добор DECISION-0036): ground-литералы
order_requests	Запросы судье в каноническом порядке E-0111, без дублей по ключу.
position_judgment_blockers	E-0100, носитель condition цели §123/§124: судьи, от которых зависит
power_judgment_blockers	E-0100, носитель valid_when полномочия §127: судьи, от которых
request_key	E-0111: ключ запроса судье — канонические байты §208 объекта request
rules_by_head	Правила по ПРЕДИКАТУ ГОЛОВЫ, внутри — в порядке id (DECISION-0114 §2.4).
term_error_blockers	E-0105 (§58/§175/§185): ошибки терма у правил, которые могли бы вывести
term_error_inputs	missing_inputs §174 — по одному InputRequirement на (правило, код).
term_error_status	§175: статус результата по старшему из кодов ошибок терма.
unify_head	Подстановка, при которой голова правила совпадает с ground-целью.
why_not	Отчёт по кандидатам-правилам для ground-цели.

CONJUNCT_STATUSattributemodule attribute#

View source

CONJUNCT_STATUS = {
  'TRUE_ONLY': 'SATISFIED',
  'FALSE_ONLY': 'NOT_SATISFIED',
  'BOTH': 'CONFLICTED',
  'NEITHER': 'UNDETERMINED'
}

FOLD_GOAL_KINDSattributemodule attribute#

View source

FOLD_GOAL_KINDS = (
  ('validPredicate', 'valid'),
  ('enteredPredicate', 'entered'),
  ('currentStatePredicate', 'current')
)

HEAD_ARGUMENT_DETAILattributemodule attribute#

View source

HEAD_ARGUMENT_DETAIL = 'вычисляемый аргумент головы: равенство с целью не проверено — считать в объяснении нельзя (§185)'

JUDGMENT_ENUM_CAPattributemodule attribute#

View source

JUDGMENT_ENUM_CAP = 8

TERM_ERROR_PRECEDENCEattributemodule attribute#

View source

TERM_ERROR_PRECEDENCE = (
  'MISSING_INPUT',
  'MISSING_POLICY',
  'NON_EXECUTABLE',
  'EXTERNAL_UNAVAILABLE',
  'TYPE_ERROR',
  'RUNTIME_ERROR',
  'RESOURCE_LIMIT'
)

Show moreShow less

TERM_ERROR_SILENTattributemodule attribute#

View source

TERM_ERROR_SILENT = frozenset({'MISSING_PARAMETER_VALUE'})

TERM_ERROR_STATUSattributemodule attribute#

View source

TERM_ERROR_STATUS = {
  'MISSING_POLICY': 'MISSING_POLICY',
  'DEADLINE_POLICY_INVALID': 'MISSING_POLICY',
  'MISSING_CALENDAR': 'MISSING_INPUT',
  'CALENDAR_DATASET_INVALID': 'MISSING_INPUT',
  'CALENDAR_DATASET_HASH_MISMATCH': 'MISSING_INPUT',
  'CALENDAR_OUT_OF_RANGE': 'MISSING_INPUT',
  'EXTERNAL_SNAPSHOT_MISSING': 'EXTERNAL_UNAVAILABLE',
  'EXTERNAL_SNAPSHOT_CALL_MISSING': 'EXTERNAL_UNAVAILABLE',
  'EXTERNAL_SNAPSHOT_HASH_MISMATCH': 'EXTERNAL_UNAVAILABLE',
  'EXTERNAL_SNAPSHOT_PROGRAM_HASH_MISMATCH': 'EXTERNAL_UNAVAILABLE',
  'EXTERNAL_SNAPSHOT_CONTEXT_MISMATCH': 'EXTERNAL_UNAVAILABLE',
  'EXTERNAL_SNAPSHOT_TYPE_MISMATCH': 'EXTERNAL_UNAVAILABLE',
  'EXTERNAL_SNAPSHOT_DUPLICATE_CALL': 'EXTERNAL_UNAVAILABLE',
  'TYPE_ERROR': 'TYPE_ERROR',
  'CURRENCY_MISMATCH': 'TYPE_ERROR',
  'DIMENSION_MISMATCH': 'TYPE_ERROR',
  'DATE_INSTANT_MISMATCH': 'TYPE_ERROR',
  'RESOURCE_LIMIT': 'RESOURCE_LIMIT',
  'OPAQUE_NON_EXECUTABLE': 'NON_EXECUTABLE',
  'NON_EXHAUSTIVE_MATCH': 'NON_EXECUTABLE',
  'UNKNOWN_FUNCTION': 'NON_EXECUTABLE',
  'NON_EXECUTABLE_FUNCTION_RECURSION': 'NON_EXECUTABLE'
}

Show moreShow less

candidate_rulesfunction#

View source

def candidate_rules(index: dict[str, list[dict]], goal: dict) -> list[dict]

Кандидаты по цели: корзина её предиката (пусто — правил нет вовсе).

computed_head_argumentsfunction#

View source

def computed_head_arguments(head: dict) -> list[dict]

Вычисляемые аргументы головы правила-кандидата (E-0164) — по записи {position, term, status: UNEVALUATED, detail} на каждый аргумент, чей вид не переменная и не ground-значение (call §86, арифметика §58, let), в порядке позиций. Пусто у литеральной головы.

defeater_judgment_blockersfunction#

View source

def defeater_judgment_blockers(goal: dict, nodes: list[dict], store: SupportStore, judgment_decls: dict[str, dict], legal_time: str, env: Any = None, proof_nodes: list[dict] | None = None) -> list[dict]

E-0100, носитель «условие дефитера» (клауза unless §149, правило defeater §95.3): судьи, прочитанные из тел живых дефитеров СТОЯЩЕЙ цели.

Зовётся при паре TRUE_ONLY (вывод стоит поражаемо): корень обхода — только дефитеры головы цели, способные снять вывод (_defeater_can_remove); ниже корня обход тот же, что у judgment_blockers (§47.5 транзитивно), и живость E-0101 читается по конъюнктам дефитера так же. Результат — статус остаётся TRUE_ONLY, evaluation status REQUIRES_JUDGMENT с запросом: ответ судьи способен снять вывод. Общее правило, которое не сработало, дефитера не активирует — цель тогда NEITHER, и это путь judgment_blockers, где дефитер головы разбирается наравне (E-0066).

fold_blockersfunction#

View source

def fold_blockers(goal: dict, nodes: list[dict], store: SupportStore, proof_nodes: list[dict], env: Any = None) -> list[dict]

§185 над предикатами свёртки §164.1 (DECISION-0156 §2.9).

До DECISION-0156 попытка перехода понижалась в правило <P>/<T>/valid, и §185 называл его блокером с недостающими конъюнктами гарда. Правила больше нет: переход есть элемент узла procedure §201.1, а исход попытки — proof-узел procedure_step §180.2 с outcome и reason. Отчёт читает ЕГО и переводит в тот же словарь блокеров: rule — StableId ПЕРЕХОДА, conjuncts — недостающие посылки причины. Ничего не вычисляется заново: свёртка уже прошла, и §185 её только называет.

Граница названа: конъюнкты гарда размечаются по ИТОГОВОМУ store, тогда как свёртка читала префикс §161.2. У гарда над предикатом ниже барьера (обычный случай — барьер §161.2 иного и не допускает) они совпадают; у гарда, читающего свёртку ДРУГОГО экземпляра §163.1, могут разойтись, и тогда сводка блокера остаётся UNDETERMINED, а не объявляет посылку выполненной.

fold_goalfunction#

View source

def fold_goal(nodes: list[dict], goal: dict) -> tuple[dict, str] | None

Узел procedure §201.1 и вид цели, если цель — предикат свёртки.

head_compatiblefunction#

View source

def head_compatible(head: dict, goal: dict) -> dict[str, dict] | None

Подстановка, при которой голова правила МОЖЕТ совпасть с целью (E-0105).

От unify_head отличается ровно двумя допущениями, и оба названы: вычисляемый аргумент головы (call §86, арифметика §58) считается совместимым с любым аргументом цели — его значение без вычисления неизвестно, а §185 запрещает считать в объяснении; аргумент-переменная ЦЕЛИ (частично связанный подцель обхода) совместим с любым аргументом головы. Обход ошибок терма ищет правила, которые МОГЛИ БЫ вывести цель, и ложное «несовместимо» здесь дороже ложного «совместимо»: первое прячет причину, второе называет лишнее правило по имени.

judgment_blockersfunction#

View source

def judgment_blockers(goal: dict, nodes: list[dict], store: SupportStore, judgment_decls: dict[str, dict], legal_time: str, env: Any = None, proof_nodes: list[dict] | None = None) -> list[dict]

§47.3 + §185 (DECISION-0025, добор DECISION-0036): ground-литералы judgment-relations, стоящие между ground-целью и её возможным выводом.

Словарь — строго §185, через тот же _conjunct_report: запрос порождается там, где конъюнктный разбор ставит UNDETERMINED, плюс два добора DECISION-0036, живущие ТОЛЬКО здесь (сам §185-отчёт why_not не тронут):

• refuted-тест над judgment-relation при паре опор NEITHER — «опровергнуто ли» решает судья (adjudicated может быть отрицательным §73); НЕ транзитивно — FALSE_ONLY производных достижим лишь negative-выводами вне v1-разбора;
• judgment-конъюнкт с несвязанными переменными перечисляется по активному домену (кап JUDGMENT_ENUM_CAP кандидатов, порядок §208); не-judgment конъюнкт с переменной, не связанной ни целью, ни свидетелем store (errata E-0189, _witness_substs), по-прежнему вне разбора.

Судья под not_known/unknown при NEITHER — SATISFIED, запроса нет. Границы разбора — _judgment_skip_reason: с errata E-0066 сюда входят и поражаемые правила §104 (отчёт §185 у why_not при этом не тронут — он по-прежнему объясняет их несрабатывание механикой §107–§108). Правило, у которого иной конъюнкт УЖЕ не выполнен, запроса не даёт (errata E-0101, _rule_is_dead): судья называется только там, где его ответ может изменить исход; при нескольких правилах одной головы запрос собирается по живым, и голова без живого правила отвечает COMPUTED. Поражаемое правило, чей вывод поразил бы уже сработавший дефитер §107.3, запроса не даёт по той же мере (errata E-0103, _conclusion_defeated); proof_nodes — proof-граф вычисления, в котором лежат применения дефитеров (без него поражение не читается — так зовут только юнит-тесты).

Рекурсия — транзитивное распространение §47.5 (JUDGMENT_DEPENDENT по transitive dependency graph): неопределённая НЕ-судейская подцель разбирается своими правилами; цикл держит visited. Живых ветвей бывает несколько, и у каждой свой судья (errata E-0111): посещение ключуется парой (атом, полярность), отрицательная подцель спускается в правила с отрицательной головой, собираются ВСЕ живые ветви. До errata посещение ключевалось без полярности, и на развилке g ⇐ p / g ⇐ q ⇐ not p ветвь, дошедшая до p первой, закрывала not p для второй — какая первая, решал порядок обхода реализации, и оракул с движком называли разных судей. Порядок результата — канонические байты §208 объекта request (request_key): воспроизводимость §211.

order_requestsfunction#

View source

def order_requests(literals: list[dict]) -> list[dict]

Запросы судье в каноническом порядке E-0111, без дублей по ключу.

position_judgment_blockersfunction#

View source

def position_judgment_blockers(positions: list[dict], store: SupportStore, judgment_decls: dict[str, dict]) -> list[dict]

E-0100, носитель condition цели §123/§124: судьи, от которых зависит статус позиции обязанности (achievement/maintenance) в запросе positions.

Живость — по §134: позиция ACTIVE либо UNDETERMINED (в окне ответ судьи даёт SATISFIED/VIOLATED, после окна — разрешает неопределённость); PENDING, CREATED, DEFEATED, SATISFIED и VIOLATED ответом судьи не меняются. Условие — ground-литерал payload (condition_literal), пара NEITHER.

power_judgment_blockersfunction#

View source

def power_judgment_blockers(goal: dict, positions: list[dict], store: SupportStore, judgment_decls: dict[str, dict], blocked_effect: dict | None = None) -> list[dict]

E-0100, носитель valid_when полномочия §127: судьи, от которых зависит действительность ОСУЩЕСТВЛЁННОГО полномочия с эффектом-целью.

Живость — по §127: позиция ACTIVE, событие exercise в деле (без попытки эффекта нет не из-за судьи, запроса нет), valid_when читает отношение суждения при паре NEITHER.

E-0120 (§47.3/§128) — третье лицо живости, после E-0101 (мёртвое правило) и E-0103 (поражённый вывод): полномочие, чей эффект заперт применимым и не побеждённым иммунитетом §128 на ЭТОМ деле, не живо — ответ судьи исхода не изменит, и запроса от valid_when нет. Как и у _conclusion_defeated, вердикт ЧИТАЕТСЯ по уже вычисленному, а не решается заново: материализация эффектов §127 сравнила protected_effect и приоритеты §106 (effects.immunity_verdict) и записала исход в карту blocked_effects под ключом эффекта — reason: "immunity". Пересчитать его здесь нельзя: связка _rule, на которой стоит §106, снимается с позиций до ответа.

request_keyfunction#

View source

def request_key(literal: dict) -> str

E-0111: ключ запроса судье — канонические байты §208 объекта request (отношение, полярность, аргументы). Он же задаёт порядок элементов results[].judgmentRequests и нумерацию proof-узлов judgment: два запроса одного отношения с разной полярностью — разные запросы, и один вопрос обязан давать один документ при любом порядке обхода.

rules_by_headfunction#

View source

def rules_by_head(nodes: list[dict]) -> dict[str, list[dict]]

Правила по ПРЕДИКАТУ ГОЛОВЫ, внутри — в порядке id (DECISION-0114 §2.4).

Обходы §185 (term_error_blockers, judgment_blockers и соседи) ищут правила, чья голова совместима с целью, и обе совместимости — unify_head и head_compatible — отвергают несовпадение предикатов ПЕРВОЙ проверкой. Значит правило с другим предикатом головы не может попасть в ответ ни при каком продолжении обхода, и индекс отдаёт ровно то же множество кандидатов, что полный скан.

Порядок сохранён намеренно и является частью контракта: внутри корзины правила лежат в том же порядке id, в каком их обходил скан, поэтому порядок посещения подцелей, порядок вставки в found и, значит, байты ответа не меняются. Селфтест сверяет обе стороны — множество и порядок.

Замер, ради которого индекс заведён (04.09.2026): у обхода стоял sorted(n for n in nodes if kind == "rule") ВНУТРИ walk, то есть все узлы программы фильтровались и сортировались на каждый шаг обхода. На kz-entrepreneurial-code (5890 узлов, 1704 сценария) половина тёплого вызова уходила в term_error_blockers: 31 тыс. вызовов head_compatible на один вопрос.

term_error_blockersfunction#

View source

def term_error_blockers(goal: dict, nodes: list[dict], store: SupportStore, issues: list[dict], legal_time: str, env: Any = None) -> list[dict]

E-0105 (§58/§175/§185): ошибки терма у правил, которые могли бы вывести цель, — то, из-за чего результат NEITHER есть не «право молчит», а «право не посчитано».

Обход — тот же, что у запроса судьи §47.5: правила, чья голова совместима с целью (head_compatible: вычисляемый аргумент головы не мешает), и дальше в их конъюнкты без опоры (пара NEITHER у связанного, любой несвязанный — по предикату). У каждого правила читается store.term_errors — те же пары (правило, код), по которым вычисление уже выпустило issue: здесь ничего не считается заново, а только называется. Сообщение берётся из той самой issue. Порядок — по правилу и коду (§211).

term_error_inputsfunction#

View source

def term_error_inputs(blockers: list[dict], query_tail: str) -> list[dict]

missing_inputs §174 — по одному InputRequirement на (правило, код).

term_error_statusfunction#

View source

def term_error_status(blockers: list[dict]) -> str

§175: статус результата по старшему из кодов ошибок терма.

unify_headfunction#

View source

def unify_head(head: dict, goal: dict) -> dict | None

Подстановка, при которой голова правила совпадает с ground-целью.

None — головы несовместимы. Цель обязана быть ground: why_not спрашивают про конкретное утверждение («почему не разрешено Бобу»), а не про схему.

Переменная, встреченная дважды, обязана связаться одинаково: p(x, x) против цели p(a, b) не унифицируется. Без этой проверки правило с повторной переменной диагностировалось бы по неверной подстановке.

why_notfunction#

View source

def why_not(goal: dict, nodes: list[dict], store: SupportStore, legal_time: str, env: Any = None, excluded: tuple[list[dict], dict[str, str]] | None = None, proof_nodes: list[dict] | None = None) -> list[dict]

Отчёт по кандидатам-правилам для ground-цели.

Порядок — по id правила (§211): отчёт обязан быть воспроизводим. excluded — правила, исключённые проекцией §92.3 (E-0095), и причина по id: в вычислении их нет, в объяснении они — NOT_APPLICABLE, тем же словарём, что правило вне effective §87.