Skip to content
docs
Arxo ↗

Expressions and quantities: boundaries

For LLMs3 sections

What the construct does NOT do: limits, reserved values, neighbouring constructs and the selection rule.

  • Not mix kinds. No implicit conversions: neither Integer into Decimal, nor currencies with each other, nor Date into Instant. An offset-free instant is not a moment: comparing an offset spelling with an offset-free one is rejected — coercion needs a timezone/boundary policy and is not done silently.
  • Not round silently. An inexact Money/Quantity quotient and Money * Rational on a non-10-smooth total are a loud INEXACT_DIVISION, not quiet rounding. Rounding is only an explicit round / div_round policy.
  • Not multiply dimensioned by dimensioned. Money * Money, Quantity * Quantity are undefined (TYPE_ERROR): dimension algebra arrives with the unit package. The bridge between magnitude and money is rounding-policy territory.
  • Not divide without a claimant. The dividend tables are closed: a pair outside an operation’s table has no operation — TYPE_ERROR, operand order changes nothing. Quantity * Rational is unnamed: there is no witness in the corpus, extension awaits a claimant act. Quantity / Quantity does not divide under a div_round policy: it has no claimant act (only Money / Money divides under a policy).
  • Not hold 64-bit overflows silently. add, sub, mul(Integer, Integer), abs(Integer) and pow must lie in the signed 64-bit range: overflow is an evaluation error, with no wrapping or saturation. Decimals (Decimal, Money, Quantity) compute exactly; leaving the carrier range is a loud UNSUPPORTED_IN_SLICE, not silent rounding.
  • Not order enumerations. No order is defined over enum members: </<=/>/>= and min/max over members are TYPE_ERROR (“enum kind not ordered”), not declaration or name order. Members of different enumerations are incomparable — also TYPE_ERROR, not false.
  • Not execute average over Integer. Still rejected at execution; over Money it works.
  • Not tell empty: error from no policy apart in CLIR. The canon does not tell them apart: an aggregate node lowers without the options.empty key, byte for byte like a record without a policy.
  • The dividend, multiplicand, remainder, power and absolute tables are closed: they define the operation, not illustrate it.
  • mod — only Integer mod Integer, Euclidean remainder (0 <= r < |b|). pow — only Integer pow Integer, exponent 0..4096, 0 pow 0 = 1. An exponent < 0 is TYPE_ERROR.
  • There is no Rational literal: only Integer / Integer gives a fraction, canonized as an irreducible fraction with a positive denominator. Rational and Decimal mix in no operation.
  • The scalar rule holds for multiplication only: Integer/Decimal scale a magnitude, but Integer + Rational is TYPE_ERROR.
  • A money literal has a mandatory space (1000 KZT); a currency is a code, not a name.
  • Source-metadata jurisdiction/authority/issuer and judgment authority are not terms but institute StableIds: they need no declarations, checked by equality.
  • Expression vs judgment: a threshold in the body (n >= 10) is an expression over data; a disputable norm reading (“manifestly excessive”) is the judgment channel, not a comparison. See the selection table in README.md.
  • round vs div_round: rounding a finished value — round(v, p, mode); division with rounding — div_round(a, b, p, mode) as one operation over the exact quotient, not a composition of two.
  • collect vs collect all: counting entities — collect (Set, distinct values); summarizing charges — collect all (List, positions). The mistake is not diagnosed statically — only by a test on equal values.
  • const vs case fact: program immutables — const; mutable legal facts are not modelled with const — that is assert with origin. Case constants (case.constants) are ephemeral query values, not in the program hash.
  • function vs rule: pure value computation — function; concluding an assertion from premises — rule. Function before rule: every parameter read executes with a witness.
  • if-term vs unless: value choice by status — IfTerm (branches on TRUE_ONLY/FALSE_ONLY, BOTH — CONFLICTED_CONDITION, NEITHER — no branch picked); conclusion defeat — unless/defeater. A conditional term in the head and in the body is a support reader: a cycle through it is forbidden (LDC-E4102), a strict rule over a defeasible producer is declined (LDC-E4103).

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

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