From article text to norm — and where the language says "no"

Article 175 speaks not only of the right to benefit but of the date from which it is granted. This half of the article is more interesting than the first: it shows both how formalisation catches its own mistakes and where the core’s expressiveness ends.

Arxo Law

language "law.core" version "0.2";
package tutorial.kz.social version "0.2.0";
namespace "urn:law:tutorial:kz:social";

entity Actor;
entity Person : Actor;
entity DisabilityStatus;
entity Benefit;
entity BenefitApplication;

const DisabilityBenefit: Benefit = entity_ref("urn:law:tutorial:kz:social#DisabilityBenefit") {
    label ru-KZ official "Пособие по инвалидности";
};
const SurvivorBenefit: Benefit = entity_ref("urn:law:tutorial:kz:social#SurvivorBenefit") {
    label ru-KZ official "Пособие по случаю потери кормильца";
};

relation disability_established(person: Person, status: DisabilityStatus, from: Date) kind institutional;
relation entitled(person: Person, benefit: Benefit) kind institutional;
relation application_for(application: BenefitApplication, person: Person, benefit: Benefit) kind empirical;
relation application_registered(application: BenefitApplication, day: Date) kind institutional;
relation benefit_start_date(person: Person, benefit: Benefit, day: Date) kind institutional;
relation beneficiary_choice(person: Person, benefit: Benefit) kind institutional;

The labels read: “Disability benefit” and “Survivor benefit”.

A bound variable instead of a pseudo-function

The first draft of this norm held any_status(person) in its body — “disability established with some group”. It looks like a function and reads like a function, but there is no such function in the language: any_status was declared nowhere. The formaliser wrote an intention, not a norm.

The correct record is a bound variable: declare status in for and use it in the body. Existential quantification is expressed by the variable being bound and needed nowhere else.

Right there a second find surfaced: the head predicate benefit_start_date was not declared at all. Both finds were caught by the compiler, not by reading.

Arxo Law

@source("KZ-SOCIAL-CODE-224-VII-ART-175")
rule DisabilityBenefitStart strict {
    label ru-KZ official "Статья 175. Дата назначения пособия по инвалидности";
    for person: Person;
    for status: DisabilityStatus;
    for from: Date;
    for application: BenefitApplication;
    for registered: Date;
    when entitled(person, DisabilityBenefit)
        and disability_established(person, status, from)
        and application_for(application, person, DisabilityBenefit)
        and application_registered(application, registered);
    then benefit_start_date(person, DisabilityBenefit, max(from, registered));
}

The rule label reads: “Article 175. The grant date of disability benefit”.

Note that the body rests on entitled(person, DisabilityBenefit) — the head of the norm from the previous tutorial. Norms chain through predicates, not through references to each other: law knows nothing of law; it knows of facts.

Where the language says “no”

The real article grants the benefit not from the application registration date but no earlier than three months before it. That is, the norm head should read max(from, registered - 3 calendar_month).

So it is written in the worked example. And that file fails the compiler check:

Output

error LDC-E2108: «-»: несовместимые виды Date и Quantity — §58 требует
совпадения видов для сложения и вычитания; правило скаляра §49 действует
ТОЛЬКО для умножения (§48: неявных конверсий нет)

The diagnostic reads: “‘-’: incompatible kinds Date and Quantity — kinds must match for addition and subtraction; the scalar rule applies ONLY to multiplication (no implicit conversions)”.

Replace max(from, registered) with max(from, registered - 3 calendar_month) in the norm above and you get exactly this diagnostic with the LDC-E2108 code: the lesson is checked, not told.

This is not a defect of the example. The core’s computable surface is closed deliberately: subtraction requires kinds to match, while “three calendar months” is not a duration in the same sense in which a date is a point. A month is not a fixed number of days; “minus three months” from 31 March needs a policy that the core lacks and that must not be chosen silently.

Hence three honest exits, none of which is to add a conversion:

1. The date arrives in the case. The threshold date is computed outside the core and fed as a fact — then whoever chose the rounding policy answers for it, visibly in the case.
2. The norm is expressed as a table. Layer A3 (temporal parameters, decision tables) describes such terms as data, not as arithmetic in a rule head.
3. A language change. If the core needs calendar arithmetic, that is a semantic change, and it goes the full circle: prose, schema, and both implementations. “Simply allowing subtraction” is not an option, because then the month-boundary policy would turn silent.

The worked example keeps the inexpressible form on purpose: it shows the article as it is, and thereby marks the boundary. The boundary is worth seeing before you write forty norms and hit it on the forty-first.

Restriction: law requires, not derives

The last part of article 175 says: two benefits are not granted at once; the recipient chooses one. This is not an inference rule — nothing follows from it. It is a requirement on the case.

Arxo Law

@source("KZ-SOCIAL-CODE-224-VII-ART-175")
constraint OneBenefitByChoice {
    label ru-KZ official "Статья 175. Одно из двух пособий по выбору получателя";
    for person: Person;
    scope true;
    when entitled(person, DisabilityBenefit) and entitled(person, SurvivorBenefit);
    require beneficiary_choice(person, DisabilityBenefit) or beneficiary_choice(person, SurvivorBenefit);
    severity error;
    message "One of the two concurrent benefits must be selected by the beneficiary.";
}

The constraint label reads: “Article 175. One of the two benefits at the recipient’s choice”.

The difference from a rule is fundamental. A rule written in this place would choose the benefit for the recipient — by order, by size, by alphabet — and the choice would stay invisible. A constraint does not choose: it records that a case without a choice is incomplete, and names the culprit in the words of message.

A rule says “hence follows”. A constraint says “so it must not be”. Confusing them is the cheapest way to teach a system to take decisions it is not authorised to take.

Next

The norm is tied to the text by an anchor, but the text bytes have not yet been presented to the core. The tutorial on pinning an edition is about how the official text is placed next to the package and verified by hash on every build.

The exercise for this page is /tutorials/exercise-real-article-rules/.