Expressions and quantities: boundaries
For LLMs3 sections
What the construct does NOT do: limits, reserved values, neighbouring constructs and the selection rule.
Does not do
Section titled “Does not do”- Not mix kinds. No implicit conversions: neither
IntegerintoDecimal, nor currencies with each other, norDateintoInstant. 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/Quantityquotient andMoney * Rationalon a non-10-smooth total are a loudINEXACT_DIVISION, not quiet rounding. Rounding is only an explicitround/div_roundpolicy. - Not multiply dimensioned by dimensioned.
Money * Money,Quantity * Quantityare 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 * Rationalis unnamed: there is no witness in the corpus, extension awaits a claimant act.Quantity / Quantitydoes not divide under adiv_roundpolicy: it has no claimant act (onlyMoney / Moneydivides under a policy). - Not hold 64-bit overflows silently.
add,sub,mul(Integer, Integer),abs(Integer)andpowmust 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 loudUNSUPPORTED_IN_SLICE, not silent rounding. - Not order enumerations. No order is defined over enum members:
</<=/>/>=andmin/maxover members areTYPE_ERROR(“enum kind not ordered”), not declaration or name order. Members of different enumerations are incomparable — alsoTYPE_ERROR, not false. - Not execute
averageoverInteger. Still rejected at execution; overMoneyit works. - Not tell
empty: errorfrom no policy apart in CLIR. The canon does not tell them apart: anaggregatenode lowers without theoptions.emptykey, byte for byte like a record without a policy.
Reserved and closed
Section titled “Reserved and closed”- The dividend, multiplicand, remainder, power and absolute tables are closed: they define the operation, not illustrate it.
mod— onlyInteger mod Integer, Euclidean remainder (0 <= r < |b|).pow— onlyInteger pow Integer, exponent0..4096,0 pow 0 = 1. An exponent< 0isTYPE_ERROR.- There is no
Rationalliteral: onlyInteger / Integergives a fraction, canonized as an irreducible fraction with a positive denominator.RationalandDecimalmix in no operation. - The scalar rule holds for multiplication only:
Integer/Decimalscale a magnitude, butInteger + RationalisTYPE_ERROR. - A money literal has a mandatory space (
1000 KZT); a currency is a code, not a name. - Source-metadata
jurisdiction/authority/issuerand judgmentauthorityare not terms but institute StableIds: they need no declarations, checked by equality.
Neighbours and the selection rule
Section titled “Neighbours and the selection rule”- 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 inREADME.md. roundvsdiv_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.collectvscollect 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.constvs case fact: program immutables —const; mutable legal facts are not modelled withconst— that isassertwithorigin. Case constants (case.constants) are ephemeral query values, not in the program hash.functionvsrule: pure value computation —function; concluding an assertion from premises —rule. Function before rule: every parameter read executes with a witness.if-term vsunless: value choice by status —IfTerm(branches onTRUE_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.