lawref.evaluator.focus
focused_truth — полнота относительно вопроса (SPEC §181.3, DECISION-0368).
Эталон ВСЕГДА исполняет полный truth о том же литерале и проецирует его
документ D по конусу вопроса: ProjectFocused(D). Способ вычисления в
байты не входит; порт вправе исполнять только подпрограмму конуса там, где
статический квалификатор DECISION-0368 §3.8 это разрешил, но обязан выдать
ровно эти байты.
Функции модуля — чистые функции от IR вида программы и документа D:
конус (cone), профиль первого среза (profile_refusal), проекция
(project). Порядок всех перечней — §208-порядок строк либо порядок D.
Attributes
| Name | Description |
|---|---|
CONTRACT | No description. |
PROFILE | No description. |
SCHEMA_VERSION | No description. |
Functions
| Name | Description |
|---|---|
comparable_nodes | Узлы proof focused-документа в форме для сверки двух путей: без узла |
cone | §181.3: наименьшее множество предикатов, замкнутое назад по рёбрам |
cone_hash | No description. |
cone_subprogram | Программа, в которой из правил остались только правила с литеральной |
evaluate_focused | focused_truth: полный truth о том же литерале + ProjectFocused. |
profile_refusal | §181.3 «Вне профиля первого среза»: пересечение конуса с предикатами |
project | ProjectFocused(D) — §181.3 пп. 1–7. |
refusal_document | Отказ вида: манифест D, одна issue, без результата и без proof. |
view_nodes | Узлы вида программы — те же оси, что у полного вызова (§181.3: конус |
CONTRACTattributemodule attribute#
CONTRACT = 'law.focus/0.1'PROFILEattributemodule attribute#
PROFILE = 'i-relational-defeasible'SCHEMA_VERSIONattributemodule attribute#
SCHEMA_VERSION = 'law.core.focused-evaluation/0.1'comparable_nodesfunction#
def comparable_nodes(document: dict) -> list[bytes]Узлы proof focused-документа в форме для сверки двух путей: без узла завершения и корня, с сертификатами без привязки к программе и БЕЗ id (id сертификата §181.1 — контентный и включает эту привязку).
conefunction#
def cone(nodes: list[dict], predicate: str) -> tuple[list[str], list[str]]§181.3: наименьшее множество предикатов, замкнутое назад по рёбрам графа §110 (те же рёбра, что у замыканий §181.2) и по ограничениям §93.3, читающим конус. Возвращает (предикаты, ограничения) в §208-порядке строк.
Вершины замыканий §70 (id closure_policy) — вершины графа §110 наравне с
предикатами; в перечень предикатов конуса они не входят.
cone_hashfunction#
def cone_hash(predicates: list[str]) -> strcone_subprogramfunction#
def cone_subprogram(ir: dict, predicates: list[str]) -> dictПрограмма, в которой из правил остались только правила с литеральной головой предиката конуса; прочие узлы (декларации, утверждения, ограничения, замыкания, приоритеты) — без изменений и в прежнем порядке.
Не норма, а материал теоремы §3.6 п. 6: её вывод обязан дать те же узлы
proof по конусу, что и проекция полного документа. Манифест у неё свой
(другой programHash), поэтому сравниваются узлы, а не документы.
evaluate_focusedfunction#
def evaluate_focused(request, evaluate: Callable[[Any], dict]) -> dictfocused_truth: полный truth о том же литерале + ProjectFocused.
profile_refusalfunction#
def profile_refusal(nodes: list[dict], predicates: list[str]) -> dict | Noneprojectfunction#
def project(full: dict, query: dict, nodes: list[dict], case: dict, predicates: list[str], constraints: list[str]) -> dictProjectFocused(D) — §181.3 пп. 1–7.
refusal_documentfunction#
def refusal_document(full: dict, query_id: str, predicates: list[str], issue: dict) -> dictОтказ вида: манифест D, одна issue, без результата и без proof.
view_nodesfunction#
def view_nodes(request) -> list[dict]Узлы вида программы — те же оси, что у полного вызова (§181.3: конус считается после изоляции прочтений и проекции редакций).
Documentation for Arxo. Writings — blog.arxo.io.
Anonymous visit counts on stats.arxo.io, no cookies.