日本語 · English（未訳）

ADR-36: 結合子・軸所属の粒度整合——整列の静的検査

判断: 点の等値で所属を判定する演算——結合子 &・\（および | の一部規則）と軸所属 （filter(on:)・roll(on:)・shift(unit: 点列軸)・stride(n)）——に、整列（alignment）の静的 検査を規定する（F56。F54 の詳細規則と ADR-33 判断 10 の残点＝tz 等値の時期もここで確定する）。

  1. 意味論は変えない: 点の同一性は chronos 上の等値（ADR-33 判断 7）であり、結合子は点集合の 演算のまま。本 ADR が足すのは統治（どの二流の突合を正当と認めるか）だけである。 整列は式の導出構造に付く保守近似であり、同じ外延を表す二式で検査の可否が割れうる （snapTo の明示でいつでも合流できる）——外延の意味論は不変。従来この検査が無かった下で 合法（だが黙って空振り）だった式は静的エラーに変わる: 挙動が変わるのは誤結果だけだが、 破壊的変更として記録する（ADR-16 の基準では欠陥の修正）。「正当な空」（ADR-15）とは別物—— 同一整列の突合が空になるのは従来どおり正当な値である。

  2. 整列とは: 時間ストリームの静的性質で、「全点が、ある原子グリッド G の目盛り点上にある」 という主張。G の正体は三つ組——幅（1d 等）・正規化位相（既定整列・anchor:・紀元を幅を 法として正規化した値。判断 3）・tz 名（市民時幅のとき。経過時間幅は位相が幾何を全て持つので tz を持たない）。整列の値は G か「なし」の二値で、式の導出構造から静的に計算される:

    窓語の要素グリッドとは、その窓連鎖の原子 grid を指す（month・year・quarter・week なら day の grid——span/split は要素グリッドを保存して窓を組むため、公開窓語由来のストリームの点は 常に原子 grid の目盛り上にある）。segmentBy 由来の窓の「要素グリッド」はマーカーの整列で読む （窓の切れ目＝マーカー点。snap 済みマーカーなら原子 grid と一致し、未 snap の瞬間マーカーなら 「なし」——snapTo(その窓) が原子 grid を主張しない安全側になる）。 単点の日付リテラルは表の対象外＝主張なし（単発の除外は [2026-01-05] とテーブルで書く。保守近似・ 意味論不変）。

    式の形 整列
    everyDay・公開窓語由来のストリーム（month \|> first 等） 要素グリッド（Gregorian なら day = chronos grid 1d の正体）
    テーブルリテラル（全要素が日付のみの字句） 市民日グリッド。tz 成分＝そのリテラルの錨打ちに実際に使われた tz（ADR-33 判断 8 の在圏解決と同一物——タグと点の幾何を乖離させない。実体・データ premise は tz: 必須＋member 解決規則〈ADR-35 判断 8〉により定義側の tz に収束する）
    テーブルリテラル（時刻付き要素、または字句でない要素〈計算値・名前参照〉を含む） なし
    strideBy(w, from: p) 由来（everyInstant の実体化を含む） anchor 付きグリッド（幅 w・anchor p）——出力は定義上この目盛りそのものであり、「なし」に落とすと G の体系と不整合になる
    filter（両形）・選択子・within・segmentBy・stride 入力の整列を保存
    roll(conv, on: A) 軸 A の整列（出力点は A 上の点）
    shift(n, unit: 窓語 U) 入力整列＝U の要素グリッドなら保存、さもなくば なし（検査なし・下記）
    shift(n, unit: 点列軸 A) 判断 3 の検査に合格した共通 G（＝軸 A の整列。roll と対）
    snapTo(w) w の要素グリッドを主張（＝再整列の明示手段。判断 5）
    A \| B 両辺同一ならそれ、さもなくば なし（判断 4）
    A & B・A \ B 共通整列（判断 3 で同一が保証される）

    「窓語」と「点列軸」の区別は値の種別で決まる（規準は既存の意味論のまま）: 軸位置の名前が 窓（パーティション）に解決されれば窓語（shift は窓の添字移動＋窓内オフセット保存）、 時間ストリーム（点列）に解決されれば点列軸（shift は軸上の歩進——軸外の点はエラー）。

    糖衣は core への展開後（機械的差し込み・ADR-23）・実引数の束縛後に計算する——仮引数 （businessDays(on: p) = filter(on: p) の p）は定義体単独では不定だがエラーにせず、呼び出しごとに 展開先で判定する。premise 束縛越し（実体の nonWorking 等）は定義側の文脈で計算した整列がそのまま 運ばれる。整列の tz 名成分は遅延解決の解決後に確定する（day = chronos grid 1d の tz は利用側 前文で決まる——wkst と同型・ADR-17）。ゆえに「静的」とは前文・名前解決の後、データ評価の前の 層を指す（在圏 premise の実体化ごとに検査が走る）。

  3. 検査: &・\・filter(on:)・roll(on:)・shift(unit: 点列軸) は、両辺（入力と軸）の整列が 「同一の G」であることを要求する。どちらかが「なし」でも、G 不一致でも静的エラー。 shift の検査は unit が点列軸（軸ストリーム）のときに限る——窓語 unit（shift(+87, unit: day)）は 等値所属でなく区間所属（属する窓の添字を動かし窓内オフセットを保存）なので判断 7 の免除系に 準じ、整列なしの入力も合法（節気の瞬間を +87 日して八十八夜を得る確定例がこの形）。 stride(n) の軸相対カウント（在圏 axis:・on: 上書き）も同じ検査を受ける——数える単位（軸）と 数えられる列（入力）の整列がずれると「3 営業日ごと」が黙って別の間隔にずれるためである。 細分・包含による自動整合はしない——「時刻付き列と日次列は hour で見れば揃っている」式の 緩い判定を許すと、意図の単位（日）での突合が黙って空振りする反例（後述）が通ってしまう。

    G の同一＝幅の同一・正規化位相の同一・（市民時幅なら）tz 名の等値。位相は anchor・紀元を 幅を法として正規化して比べる——経過時間幅は「anchor（無ければ紀元。epoch: 上書きを含める）の chronos 点 mod 幅」、市民時幅は「anchor の属する市民日の序数 mod 日数幅」と「anchor の日内 オフセット（壁時計）」の組。既定整列の日内オフセットは 0 なので、時刻付き anchor のグリッド （毎日 09:00 級）は既定の day と別 G になる——日内オフセットを落とすと「毎日 09:00 と everyDay の &」が同一判定で素通りし黙って空になる（検査が防ぐはずの形）。既定整列は正規位相の一値として同じ土俵で比較される（市民時幅＝真夜中位相・ 経過時間幅＝紀元位相）——chronos grid 1d anchor: 2026-01-01 と既定整列の day は同一 G （目盛りは点集合として同じ）。anchor の chronos 点そのものの等値を要求する案は、等価なグリッド 同士（anchor が幅の整数倍だけ違う定義）を安全側エラーで割るため採らない。紀元を落とす案は、 epoch: の異なる premise 間の同幅グリッドを同一と誤判定し、検査が防ぐはずの空振りを検査自身が 通すため採らない。premise を跨いでも成立する（同じ Gregorian 系の day・同じ tz 名なら別 premise 由来でも同一）。F54（実体と利用側の tz 不一致）は tz 名の不一致としてここで検出される。 図解（2026-07-13 追補・判断 2〜5 の全体像——判断内容の変更なし。spec §4.5 と同図）:

    flowchart TD
  OP["S₁ ⊕ S₂（⊕ ＝ &・差・filter(on:)・roll(on:)・shift(unit: 点列軸)）"]
  OP --> Q{"G(S₁) ＝ G(S₂) ?<br/>（幅・正規化位相・tz 名の三つ組＝判断 2/3）"}
  Q -- "はい" --> OK["合成 OK——結果も同じ G 上"]
  Q -- "いいえ・どちらかが「なし」" --> ERR["静的エラー（黙った空振りの封止）<br/>誘導: snapTo(w)＝明示の再整列（判断 5）・rebase＝ラベル対応（ADR-40）<br/>同じ所属なら coincides（ADR-38）"]
  UNION["S₁ | S₂（和）"] --> FREE["検査なし——混合スケジュールの保護（判断 4）"]
  4. 和 \| は整列不問。点は足されるだけで「黙って空振り」の危険が無く、混合スケジュール （「毎営業日と、3/3 の 15:30 の単発」）は発報列の正当な形である。混合の出力は整列「なし」となり、 後段で &/\ 等に流せばそこで検査に掛かる（安全網は保たれる）。
  5. 再整列は snapTo で明示する。snapTo(w) は「点→属する w 窓の先頭点」の点変換（ADR-30）で あり、出力は構成的に w の要素グリッドに整列する——既に整列している点には恒等で、整列主張の 付け替えだけが起きる。これが ADR-30 の点変換としての意味に加わる第二の役割（F22 で segmentBy の 所属規約が「snapTo で粒度をそろえる」と定めたのと同じ形が、結合子側の規則になった）。
  6. tz 名の等値はリテラル文字列の等値（ADR-33 判断 10 の残点の確定）: リンク解決の前・正規化 なしで比較する。"UTC" と "Etc/UTC"、"Asia/Tokyo" と "+09:00" は不一致＝安全側エラー。 リンク表（tzdb の Link）も版相対であり、判断の趣旨（版非依存）からはリテラル等値だけが安定する。 同名 tz の版差（premise ごとに tzdb の版が違う場合の市民日境界のずれ）は名前等値の残余リスク として ADR-33 判断 10 が引き受け済み（本検査の射程外——実装系は単一 tzdb 版を既定とする）。 固定オフセット表記の正準形が字句で一意でないと "+09:00"/"+9:00" 級の別綴りが安全側エラーを 量産する——F66(b) の確定時に正準形を一意化する（依存を F66 に追記）。
  7. 検査の対象外: 区間所属（containment）で判定する演算——within・snapTo・ ordinalIn/epochOrdinal・cycle 射影——は、窓が全域を覆う（I5）ため粒度不一致で黙る形が無い。 segmentBy のマーカーも対象外だが、根拠が異なる——所属は F22 の代表点規約として定義済みで、 マーカーの粒度（瞬間で切るか、snapTo(day) で日境界へ落として切るか）は朔日規約のような意味の 選択であり、どちらでも窓は全域を覆い黙って消える点が無い（stdlib の Kyureki は「朔を含む日から」の 規約を snapTo(day) で明示する側の実例）。ラベル付きテーブルの束縛名射影（sekki(d)）は点の 等値所属だが、外れたら硬エラー（ADR-30）で黙らないため対象外。ただし並行値リストの添字読み （monthNos[epochOrdinal(…)]）に同長性検査が無い穴（F62）は本 ADR の射程外として残る—— 「等値所属は黙らない」をこの形へ過大に一般化しない。
  8. 整列なし同士の &/\ も不許可（判断 3 の帰結の明文化）。瞬間レベルの exact-match 突合を 意図するときの合法形は、細かい原子 grid への明示の再整列——sec = chronos grid 1s 級の窓語を premise に立てて両辺を snapTo(sec) する（分・秒精度のデータには恒等＝主張の付け替えだけが起きる。 判断 5）。新機構は要らない。

背景: §1.19 のレビュー（2026-07-07・F56）で「結合子は点集合の演算として定義され、粒度のそろわない 二流の演算（everyDay \ 瞬間列）の規定が無い——点が一致しなければ黙って空振り＝サイレント誤結果 （ADR-16 の危険基準）」と指摘された。F22（segmentBy の所属規約）と同形の問題の結合子版であり、 F52 の裁定（細粒度も射程内）と F54（tz 不一致の空振り）がどちらも「点の一致規則」に合流する。 土台は ADR-33 が確定した（点の同一性＝chronos 等値・tz の同値＝名前等値）。

検査の合格条件を「同一の G」（細分不可）に置く決め手になったのは次の反例である。hour = chronos grid 1h を持つ premise（Gregorian は hour を持たないのでユーザー定義の原子）で、日次列（整列＝ 1d）と「毎日 9 時」の列（shift(9, unit: hour) の出力。点は毎日 09:00）の & を考える——書き手の 意図は「月曜の 9 時」のような日単位の突合だが、chronos 等値の交叉は 00:00 と 09:00 が一致せず空に なる。ここで「両辺の点はどちらも 1h の目盛り上にはある」（日次の点は時の目盛りにも乗る——事実と しては真）という細分の論法を合格条件に許すと、この空振りが検査を通ってしまう。細分の事実は整列の 推論（判断 2）が使ってよいが、検査の合格条件（判断 3）には使えない——これが「同一の G」の 根拠である。

却下した案:

帰結:

改訂（2026-07-08・ADR-38）: 二点を改める。(1) 判断 3 の検査リストから stride(n) を削除—— stride は入力相対に確定し（F70・ADR-38 判断 10）軸を読まないため突合が無い（軸との整列は前段の filter(on:) が検査する）。帰結の「stride 検査は未実装＝制約に明記」も解消（検査自体が不要になった）。 (2) 判断 7 の免除系（区間所属）に窓所属述語 coincides(S, w, d)（仮称・ADR-38）を追加—— 等値でなく所属で結合する明示手段であり、F68 の解。ただし免除は無条件ではない: S の整列が市民時 グリッドで w の要素グリッドと tz 名不一致なら静的エラー（ADR-38 判断 5——本 ADR 判断 6 が等値側で 止めていたクロス tz の黙った 1 日ずれを、免除系の裏口から再開させない）。coincides は chronos 所属で あり「同じ日付ラベル」の所属ではない（そちらは F69 の再錨の領分のまま）。あわせて判断 3 の エラーメッセージに分岐案内を足す——「同じ点が欲しいなら snapTo で整合・同じ所属（日）が 欲しいなら coincides」（等値差を coincides に書き換える逆方向の迂回は悪化——ADR-38 判断 8）。

改訂 2（2026-07-08・ADR-40）: 判断 7 の免除系にも tz 名の検査を敷く——rebase（ADR-40）が クロス tz 整列のストリームを常態化させると、免除系（within・ordinalIn・選択子・cycle/値射影）は tz を見ないため「ラベル 1 日ずれの束ね・曜日読み」が黙って通る（東京 3/1 の日先頭を NY premise の within(month) に流すと 2 月窓へ）。市民グリッド入力 × 窓要素グリッドの tz 名不一致は静的エラー （幅・位相は不問のまま＝区間所属の免除は維持・tz だけは日付座標系そのもの——ADR-38 判断 5 の coincides 検査の一般化。既存の潜在穴でもある）。snapTo は除外（chronos 所属が文書化済みの意味）。

改訂 3（2026-07-13・ADR-45）: 整列の値に第三状態「空虚適合」を追加——空テーブル （[] covering: …・ADR-45）は点を持たず、どの整列にも違反し得ないため、判断 2 の「G か『なし』の 二値」を三値に拡張する。空虚適合は判断 3 の検査に通り（相手が「なし」でも通す——「なし」＝ 主張できない・検査に落ちる、との対比）、判断 4 の和および &/\ の出力整列は相手側を継承、 保存系の段（filter・選択子・shift 窓語・roll・snapTo・rebase）は空虚適合を保存する。判断 7 の 免除系 tz 名検査（改訂 2）は市民グリッド同士の規定のため空虚適合には掛からない。詳細は ADR-45。

This site is open source. Improve this page.