# Часть VIII. Типовая система ## 34. Разделение data values и propositions Core различает: - **data values** — обычные типизированные значения; - **propositions** — утверждения, имеющие четырёхзначную support semantics. `Boolean` является двухзначным data type. Результат relation не является `Boolean`; это proposition, оцениваемое как `TRUE_ONLY`, `FALSE_ONLY`, `BOTH` или `NEITHER`. Нельзя присвоить proposition в Boolean без явного status test: ```text // Ошибка let x: Boolean = registered(company); // Корректно let x: Boolean = established(registered(company)); ``` ## 35. Встроенные типы данных `LanguageTag` 0.1 использует переносимый BCP-47-compatible subset `[A-Za-z]{2,8}(-[A-Za-z0-9]{1,8})*`; это поддерживает, в частности, `kk-KZ`, `ru-KZ` и region subtags вроде `es-419`. Resolver канонизирует casing для сравнения, но сохраняет исходное написание как source trivia. Grandfathered/private-use tags требуют feature profile и нормализуются в явный canonical value. `Timezone` 0.1 несёт имя зоны IANA tzdb в переносимом подмножестве `[A-Za-z][A-Za-z0-9_+-]*(/[A-Za-z0-9_+-]+){0,2}`: `UTC`, `Asia/Qyzylorda`, `Etc/GMT+5`, трёхсегментные имена вроде `America/Argentina/Buenos_Aires`. Значение вне этого подмножества именем зоны не является и отвергается до вычисления, как и всякое значение вне своего вида. **Существование зоны в базе профилем НЕ проверяется, и это не пробел, а граница:** правила зон versioned (§86), база пиннится отдельным `timezone_db_snapshot` (§85), а сверка с базой хоста внесла бы в семантический путь недетерминизм, запрещённый §211. Профиль отвечает на вопрос «это запись имени зоны», не на вопрос «такая зона есть»; регистр букв он тоже не предписывает — это свойство самой базы, а не формы записи (errata E-0061). ```text Boolean Integer Natural Decimal Rational Text LanguageTag Uri Digest Date LocalTime OffsetDateTime Instant Duration CalendarPeriod BusinessPeriod Timezone Currency Money Dimension Quantity Percentage Option Result List Set Map Interval ``` `null` отсутствует. Необязательное значение представляется `Option`. `Rational` (errata E-0005) — точное рациональное значение: тип результата точного деления (§58) и допустимая внутренняя арифметика (§18); в canonical serialization представляется несократимой дробью. **Носитель не ограничен по разрядности** (errata E-0159) — ни в значении, ни в промежуточных вычислениях; защита от неограниченного расхода — счётчики §238, а не ширина отдельного значения, и её превышение даёт `RESOURCE_LIMIT` без частичного результата. Этим `Rational` отличается от `Integer`, у которого §58 (errata E-0075) предел значения называет прямо; на `Integer`, индексы, размеры и результаты конверсий в другой числовой вид неограниченность носителя `Rational` не распространяется. `CardinalityError` (§51), `CountryCode` (§37) и `Jurisdiction` (§54/§89, errata E-0039) — библиотечные типы `law.std.data` (§257), а не встроенные типы ядра. Перечень выше **закрыт** и вместе с §257–§266 составляет словарь имён типов, разрешаемых в `urn:law:std#N`; имя вне этого словаря обязано быть объявлено в файле (§36–§40), иначе это статическая ошибка. **Порядок разрешения имени типа (errata E-0155, DECISION-0166 §4.4):** квалификация `law.std.::N` всегда адресует `urn:law:std#N` и не требует resolve-контекста (имя, которого пакет прелюдии не экспортирует или которое в позиции типа не разрешается, — `LDC-E2101`); generic-применение (`Option`, `List`, `Money`) и литералы (`10 kg`, `2026-09-06`, `100 KZT`) всегда несут тип std; голое имя разрешается в объявление ТЕКУЩЕГО пакета, если оно есть, иначе в прелюдию. Локальное объявление с именем прелюдии законно и сопровождается предупреждением `LDC-W1115` (как взять std квалификацией), а не ошибкой. До E-0155 действовало обратное правило E-0039: std-имя перекрывало объявление пакета молча. **Параметрические std-имена перечислены здесь же, и перечень закрыт (errata E-0194).** Параметр законен ровно у семи: `Option`, `Result`, `List`, `Set`, `Map`, `Interval` и `Money`. У всякого другого std-имени параметр — статическая ошибка `LDC-E2118` (§189), и `Quantity` названа первой: до errata таблица печатала `Quantity`, примеры §45–§48 писали `Quantity` и `Quantity`, грамматика (`type_ref`) параметр принимала, `lower` понижал его в `args` узла типа, схема `legal-ir` документ принимала — и НИКТО не проверял: величина массы, переданная в слот длины, давала `check OK` (проба 20.09.2026). Это тот же класс, что E-0064 (`Quantity` в примере §49), только носителем была не иллюстрация, а сама форма записи. Размерность в 0.1 несёт алгебра `Magnitude` §49.1 (DECISION-0154, errata E-0136), и она вычисляет её по реестру единиц §49.2, а не хранит в имени типа; второй механизм размерности в имени завёл бы второй источник истины о ней. Ни `Dimension`, ни имена размерностей (`Mass`, `Length`, `Velocity`) в позиции типа не разрешаются вовсе. **ЧИСЛО параметров у этих семи — часть их объявления (errata E-0201).** Форма каждого напечатана таблицей выше, и несовпадение с ней — статическая ошибка `LDC-E2121` (§189): `Set`, `Option`, `Map` и `Result` до errata понижались в `args` узла типа и не проверялись ничем — та же дыра, что у параметра непараметрического имени, и закрыта она отдельным кодом, потому что утверждает другое. Что именно законно в позиции `T`, `K`, `V`, `E` и `C`, перечень не сужает: §35 вид параметра не ограничивает, а описательная запись `Money` §50 объявлена НЕ поверхностью 0.1 (errata E-0130). ## 36. Nominal entity types ```law pub entity Person; pub entity Company; pub entity Permit; ``` Два nominal types несовместимы, даже если имеют одинаковое внутреннее представление ID. Entity identity не должна кодироваться mutable record fields. Факты об entity задаются relations/assertions. Standard constructor: ```law const project: BlastProject = entity_ref("urn:case:project:17"); ``` `entity_ref(id)` contextually получает ожидаемый nominal entity type. Identity является парой `(nominal_type, stable_id)`; одинаковая строка в `Person` и `Company` не делает values равными. В `core-production` entity ID должен быть absolute IRI/URN либо разрешённым package/case-scoped StableId. Anonymous/mutable entity objects отсутствуют. Entity declaration МОЖЕТ перечислять только intrinsic immutable payload fields; временные, sourced или юридически оспоримые свойства должны быть relations/assertions. Linter предлагает relation migration для полей `status`, `registered`, `owner`, `valid_until` и аналогичных изменяемых признаков. ## 37. Value records ```law pub record Address { country: CountryCode; region: Text; city: Text; street: Text; postal_code: Option; } ``` Records сравниваются структурно и являются immutable values. ## 38. Enums ```law pub enum EvidenceStatus { verified; unverified; disputed; expired; inadmissible; } ``` Enum variant имеет stable qualified identity. Она и есть его значение: равенство членов §57 сравнивает идентичность, порядок над перечислением не определён, а universe перечисления — его объявленные члены целиком (§70, §A3.3.1). StableId члена — `{namespace}#{Член}` (§24, errata E-0065); исполнимость члена как значения — errata E-0067. ## 39. Variants ```law pub type Identifier = NationalId { value: Text; } | BusinessId { value: Text; } | ForeignId { scheme: Text; value: Text; }; ``` Compiler ДОЛЖЕН проверять исчерпывающий `match` в executable profile. ## 40. Type aliases ```law type ArticleNumber = Natural; type RuleIdText = Text; ``` Alias не создаёт nominal separation. Для юридически значимого различия следует использовать entity или newtype profile. Прозрачность алиаса действует на обеих стадиях, а не только в статике: сверка типа аргумента против сигнатуры §189 (дело — errata E-0046, выведенная голова — E-0077) сравнивает имена ЗА цепочкой алиасов, и `relation r(n: N)` при `type N = Natural;` принимает значение `Natural` — иначе `check` принимал бы файл, который исполнение отвергает `TYPE_ERROR` (errata E-0098). Цикл алиасов обрывается на повторе имени. **Алиас на тип чужого пакета** (`type Persona = doctrine.ius_privatum::Persona;`) — та же qualified-ссылка §23, что и прямое употребление `pkg::T` в сигнатуре, и разрешается так же: без предъявленной зависимости — `LDC-E1104`/`LDC-E1105` при lowering (§24), с предъявленной — понижается в `type_decl` вида `alias` с целью `pkg#T`, а переменная такого типа — в локальный `ns#Persona`. Для статики `check` тип чужого пакета НЕПРОЗРАЧЕН: деклараций зависимости у неё нет, и совместимость аргумента §48 с параметром такого типа проверяется только по имени — два чужих имени совместимы, когда это одно имя; чужое имя против сущности этого пакета не проверяется ни в одну сторону (переменная типа-алиаса ходит и в предикат своего пакета, и в голову чужого); чужое имя в слоте скаляра std — `LDC-E2104`. До errata E-0098 алиас на чужой тип разрешался как неизвестное голое имя (`LDC-E2101` на каждом употреблении при том, что `lower` тот же файл принимал), а совместимость была односторонней: своя сущность в чужой слот принималась молча, чужая в свой — отвергалась. Голое имя за алиасом, которого пакет не объявляет, остаётся `LDC-E2101`. ## 41. Refinement constraints ```law record FineAmount { value: Money where self >= 0 KZT; } ``` Статически проверяемые ограничения проверяются compiler-ом; остальные становятся case validation constraints. Refinement не должен скрыто превращаться в нормативное правило. ## 42. Subtyping 0.1 поддерживает только явное nominal subtyping для entity categories: ```law entity NaturalPerson : Actor; entity LegalPerson : Actor; entity Court : PublicAuthority; ``` Roles вроде `Taxpayer`, `Employee`, `Applicant` СЛЕДУЕТ моделировать relations, а не subtypes, если они зависят от времени, дела или отношения. ## 43. Role sugar ```law role Taxpayer for Actor; ``` десугаризуется в: ```law const Taxpayer: LegalRole = entity_ref("#Taxpayer"); relation has_role( actor: Actor, legal_role: LegalRole, legal_context: LegalContext, during: Interval ); ``` `role` порождает **ровно одну** package-константу `Taxpayer: LegalRole` со значением собственного StableId. Это не создаёт ни membership-assertion, ни новую relation: `has_role` — единый standard relation `urn:law:std#has_role`. Если второй аргумент `has_role` является известной role-константой, compiler дополнительно проверяет, что первый аргумент совместим с её `for TypeRef`. Jurisdiction profile МОЖЕТ уточнить standard role model. ## 44. Concept sugar ```law concept Minor(person: Person); ``` десугаризуется в unary relation с `kind institutional`, если автор явно не указал другой kind. Запись депрекирована (errata E-0071): пара «concept против relation той же сигнатуры» даёт равный semantic hash §209, то есть форма — чистый поверхностный синоним, и корпус в 200 пакетов не употребил её ни разу (40 234 relation). Реализация отвечает предупреждением `LDC-E1328`; в 0.2 запись станет ошибкой. ## 45. Relations ```law pub relation registered(company: Company) kind institutional; pub relation measured_distance( project: BlastProject, distance: Quantity ) kind empirical; ``` Relation kinds: ```text empirical institutional evaluative derived normative_auxiliary external ``` Kind является metadata для analysis и policies. Сам по себе он не меняет truth semantics. ### 45.1. Relation keys Функциональные/record-like relations могут объявлять один или несколько candidate keys: ```law relation charge_mass( project: BlastProject, mass: Quantity ) kind empirical { key(project); } ``` `key(project)` означает integrity constraint: для одного accepted key tuple две различные non-key projections образуют `KEY_CONFLICT`. Evaluator НЕ выбирает последнее значение и не удаляет ни одну assertion. Conflict попадает в data-quality report и может сделать `the/value lookup` недетерминированным. Кого такой конфликт блокирует, решает §181.2 (errata E-0210): результат, чей вопрос отношения не читает по графу §110, остаётся `COMPUTED`, а issue в его документе несёт `warning`. Само правило §45.1 этим не смягчается — выбор по-прежнему не делается и ни одно утверждение не удаляется; меняется только область блокировки. Конфликт, принесённый ПАКЕТОМ, до вычисления не доживает: две его собственные ground-assertion одного отношения с одинаковой key-проекцией, разными остальными аргументами и пересекающимися окнами применимости §92 — статический отказ `LDC-E1368` (§196). Keys входят в semantic IR и используются для indexing, incremental invalidation и conflict detection. Они не создают closed-world semantics и не доказывают существование tuple. Несколько declared keys допустимы; пустой key запрещён. ## 46. Functions ```law pub pure function required_distance( charge: Quantity ) -> Quantity = if charge <= 500 kg then 320 m else 400 m; ``` Function: - возвращает data value, не proposition; - должна быть чистой в `pure` mode; - не может создавать assertions или norms; - не читает ambient clock/network; - может завершиться `Result`, если операция частична. `pure function` — явное требование чистоты; bare `function` — запрос на её вывод. Обе формы понижаются в `FunctionDecl` только когда полный транзитивный graph вызовов доказан как `PURE_DETERMINISTIC`. Локальная чистая функция и standard pure term являются допустимыми рёбрами; qualified/imported callee без effect descriptor даёт `LDC-E2403 COMPUTABILITY_NOT_PROVED`. Зависимость от snapshot, judgment или opaque declaration статически отклоняется и для explicit `pure`, и для inferred bare-формы. Block-body функции в 0.1 является expression-oriented: ноль или более `let`, затем ровно один `return`. Early return, loop и произвольный expression statement запрещены. Ветвление выражается `if` или `match`. Такой surface детерминированно понижается в nested `LetTerm` и один итоговый Term, без control-flow graph и скрытых side effects. В `core-executable/0.1` function recursion запрещена, если compiler не доказал structural termination. Reference compiler baseline МОЖЕТ консервативно запрещать всю user-defined recursion. Циклы между functions являются static error. Modeling rule: sourced, temporal или potentially conflicting attribute СЛЕДУЕТ представлять relation + assertions/evidence, а не pure function. Pure function предназначена для детерминированного вычисления из уже выбранных values; snapshot function — для pinned external dataset. Linter предупреждает, если public pure function выглядит как mutable registry lookup без snapshot dependency. ### 46.1. Тотальные отображения перечислений (аддитивно, DECISION-0069) ```law pub map harmony_of: Vowel -> Harmony { A => Zhuan; Ae => Zhinishke; Y => Zhuan; } ``` `map` — закрытое ТОТАЛЬНОЕ отображение перечисления в перечисление, сахар над pure function §46: собственного вида узла CLIR у него НЕТ, декларация понижается в `SymbolDecl` + `FunctionDecl`, чьё тело — if-цепь по идентичностям членов (§57, errata E-0067) в порядке пар источника; последняя пара — терминальный else, потому что тотальность доказана и ветви «не член» не существует. Происхождение узла помечено provenance-атрибутом `mapKind: enum-total` с доменом и кодоменом. Собственное свойство у формы одно, и ради него она существует: компилятор ДОКАЗЫВАЕТ тотальность по объявленному составу домена. Каждый член домена отображён ровно один раз, каждое значение — объявленный член кодомена; пропуск, повтор, чужое имя и не-перечисление на любой из позиций — статическая ошибка `LDC-E1326`, и она обязана звучать уже в `check` («check OK на декларации, которую отказывается компилировать lower» — запрещённое состояние). За то же свойство A3-таблица берёт `total: true`; рукописная функция §46 его не обещает никому. Домен и кодомен — имена перечислений ЭТОГО пакета: тотальность доказывается по объявленному составу, а контекст импорта §23 несёт плоский список имён, состава чужого перечисления в нём нет. Межпакетное отображение — аддитивный кандидат, зависящий от расширения контекста импорта (DECISION-0069 §5). Слово `map` — contextual keyword позиции декларации (как `entrenchment`), а не hard keyword §15: программа, использующая `map` как имя, разбирается как прежде, и minor-версии языка добавление не требует. ## 47. Effect/capability classes ### 47.1. `pure` Детерминированная локальная функция без внешних зависимостей. ### 47.2. `snapshot` ```law external snapshot function exchange_rate( from: Currency, to: Currency, date: Date ) -> Decimal { capability "nbk.exchange-rates"; snapshot_from context.exchange_rate_snapshot; } ``` Результат детерминирован только относительно exact snapshot hash. Снимок, предъявленный сценарию §267, ОБЯЗАН нести `programHash`, и оценщик сверяет его с программой запроса (`EXTERNAL_SNAPSHOT_PROGRAM_HASH_MISMATCH`): набор решений внешнего вычислителя получен для конкретного права, и применение его к иной программе утверждало бы не то, что было вычислено (DECISION-0244). Вне сценариев `programHash` остаётся необязательным. `programHash` СНИМКА есть семантический хэш §209 программы запроса, у которой список `imports` заменён пустым (`imports: []`; проекция нормирует поле независимо от того, было ли оно в документе). Это НЕ `programHash` манифеста §170: тот охватывает и бухгалтерию импортов — `contentHash`, которым потребитель закрепил каждую зависимость, — и снимок протухал бы от перевыпуска далёкой зависимости, не изменившего в мире ни одного узла (errata E-0216, DECISION-0347 §2: замер назвал 62 минуты жизни снимка и раздвоение верного значения между закоммиченным CLIR и собранным из исходников). Пин закрепляет ПРАВО, к которому набор предъявлен: снимок по-прежнему не принимается программой с другими узлами — иным правилом, иной декларацией, иным связанным миром, — и перестаёт различать миры, отличающиеся только пинами зависимостей при тех же узлах. Сборочный якорь §11 у этого различия свой и проверяется линковщиком мира до вычисления (`LDC-E1104`). ### 47.3. `judgment` ```law external judgment relation proportionate( measure: AdministrativeMeasure, proceeding: Case ) { authority Court; request_schema ProportionalityAssessment; label ru-KZ official "Соразмерность меры"; } ``` Тело канала суждения несёт метки §218 наравне с прочими декларациями, имеющими тело: канал предъявляется юристу дважды — в вербализованной норме, которая на него ссылается, и в самом `JudgmentRequest`, где вопрос адресован органу. Без метки оба места зовут его идентификатором (errata E-0035). До поступления adjudicated assertion результат остаётся `NEITHER` с evaluation status `REQUIRES_JUDGMENT`. Носитель канала — ЛЮБАЯ статусная формула, которую программа вычисляет, а не только тело правила (errata E-0100). Отношение суждения, прочитанное из `valid_when` полномочия §127, из `condition` цели обязанности §123 либо из условия дефитера — клаузы `unless` §149 либо правила `defeater` §95.3 (отсылка поправлена 03.09.2026 при исполнении E-0100: прежний адрес §113 — default negation, условия дефитера там нет), обязано давать тот же ответ, что и из тела правила: результат `NEITHER` с evaluation status `REQUIRES_JUDGMENT` и типизированный `JudgmentRequest` в `results[].judgmentRequests`. Обратное прочтение — что канал виден только сквозь `when` — обе реализации держали до 02.09.2026, и вопрос об эффекте полномочия, чья действительность зависит от судьи, отвечал `NEITHER` с evaluation status `COMPUTED`: молчанием, неотличимым от нехватки фактов. Это тот же дефект, что закрыла errata E-0066 для силы правила, и та же его цена: канал §47.3 существует ровно затем, чтобы «право посчитано и молчит» не выглядело как «решает суд». Требование касается СТАТУСА, а не исхода. Эффект полномочия, чей `valid_when` не решён, по-прежнему не материализуется — §127 не даёт опоры без выполненного условия действительности; меняется лишь то, ЧЕМ документ объясняет отсутствие эффекта. Запрос называет судью только там, где его ответ МОЖЕТ изменить исход (errata E-0101). Правило, чьё тело читает отношение суждения, даёт `JudgmentRequest` лишь пока оно живо на подстановке цели: ни один другой его конъюнкт не выполнен заведомо — нет опоры против (`FALSE_ONLY`), нет конфликта опор (`BOTH`), не провален гард §57–§58, не найдена опора под отрицанием по умолчанию §113, не расходится статус-тест §65. Такое правило мертво: что бы ни ответил судья, оно не сработает, и «решает суд» здесь было бы ложью при праве, которое уже ответило. Неопределённый конъюнкт (`NEITHER`) правило не убивает — недостающий факт может прийти, и судья остаётся адресатом. При нескольких правилах одной головы запрос собирается по живым: голова, у которой живых правил нет, отвечает `NEITHER` с evaluation status `COMPUTED` и пустым `judgmentRequests`, а два правила с двумя судьями называют судью того, которое живо. Единственное исключение — refuted-тест над самим отношением суждения при паре `NEITHER` (DECISION-0036 (а)): там «опровергнуто ли» ещё не решено, решает судья, и правило живо. Обе реализации до 02.09.2026 читали обратное: обход блокеров §185 спускался в судейский конъюнкт, не глядя на опровергнутого соседа, и правило `head ⇐ gate ∧ judged` на деле `not gate` отвечало `REQUIRES_JUDGMENT` с запросом, ответ на который ничего изменить не мог; сила правила (§104) этого не меняла. Живость читается и по ПОРАЖЕНИЮ вывода (errata E-0103): поражаемое правило §104, живое по конъюнктам, запроса не даёт, если дефитер §107.3 его цели уже дал применение на этом деле и правило не имеет над ним приоритета §106 (цикл §106 приоритета не даёт никому). Кандидат такого правила стоял бы в той же страте §110/§111, что и дефитер, и был бы поражён при любом ответе судьи; adjudicated assertion его не оживляет — исход тот же `NEITHER`/`COMPUTED`, в proof-графе узел `defeat`. Поражение читается по применениям proof-графа и замыканию приоритетов, которые вычисление уже произвело, — тела здесь не решаются заново и порядок не пересчитывается. Три границы названы поимённо. При любом условном приоритете §117/§118 в программе вопрос не решается и правило остаётся живым: ребро такого приоритета считается на паре применений, а гипотетического применения нет, — судья назван там, где, возможно, не нужен, то есть ошибка в прежнюю, безопасную сторону. §107.1 на этом пути не встречается: строгая опора комплемента делает цель `FALSE_ONLY`, и путь запроса не вызывается. §107.2 у противоположного поражаемого кандидата, который сам поражён, но старше правила, не читается: уцелевший такой кандидат делает цель `FALSE_ONLY` и до пути не доходит, а поражённый и старший — редкость, оставленная без чтения до собственного вектора. Третье лицо живости — ИММУНИТЕТ §128 (errata E-0120): полномочие, чей эффект заперт применимым и не побеждённым иммунитетом §128 на данном деле (совпал `protected_effect`, а при заданном `against` — и держатель полномочия; иммунитет старше по §106 либо пара непобеждена и несравнима, то есть эффект не создаётся и в conservative materialization §127), не живо — запроса судье от его `valid_when` нет, результат остаётся `NEITHER` с evaluation status `COMPUTED`. Ответ судьи здесь не меняет ничего: действительным осуществление или нет, эффект заперт всё равно. Вердикт читается по уже вычисленному, как у поражения: материализация эффектов §127 сравнивает защищаемый эффект и приоритеты создавших правил, и путь запроса читает её исход, а не решает тела и приоритеты заново. Переменную правила, которую не связала цель, связывает СВИДЕТЕЛЬ (errata E-0189). Обход транзитивен — §47.5 выводит `JUDGMENT_DEPENDENT` по transitive dependency graph, и неопределённая не-судейская подцель разбирается своими правилами на любую глубину, — но спускается он в ground-подцель, а у правила `contract_avoided(c) ⇐ may_avoid_contract(c, p) ∧ notice_given(c, p)` цель `contract_avoided(c)` переменную `p` не связывает, и конъюнкт, выводимый правилом, которое ждёт судью, остаётся без адреса. Такую переменную связывает то, что дело уже установило: ground-атом store, совпавший с ПОЛОЖИТЕЛЬНЫМ литеральным конъюнктом того же правила под тестом `established` (пара `TRUE_ONLY`) либо `supported`/`monotone` (`TRUE_ONLY` или `BOTH`) — те же пары, что у свидетеля существования §98 (E-0165). Каждое продолжение подстановки разбирается как своя подстановка правила: со своей живостью (E-0101, E-0103), со спуском в неопределённые подцели и со своими судейскими конъюнктами; подстановка цели без продолжений разбирается по-прежнему, и запросы складываются. Это чтение store, а не вычисление, которого §185 в объяснении не допускает: свидетеля даёт лишь литерал, чьи аргументы — переменные, `entity_ref` и `value`; конъюнкт с вычисляемым аргументом (`call` §86, арифметика §58), с именованной константой, с `_` §98, отрицательный литерал и тесты `not_known`/`refuted`/`unknown` свидетелей не дают. Порядок детерминирован: конъюнкты — в порядке тела, атомы — по каноническому ключу §208, конъюнкт без единого свидетеля подстановку не меняет; продолжений не больше восьми на правило (тот же кап, что у перечисления DECISION-0036 (б)), кап берётся после каждого конъюнкта. Граница названа: переменная, не связанная ни целью, ни свидетелем, у судейского конъюнкта перечисляется по активному домену (DECISION-0036 (б)), у не-судейского оставляет конъюнкт вне разбора — результат `NEITHER` с evaluation status `COMPUTED`. Обход «по предикату» с частично связанной подцелью, которым §175 ищет ошибки терма (E-0105), судей НЕ ищет: там называется issue, которую вычисление уже выпустило, здесь назывался бы судья от имени правил, чью живость на несвязанной подстановке прочесть нельзя. До errata обе реализации отвечали на «расторгнут ли договор» `NEITHER`/`COMPUTED` с пустым `judgmentRequests` там, где на «вправе ли сторона расторгнуть» отвечали `REQUIRES_JUDGMENT`: спросивший о следствии не узнавал, что решает трибунал. Форма вопроса нормативна (errata E-0102): вход `evaluate` описан схемой `spec/schema/query.schema.json`, парной к `evaluation.schema.json`, и литерал вопроса — тот же `Literal`, что в CLIR, с обязательным `kind: "literal"`. Вопрос вне схемы не отвечается, а отвергается до вычисления error-объектом с кодом `QUERY_INVALID` (§172). До errata литерал без `kind` отвечался ДРУГИМ по смыслу ответом: ключ атома поле `kind` игнорирует, унификация с головой правила его требует, и тот же вопрос давал `COMPUTED` там, где вопрос с `kind` даёт `REQUIRES_JUDGMENT`, — без единой диагностики. #### 47.3.1. Ответ судьи (errata E-0089) Ответ органа — assertion с origin `adjudicated` (§73) над самим отношением; это единственное, что v1 требовал, и единственное, что он проверял. Ответ МОЖЕТ нести объект `judgment`: ```text judgment { authority: StableId; // орган, давший ответ request: Option;// JudgmentRequest, на который отвечено payload: Option; // ответ по форме request_schema } ``` - `authority` обязан совпадать с `authority` декларации отношения; иначе утверждение НЕ принимается (§73 не даёт опоры), а документ несёт issue `JUDGMENT_AUTHORITY_MISMATCH` (error) с адресом утверждения; - `payload` типизируется `request_schema` декларации по правилам §46/§48 (тот же тест, что у аргумента утверждения дела, E-0046); несовпадение — утверждение не принимается, issue `JUDGMENT_PAYLOAD_MISMATCH` (error); `payload` при декларации без `request_schema` — та же issue: форму ответа некому проверить; - ответ без `judgment` — утверждение самого отношения, как до errata: принимается без проверки органа и формы (v1-совместимость; §73 не требует большего). Ответ, не принятый по этим правилам, оставляет результат `REQUIRES_JUDGMENT` с тем же `JudgmentRequest`. Принятый ответ несёт `judgment` в атрибутах узла `assertion` proof-графа (§179) — проверяющий видит, чей ответ и по какой форме, не разбирая дело. Поверхность `.law`/`.lawcase` этот объект в v1 не выражает: он живёт в CLIR и в JSON дела; ассертия с `judgment` вне выразимого подмножества рендера §168. Судей может быть несколько (errata E-0111): при нескольких живых ветвях запрос перечисляет каждого, порядок — канонический по объекту `request` (§185). Живость читается и по иммунитету (errata E-0120): полномочие, чей эффект на данном деле заперт применимым и не побеждённым `Immunity` §128, не живо — запроса судье от его `valid_when` нет, статус `COMPUTED`; читается по уже вычисленным позициям, как поражение в E-0103. ### 47.4. `opaque` Представимое, но не исполняемое содержание. Оно может иметь source anchor и human description. ## 47.5. Computability classification Computability выводится compiler-ом по transitive dependency graph: ```text PURE_DETERMINISTIC SNAPSHOT_DETERMINISTIC PARTIAL_MISSING_INPUT JUDGMENT_DEPENDENT INTERPRETATION_DEPENDENT OPAQUE_NON_EXECUTABLE CONFLICTED UNSTRATIFIED_NON_EXECUTABLE ``` Автор может указать только expectation annotation, например `@expected_computability(PURE_DETERMINISTIC)`. Несовпадение expectation и inferred class является diagnostic. Автор не может объявлением скрыть judgment/external dependency. ## 48. Отсутствие implicit conversions Запрещены неявные преобразования: ```text Integer -> Money Date -> Instant Magnitude -> Quantity Text -> Uri Company -> Person ``` Разрешены только явно объявленные pure conversions. **Сущность против сущности (§42, errata E-0121).** Аргумент сущностного типа совместим с параметром, если его тип есть сам ожидаемый либо его потомок по цепи `base`, и цепь ведётся ЧЕРЕЗ ГРАНИЦУ ПАКЕТА: звеном может быть публичная сущность зависимости, чей надтип предъявил resolve-контекст §23 (`exportBases`, считает резолвер по CLIR зависимости, цепь алиасов §40 пройдена до цели). У статики три исхода: цепь доказана — совместимо; цепь известна целиком и не доходит до ожидаемого — `LDC-E2104`; звено лежит в пакете, чьих баз контекст не предъявил (в том числе при проверке без контекста), — пара НЕПРОВЕРЯЕМА и принимается: статика не утверждает несовместимости, которой не может доказать (та же непрозрачность чужого типа, что в §40 у E-0098). Скаляр std чужим типом не бывает — такая пара отвергается всегда. Стандартные номинальные типы (`Actor`, `Event`, `Action`, `LegalContext`) в цепи сравниваются по имени. ## 49. Dimensional checking Единицы §49.2 — атомы с точным рациональным масштабом и вектором семи базовых SI. `unit atm = 101325 * Pa;` — сахар явного объявления `unit atm dimension Mass / (Length * Time * Time) scale 101325 / 1;` (DECISION-0157, errata E-0150). ```text unit atm = 101325 * Pa; ``` ```text 500 kg > 100 m // type error 280 m + 40 m // valid 5 m / 1 s // v1: TYPE_ERROR — разные единицы (§58; тождественные делятся, E-0068) ``` Размерная проверка живёт в ДВУХ видах значений, и половины у них разные. У `Quantity` она отрицательная (ниже), у `Magnitude` — положительная: произведение, частное и явная конверсия внутри размерности определены таблицами §58.1, а сами единицы объявляются в пакете декларациями §49.2 (errata E-0136). Ни одна строка про `Quantity` этим не изменена. В Core 0.1 у размерной проверки `Quantity` есть только отрицательная половина: величины разных единиц не сравниваются и не складываются, произведение двух размерных величин не определено (таблица E-0021 пары не называет), а частное определено единственной строкой — `Quantity / Quantity` при ТОЖДЕСТВЕННОЙ единице, с безразмерным ответом (errata E-0068; она же — единственное расширение, проведённое через мотивирующий акт по DECISION-0068 п. 4). Всякий отказ на этой границе обязан быть громким `TYPE_ERROR`, а не видом по догадке (errata E-0064; вектор `ERR-E0064-QUANTITY-PAIR` — терм из третьей строки примера, РАЗНЫЕ единицы — держит границу байтово). `Quantity` в комментарии выше — forward-reference: этот вид появится только с unit-package. **Параметр у `Quantity` в 0.1 не определён и отвергается статически (errata E-0194, `LDC-E2118`).** Forward-reference остаётся forward-reference и не становится записываемой формой: `Quantity`, `Quantity`, `Quantity` — не типы, а обещание unit-package, и компилятор их не принимает. До errata принимал: грамматика `type_ref` параметр разбирала, `lower` понижал его в `args` узла типа, схема `legal-ir` документ принимала, а совместимость по параметру не проверялась ни в одном направлении — масса в слоте длины давала `check OK`. Размерность в 0.1 несёт `Magnitude` §49.1 (DECISION-0154, errata E-0136): она ВЫЧИСЛЯЕТСЯ по реестру единиц §49.2 — `magnitude(x)`, произведение и частное §58.1, `quantity_of(m, "kg")` на выходе, — а не хранится в имени типа. Отрицательная половина §49 у `Quantity` при этом не изменена ни строкой: тег единицы остаётся значением, сравнение и сложение разных единиц отвергаются тем же `TYPE_ERROR`. Unit package задаёт dimension algebra и canonical conversion factors. Conversion factor должен быть точным Decimal/Rational либо объявлять precision policy. Границы будущего пакета застолблены DECISION-0068 (конверсия только явной формой; канонизация существующих единиц-тегов не меняется; вход через feature-флаг, не правкой ядра); там же — замеры выразимого в v1: пороговая норма вида «15 м² на человека» выражается уже сейчас умножением насквозь (`a >= n * 15 sq_m`), а истинно заблокированы кросс-юнитные ставки, сравнение двух размерных отношений и производная величина как значение. Явная форма конверсии, объявленная рамкой 1 DECISION-0068, — терм (errata E-0072, второй мотивирующий акт `phys.zadachnik`): ```text convert(value, num, den, unit) ``` `value` — только `Quantity` (`Money` отвергается поимённо: конверсия валют — территория §50 с exchange rate и snapshot; у безразмерных видов единицы нет). `num`/`den` — точный фактор парой СТРОГО ПОЛОЖИТЕЛЬНЫХ `Integer`: фактор точен и вечен (`18/5` — определение, не курс), поэтому реестра факторов и снапшота нет — пара живёт аргументами при норме-владельце. `unit` — непустой `Text`, тег цели; сверить его с фактором не с чем без реестра, и пришивка «фактор ↔ тег» остаётся авторской, сторожимой тестами акта (§267). Вид результата — ПО ЗНАЧЕНИЮ, по правилу пары `Decimal / Decimal` §58: 10-гладкое частное — `Quantity` целевого тега, иначе точный `Rational` числом значения в целевой единице (снимает границу 10-гладкости: перевод «1 км/ч = 5/18 м/с» иначе невыразим — `Decimal * Rational` есть `TYPE_ERROR` §48). Оператор `/` §58 терм не меняет ни на одной паре: деление `Quantity` на скаляр остаётся МАСШТАБИРОВАНИЕМ с сохранением тега, и запись «переведи делением на 3,6» — задокументированная ловушка, которую закрывает не запрет, а существование честной формы. Обратный ход — пришивка «число → величина» — имеет собственную явную форму (errata E-0074, вторая молчаливая дыра того же замера): ```text with_unit(value, unit) ``` `value` — безразмерное число: `Integer`, `Decimal` либо 10-гладкий `Rational` (неточная дробь — отказ по канону `INEXACT_DIVISION`: округление только явной политикой §50/§18). `Quantity` отвергается ПОИМЁННО — «значение уже несёт единицу», и перетег делает только `convert`: повторная пришивка невыразима по построению. `Money` отвергается к §50. `unit` — непустой `Text`; результат — всегда `Quantity` названного тега (вид, в отличие от `convert`, известен статически). Форма закрывает класс опечатки «эталон не той единицы»: скалярный идиом `n * MetrEtalon` нёс единицу выхода ИМЕНЕМ КОНСТАНТЫ, значение которой пришивалось молча (правило выводило путь «300 секунд» со статусом TRUE_ONLY без единой диагностики), — здесь тег стоит литералом на месте пришивки, и эталоны выхода не нужны вовсе. Опечатка в самом литерале остаётся авторской и сторожится тестами акта §267 — граница названа, а не спрятана. ### 49.1. Алгебра размерностей: `Magnitude` (errata E-0136, DECISION-0154) Обещанная §49 dimension algebra приходит НОВЫМ видом значения — `Magnitude`, — а не правкой `Quantity`. Все операции над `Quantity` остаются теми же байтами: `Quantity * Quantity` по-прежнему `LDC-E2108`, деление разных тегов — по-прежнему `TYPE_ERROR` E-0068. Причина в рамке 3 DECISION-0068 в редакции E-0068: флаг на арифметической ОПЕРАЦИИ сделал бы семантику исполнения зависимой от манифеста, поэтому `law.units/0.1` остаётся входом ПАКЕТА (объявления единиц, переход, конверсия), а операции над новым видом определены всегда. **Что несёт значение.** Точный рациональный коэффициент произвольной разрядности и канонический мультимножитель простых единиц — отображение «имя простой единицы → ненулевой целый показатель». Размерность (вектор показателей по семи базовым SI — L, M, T, I, Θ, N, J) и масштаб (точная дробь к базовой единице) ВЫЧИСЛЯЮТСЯ по реестру определений §49.2 и в значении не хранятся: хранить их значило бы завести второй источник истины, расходящийся с реестром молча. **Канон составной единицы** — чистая функция мультимножителя: ```text canon(F) = num(F) при пустом знаменателе canon(F) = num(F) "_per_" den(F) иначе num(F) = "1" при пустом числителе num(F) = factor "_" … "_" factor имена по возрастанию байтов den(F) = factor "_" … "_" factor имена по возрастанию байтов factor = <имя простой единицы> <показатель> показатель 1 опускается ``` Показатель в записи — модуль; знак решает, в какую половину попадает множитель. Порядок множителей — байтовый порядок имён, отдельно в числителе и в знаменателе; поэтому перестановка сомножителей исходной записи байтов результата не меняет. **Идентичность НИКОГДА не разбирается обратно.** Имя базовой единицы само может содержать подчёркивание (`ft_per_half_min` — фут на `half_min`), и грамматика «база `_per_` база» неоднозначна; неоднозначность снимается не выбором правила разбора, а отсутствием разбора. **Идентичность — сам мультимножитель, канон — только его запись (errata E-0151).** Тождество единицы в §58.1 сравнивает множители, а не строки канона. После E-0150 простая единица может носить любое имя, в том числе читающееся как канон произведения: атом `ft2` (Length²) и `ft * ft` печатаются одной строкой `ft2` при разных множителях и масштабах, и сравнение строк отождествляло их молча — сложение и `==` проходили без `unit_convert`. Совпавшая строка при разных множителях — `UNIT_MISMATCH`, называющий оба мультимножителя (`ft2^1` против `ft^2`), потому что строка канона здесь не различает операнды. Запись §208 при этом не меняется: `unit` остаётся рендерингом `factors`, и одна строка у двух значений — дефект ИМЕНОВАНИЯ, который ворота пакетов единиц бракуют до исполнения (`check_units`, сверка 7: строка канона обязана читаться однозначно по всем простым именам мира). **Каноническая запись §208** несёт поэтому МУЛЬТИМНОЖИТЕЛЬ, а не одну строку: ```text {"kind": "value", "type": {"name": "urn:law:std#Magnitude"}, "unit": "<канон>", "factors": [{"unit": "<простая единица>", "exp": <ненулевое целое>}, …], "value": "<числитель>/<знаменатель>"} ``` При чтении `unit` не РАЗБИРАЕТСЯ, а СВЕРЯЕТСЯ с рендерингом `factors`: расхождение — громкий `TYPE_ERROR`, и подделать идентичность, не тронув множители, нельзя. Реестр §49.2 для чтения не нужен — значение самодостаточно; он нужен переходу и конверсии, которым требуются размерность и масштаб. Запись обязана быть читаемой, а не только печатаемой: величина, выведенная в голове правила, публикуется в store ground-литералом (§190), и односторонняя сериализация оставила бы её невыразимой в собственном выводе. Коэффициент ВСЕГДА несократимая дробь с положительным знаменателем — тот же канон, что у `Rational` (§35, E-0005). Десятичной ветви у него нет намеренно: она сделала бы ЗАПИСЬ значение-зависимой, а вслед за ней — и вид (дефект, найденный E-0020 у `Decimal / Decimal`). Мультимножитель в записи отсортирован конструктором, поэтому одному значению отвечают одни байты. **Сокращение — только по ТОЖДЕСТВЕННЫМ именам простых единиц.** `m_per_s * s` даёт `m`; `m / km` даёт `m_per_km` — величину НУЛЕВОЙ размерности с непустой единицей, а не число. Автоматического приведения масштабов нет нигде: рамка 1 DECISION-0068 («конверсия только явной формой») действует и внутри новой алгебры, поэтому `1 km` и `1000 m` остаются разными значениями и после перехода. **Безразмерный результат — заранее установленного вида.** Пустой мультимножитель даёт `Magnitude` с идентичностью `1`, всегда и независимо от значения. Число извлекается явным термом `scalar_of` (§259), который и исполняет приведение масштабов у величины нулевой размерности: `scalar_of(magnitude(100 cm) / magnitude(1 m))` есть точный `Rational` 1. **Отказы называют РОД, а не один код на всё.** До настоящей errata `1 km + 1 m` и `1 kg + 1 m` отвечали одним `DIMENSION_MISMATCH`, то есть диагностика врала о роде отказа. У нового вида их четыре: | Статика | Исполнение | Когда | |---|---|---| | `LDC-E2110` | `UNIT_UNKNOWN` | единица не объявлена ни в пакете, ни в его закреплённых зависимостях | | `LDC-E2111` | `UNIT_CYCLE` | цикл в определениях (производная через саму себя) | | `LDC-E2112` | `UNIT_DIMENSION_MISMATCH` | конверсия между РАЗНЫМИ размерностями | | `LDC-E2113` | `UNIT_MISMATCH` | операция над величинами разных единиц там, где требуется тождество (в том числе разных масштабов ОДНОЙ размерности) | Ни один из них не смешивается с `LDC-E1104` (материализация и пин зависимости) и `LDC-E1105` (разрешение ссылки): «единицы нет в реестре» и «зависимость не закреплена» — разные диагнозы с разными развязками. ### 49.2. Объявление единиц (errata E-0136, E-0150) Определения приходят закреплённой зависимостью — пакетом семейства `packs/units/`, а не словарём и не ресурсом §85. Поверхность — три декларации: ```text unit m dimension Length scale 1 / 1; unit cm dimension Length scale 1 / 100; derived unit m_per_s = m / s; unit alias metre = m; ``` `unit` объявляет ПРОСТУЮ единицу — атом алгебры: неделимый носитель точного положительного рационального масштаба и вектора размерности по семи базовым SI. Число участвующих баз не ограничивается одной; показатели целые, включая отрицательные. Раскрытие останавливается на атоме, поэтому его канон — собственное имя, даже при составной размерности. Масштаб задан парой строго положительных целых произвольной разрядности, включая дроби вроде `1 / 3`. `derived unit` объявляет производную ПРОИЗВЕДЕНИЕМ И ЧАСТНЫМ простых: собственного масштаба у неё нет, он вычисляется из множителей. `unit alias` — второе имя той же единицы: алиас и цель дают одно и то же значение после перехода, и байты результата у них совпадают. Семь базовых размерностей названы именами std: `Length`, `Mass`, `Time`, `Current`, `Temperature`, `Amount`, `Luminosity`. Носитель в CLIR — узел `unit_decl`; экспорт через границу пакета — `pub`, как у всякого символа §23. **Равносильные формы атома (DECISION-0157).** ```text unit atm = 101325 * Pa; unit atm dimension Mass / (Length * Time * Time) scale 101325 / 1; unit third = (1 / 3) * atm; ``` Правая часть сахара — произведение и частное точных целых/десятичных чисел и объявленных единиц со скобками. Арифметика рациональная, без округления. Ссылка на атом использует его масштаб и размерность, но результат становится НОВЫМ атомом. Алиас остаётся отдельной формой. Имена разрешаются в пакете и его закреплённых зависимостях; циклы, неизвестные ссылки, конфликт имён, неизвестные базы, нулевой или отрицательный масштаб, иррациональный и неопределённый множитель — статические отказы §49.1. Прямая ссылка допускается при отсутствии цикла. `dimension` допускает `*`, `/`, скобки и `1` (нулевой вектор); степень записывается повторением базы. Промежуточный показатель обязан помещаться в знаковое 64-битное целое CLIR; переполнение отвергается, а не оборачивается и не насыщается. **Нормализация перед хэшированием (§209).** Обе формы понижаются в один узел `unit_decl` вида `simple`: в CLIR нет правой части сахара. Дробь сокращается, показатели одинаковых баз объединяются, нули удаляются, пары идут в порядке `Length`, `Mass`, `Time`, `Current`, `Temperature`, `Amount`, `Luminosity`. При одинаковых имени, публичности и namespace узлы и их contentHash побайтово совпадают; provenance исходника не создаёт второй семантики. `202650 / 2` и `101325 / 1` дают одни байты. `derived unit` сохраняет раскрытие в прежние атомы. Объявленные в `units.si` кратные (`kPa`, `hPa`, `MPa`, `bar`, `MJ`, `kHz` и другие) не мигрируют: сокращение факторов, `project`, `exponent` и допустимость сложения определяются идентичностью атомов, а не физической эквивалентностью. Конверсия между ними остаётся явной (§259.1). ## 50. Money *Описательная схема, а не объявление поверхности 0.1 (параметр generic `` у записи): блок не компилируется намеренно и остаётся `text`; см. errata E-0130.* ```text record Money { amount: Decimal; } ``` - арифметика между разными currencies запрещена; - частное двух сумм ОДНОЙ валюты безразмерно — `Money / Money` по правилу пары `Decimal / Decimal` §58 (errata E-0083): доля, а не деньги; разные валюты — `CURRENCY_MISMATCH`; - произведение суммы на безразмерную долю `Rational` — деньги той же валюты (`Money * Rational`, errata E-0085): точное, когда итог 10-гладок, иначе `INEXACT_DIVISION` — rounding не подразумевается и здесь, политика называется `round`/`div_round`; - conversion требует exchange rate, date и snapshot; - rounding никогда не подразумевается; - monetary function ДОЛЖНА объявить rounding policy там, где результат не точен. Термы политики: ```text round(value, precision = 2, mode = HALF_UP) div_round(dividend, divisor, precision = 2, mode = HALF_UP) ``` `round` округляет уже вычисленное значение. `div_round` (errata E-0036) — единственный способ РАЗДЕЛИТЬ под политикой: он округляет ТОЧНОЕ частное, а не результат `/`, и потому применим там, где `/` отказывает раньше, чем `round` получил бы что округлять (§58). - Делимые — ЧЕТЫРЕ пары §58: три с делителем `Decimal` (`Money / Decimal` даёт `Money` той же валюты, `Quantity / Decimal` — `Quantity` той же единицы, `Decimal / Decimal` — `Decimal`) и пара `Money / Money` тождественной валюты (errata E-0170) — безразмерное частное вида `Decimal`. Виды и порядок операндов те же, что в таблице §58: `div_round(Money, Integer, …)` отвергается ровно как `Money / Integer`, потому что таблица §58 определяет ОПЕРАЦИЮ, а не форму записи. - `Integer / Integer` и `Rational / Rational` в делимые `div_round` не входят: их частное точно при любых входах, решать политике нечего, а округление сменило бы вид `Rational` → `Decimal` — конверсия, которой §48 не знает. - Округление применяется ВСЕГДА, а не только при неточном частном. Иначе точность результата зависела бы от значения, а не от нормы — тот самый дефект, который E-0020 нашла у `Decimal / Decimal`, где от значения зависел вид. На представимом частном ответ совпадает с `/`, если объявленная точность его вмещает. - Деление на ноль остаётся evaluation error §58: политика округления не делает его определённым. - `precision` и `mode` обязательны и у `round`, и у `div_round`: умолчания нет ни у одного из них (правило «rounding никогда не подразумевается» выше). `div_round` над парой `Money / Money` (errata E-0170) — ДОЛЯ, а не деньги: частное двух сумм одной валюты безразмерно (§58, E-0083), и политика этого не меняет. Она снимает другое — зависимость ВИДА от значения: у оператора `/` та же пара даёт `Decimal` при 10-гладком знаменателе и точный `Rational` иначе, а под политикой округление применяется всегда, поэтому `div_round(Money, Money, precision, mode)` есть `Decimal` при любом входе. Валюта обязана совпадать (`CURRENCY_MISMATCH` тем же правилом, что у `/`), нулевой делитель остаётся `DIVISION_BY_ZERO`. Пара нужна норме, которая САМА делит деньги на деньги и САМА называет округление частного. Ст. 14 2° арретэ от 27 сентября 2019 года (Франция, расчёт жилищных пособий) определяет `RL = L / LR` — отношение учитываемого найма к эталонному — и предписывает «RL est exprimé en pourcentage et arrondi à la deuxième décimale». До errata записать это было нечем: `round` §50 определён на Integer/Decimal/Money/Quantity и `Rational` не берёт, `div_round` пары не называл, а обход через вырожденный отрезок §259.2 (`round_bounds(bounds_const(L / LR, 1), 4, "HALF_UP")`) говорит о сертификате границ там, где норма говорит о делении с округлением, и вдобавок недоступен внутри `function` (§46/§47.5: чистота термов §259.2 не доказывается, `LDC-E2403`). `Quantity / Quantity` в делимые `div_round` НЕ входит: дыра у неё та же, но акта-заявителя нет — расширение ждёт его, как ждало умножение на долю (граница DECISION-0068). `round` над `Integer` (errata E-0110) — тождество: `round(n, precision, mode)` при `precision >= 0` и любом `mode` есть тот же `n`, вид `Integer`. Дробной части у целого нет, и `precision` её не порождает — конверсии в `Decimal` §48 не возникает. До errata обе реализации отвечали `TYPE_ERROR`, и норма, округлявшая целочисленный параметр A3 «по аналогии» с денежным, молча не срабатывала. ## 50.1. Percentage `12.5 percent` канонически хранится как точное Decimal `0.125` с display unit `percent`. Сложение percentage и обычного Decimal требует явного conversion, чтобы избежать смешения «12.5» и «0.125». ## 51. Collections - `List` — упорядоченная коллекция с дубликатами; - `Set` — неупорядоченная коллекция без дубликатов; - `Map` — неупорядоченное отображение; - итерация, влияющая на результат, ДОЛЖНА иметь детерминированный порядок; - `sum` над Decimal/Money/Quantity определяется точно; - `average` требует explicit rounding/precision, если результат не точен. Standard collection API включает: ```text only(Set) -> Result min(Set) -> Option max(Set) -> Option ``` `only(collect v: T where R(key, v))` является явным functional lookup. При нуле tuples возвращается `MissingValue`, при нескольких — `CardinalityConflict` с key/proof, а не произвольный first/last value. Обе коллекции порождаются comprehension §52.1: `collect` даёт `Set`, `collect all` — `List` (errata E-0012). Различие существенно для агрегатов §59: `Set` отвечает на вопрос «какие значения встречаются», `List` — «сколько чего начислено». Свод числового поля по множеству сущностей (совокупный доход семьи, сумма позиций начисления) выражается ТОЛЬКО через `List`: над `Set` две равные позиции неотличимы от одной, и `sum` молча недосчитывает. Обратно, `only`/`min`/`max` над `List` осмысленны, но кратность для них безразлична. Детерминированный порядок (требование выше) для `List`, порождённого comprehension, определяется каноническими байтами §207 элементов, а не порядком перебора solver-а: две реализации обязаны дать одну последовательность. Равные элементы неразличимы, поэтому порядок полон. ## 52. Finite domains Quantifier в executable profile должен иметь конечный domain: ```text forall employee in employees(company) satisfies ... ``` Неограниченный: ```text forall p in global_person_domain() satisfies ... ``` допустим в representation profile, но не executable без domain provider. ## 52.1. Finite relation comprehensions Для удобного перехода от relations к коллекциям authoring surface имеет строго ограниченный оператор: `collect all value: T, binder: U where F` допускает дополнительные existential-local binder-ы generator-а. В коллекцию входит только `value`; `binder` различает решения с одинаковым value и не свободен снаружи. Это нужно, например, когда две разные позиции владения несут одну и ту же долю. ```text collect actual: Quantity where measured_safety_distance(project, event, actual) ``` Результат имеет тип `Set` и содержит все distinct ground values `actual`, для которых generator formula установлена (`TRUE_ONLY`) в уже замороженном producer stratum — это ребро `completion` §110/§111 (errata E-0112): generator под агрегатом или доменом квантора ставит потребителя выше производителей независимо от обёртки `monotone`. Вторая форма — `collect all` (errata E-0012) — даёт `List` и содержит по одному элементу на КАЖДУЮ solution substitution generator-а, включая совпадающие значения: ```text collect all amount: Money where monthly_income(member, amount) ``` Два члена семьи с равным доходом дают в `Set` один элемент, в `List` — два. Форма без `all` остаётся distinct: это не default, а самостоятельное значение (§51), и существующие программы не меняют смысла. В CLIR различие несёт булев `ComprehensionTerm.distinct`: `true` — `Set`, `false` — `List`; поле обязательно, умолчания у него нет. Ограничения `core-executable` (ниже) действуют для обеих форм одинаково: `all` расширяет результат, а не разрешённый класс generator-ов. `collect` в `core-executable` ДОЛЖЕН: - быть range-restricted хотя бы одной положительной finite relation/domain; - иметь конечный evaluation domain; - не содержать `not_known`, `judgment`, `opaque` или side effects; - не зависеть циклически от consumer rule; - использовать `supported(P)` явно, если конфликтные positive supports намеренно должны входить в результат. **Дизъюнкция в generator-е (errata E-0219).** Generator — формула §207.1 с обычной status semantics, и `or` в нём допустим. Голый литерал generator-а есть `established(P)` (§207.1), поэтому generator — Boolean-комбинация status tests, и `established(A) or established(B)` выполнено ровно тогда, когда выполнена одна из ветвей. Исполнение приводит generator к дизъюнктивной нормальной форме по тому же правилу, что §206.1: дистрибуция `and` над `or` слева направо, операнды — в порядке канонического узла §207.1 (сортировка по semantic hash). Каждая ветвь решается как конъюнкция. Узел CLIR при этом не меняется: comprehension — терм, а не правило, и развёртка в отдельные узлы для него невозможна. - **Solution substitution** — назначение переменной comprehension и её binder-ов (поверх подстановки охватывающего правила). Подстановка, которую дают несколько ветвей, — одно решение: formula выполнена один раз, и `collect all` не удваивает элемент. Различать такие решения — работа binder-а, как и для одной ветви. - **§190 для каждой ветви.** Каждая ветвь обязана связывать переменную comprehension и все её binder-ы позитивным `established`/`supported`/ `monotone`-литералом. Ветвь, которая этого не делает, выводит правило из исполнимого подмножества (`NON_EXECUTABLE_RULE`). Без этого одна и та же подстановка различалась бы по составу связанных имён. - **Опоры элемента** — опоры каждой ветви, выполненной на этой подстановке, в порядке ветвей. - **Рёбра §110 и изъятие §111** — объединение чтений всех ветвей. Монотонный агрегатный гард E-0116 признаётся, когда условие на чтение выполнено в каждой ветви: объединение монотонно растущих множеств монотонно. `or` под `not` и внутри operand status test §65 этим правилом не затрагивается. Generator, у которого после развёртки остаётся конструкция вне исполнимого подмножества, выводит правило, в чьём теле, голове или `scope` стоит comprehension, из исполнения с `NON_EXECUTABLE_RULE` и причиной — он не роняет evaluation целиком. До errata обе реализации на `or` в generator-е отдавали вместо evaluation-документа error-объект `ValueError` на любой вопрос к программе, если правило входило в мир. Comprehension без доказуемой конечности допустима только в representation profile. CLIR представляет её отдельным `comprehension` term, а не скрытым external function. Quantifier semantics на **известном** finite domain стандартна: ```text forall x in empty_set satisfies P(x) == true exists x in empty_set where P(x) == false ``` Но unresolved/missing domain не считается empty set: результат `NEITHER + MISSING_INPUT`. Истинность `forall` по наблюдаемой коллекции сама по себе не является completeness certificate для maintenance duty. На непустом finite domain `forall` вычисляется как paraconsistent conjunction всех instantiated bodies, а `exists` — как paraconsistent disjunction. Поэтому один conflicted element может сделать aggregate formula `BOTH`; rule-body conservative default затем не считает её satisfied. Ошибка терма при вычислении generator-а — гард, вызов, арифметика (errata E-0118) — есть ошибка вычисления ВСЕГО comprehension-терма, а не «элемент не подошёл»: код §175, правило на подстановке не срабатывает, коллекция НЕ считается пустой. Адрес отказа — правило, в теле которого стоит comprehension; у запроса-коллекции §174.1 правила нет по построению, и адресом служит сам запрос, а `value` результата не пишется вовсе — пустая коллекция читалась бы как «таких значений нет», тогда как их не сосчитали. После E-0105 статус доезжает до ответа. До errata требование держалось только в теле правила: у запроса-коллекции ошибка уходила ВНЕ документа §208, и две реализации отвечали на неё по-разному — расхождение, невидимое differential-у, потому что сравнивать было нечего. ---