Skip to content

lawref.evaluator.strict

Strict closure — SPEC §103, и temporal scope правила — §87.

Наименьшая неподвижная точка строгих правил над accepted-входами; выводы получают origin derived (§73) и proof-узел rule_application (§180).

Attributes

NameDescription
SemiPlanNo description.
StrictPrepNo description.

Functions

NameDescription
negative_addend§111 (errata E-0116): есть ли под монотонным гардом ОТРИЦАТЕЛЬНОЕ
prepare_strictУстановка строгого слоя — чистая функция от узлов программы:
strict_closureStrict closure §103: наименьшая неподвижная точка строгих правил над
strict_ranksРанги §110 внутри строгого слоя (DECISION-0088 §2): монотонное чтение

SemiPlanattributemodule attribute#

SemiPlan = tuple[list[tuple[str, dict]], list[dict]] | None

StrictPrepattributemodule attribute#

StrictPrep = tuple[
  list[tuple[dict, list[tuple[str, dict]]]],
  dict[str, int] | None,
  list[tuple[str, dict]],
  list[dict],
  set,
  dict,
  dict[str, frozenset[str]],
  frozenset[str]
]

negative_addendfunction#

def negative_addend(aggregates: list[dict], subst: dict[str, dict], store: SupportStore, registry: ProofRegistry, issues: list[dict], rule_id: str, env: Any = None) -> bool

§111 (errata E-0116): есть ли под монотонным гардом ОТРИЦАТЕЛЬНОЕ слагаемое sum на этой подстановке. Если есть — issue MONOTONE_GUARD_NEGATIVE_ADDEND (error, адрес правила) и правило на подстановке не срабатывает: сумма отрицательных слагаемых над растущим множеством УБЫВАЕТ, и least fixed point §103 по такому гарду не определён.

ОБЩАЯ функция обоих слоёв (дописано 03.09.2026): до этой правки проверка стояла только здесь, в строгом слое, и та же сумма под тем же гардом у правила defeasible/defeater §104 считалась молча — ноль issue при неопределённом фикспойнте. Слой знака слагаемых не меняет: §111 говорит о монотонности гарда, а не о силе правила. Единственная дуга здесь та же, что у strict_closure: defeasible зовёт strict, обратной нет.

prepare_strictfunction#

def prepare_strict(nodes: list[dict]) -> StrictPrep

Установка строгого слоя — чистая функция от узлов программы: (исполнимые правила с конъюнктами, ранги §110 либо None, предупреждения NON_EXECUTABLE_RULE по id правила, issues рангов). Вид программы (evaluator.prepared) считает её один раз; до 02.09.2026 классификация 2124 правил kz-income-tax, их страты и анализ агрегатов повторялись в каждом из трёх вызовов strict_closure на КАЖДОЕ дело (0,7 с + 0,46 с). Issues записаны, а не выброшены: strict_closure воспроизводит их в том же порядке и тем же числом раз, что и до кэша, — байты документа целы.

strict_closurefunction#

def strict_closure(store: SupportStore, nodes: list[dict], legal_time: str, registry: ProofRegistry, issues: list[dict], limits: dict | None = None, env: Any = None, prepared: StrictPrep | None = None) -> None

Strict closure §103: наименьшая неподвижная точка строгих правил над accepted-входами; head-выводы получают origin derived (§73) и proof-узел rule_application (§180). V1-ограничения (issue NON_EXECUTABLE + пропуск правила): только strength=strict, head-Literal позитивной полярности, scope=true, body из established-конъюнктов.

strict_ranksfunction#

def strict_ranks(rules: list[tuple[dict, list[tuple[str, dict]]]], issues: list[dict], derived: set[str] | frozenset[str] = frozenset()) -> dict[str, int] | None

Ранги §110 внутри строгого слоя (DECISION-0088 §2): монотонное чтение (supported/monotone) конъюнктом — ранг производителя, статусно- чувствительное (голый атом, established, not_known, unknown, refuted) и перечисление (generator агрегата или домена квантора — ребро completion, errata E-0112, обёртка monotone его не снимает) — ранг производителя + 1; правила одной головы обеих полярностей — в одной страте (§110 п. 5). Несходимость — NON_EXECUTABLE_UNSTRATIFIED. Позитивной программе ранги не нужны — все нули (_needs_strata).

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.