日本語 · English（未訳）

ADR-38: 窓所属の述語（coincides・仮称）と stride の入力相対

判断: ADR-36（整列）が顕在化させた「所属の意味論の縁」二つを確定する（F68・F70。 draft §1.21 の候補設計＝3 視点検証・設計者裁定 2 件（2026-07-08）を経た ADR 化）。

A. 窓所属の述語（F68）

  1. 受け皿は値関数一語——新しい結合子でも専用段でもなく、射影一族（ADR-27/30・§4.9）に足す:

    coincides(S, w, d)    # 仮称。点 d の属する w 窓の中に、ストリーム S の点が少なくとも一つ在るか（論理値）

    F68 の正準形は filter との合成——notices |> filter(t => not coincides(closures, day, t)) （毎営業日 9 時の通知から臨時休業「日」を除く。発火時刻 09:00 を保存する）。積の形も同じ一語 （filter(d => coincides(S, day, d))）——差と積が not の有無で書き分けられる。

  2. 理由の核は合成力と一族整合。値述語なので not・and/or・他の射影と自由に組める（専用の 結合子・段はこの合成を全部引数化する羽目になる）。ordinalIn(u, w, d) が「属する窓の中で 数える」なら coincides(S, w, d) は「属する窓の中に在るか」——点→属する窓→窓の中身、 という §4.9 の同じ骨格で、値式に有界存在量化が入る。純増の表現力（コーパス掃引で確認）: 閏月の検出（lunarMonth |> first |> filter(p => not coincides(chuki, lunarMonth, p))——monthNos 手作業更新〈F62〉の照合検査を兼ねる）・ティティ欠日（kshaya）の列挙・朔×節気の同日競合の 時刻保存検出・瞬間列テーブル（潮汐級）への営業日絞り（不規則時刻には前段差の回避形が存在しない）。

  3. 引数の解決と型: w は在圏で解決される窓語（パーティション型・segmentBy 窓とも可。cycle 名は 不可＝軸に立てない ADR-21 と同じ禁止）。S は時間ストリームに解決される式（束縛名・修飾名・括弧の インライン式。解決は軸位置と同一規則の準用＝有効点ストリームへ。ADR-35 判断 4 の premise 名 読み替えは適用しない——標準導出は bizDay の名で書ける）。窓語を S に置くのは静的エラー （原子点列への暗黙降格は恒真化の罠。点列を意図するなら month |> first を書く）。

  4. 確定は証人規則の三分岐（敵対検証で確定・安全側）:
    • (i) d の w 窓内に非註釈区間の S の点（＝証人）が在る → 真（∃ は単調——証人の存在は 未知データに依存しない。註釈不要）。
    • (ii) 証人なし かつ 窓 ∩ S の註釈区間 ≠ ∅ → 範囲外（ADR-37 判断 6。ストリーム文脈は落として 註釈・純値文脈は明示エラー）。窓内で見つかった点が註釈区間内なら証人にならない—— everyDay \ holidays の退化尾部の点を証人にすると「存在しないかもしれない祝日の上の確信付きの 真」になる（「黙って違う結果」の再生産）。
    • (iii) 窓が完全に実効被覆域内 → 偽。 基準は常に実効被覆域（輸送済み註釈区間の補集合）であり生 covering ではない（ADR-37 判断 6 と 同じ据え方）。真は部分読みで単調確定・偽は覆域完全性に依存する非対称が規範。

    図解（2026-07-13 追補・判断 4 の三分岐——判断内容の変更なし。spec §4.9 と同図）:

    flowchart TD
  Q["coincides(S, w, d)——d の属する w 窓に S の点は在るか"]
  Q --> W{"窓内に非註釈区間の<br/>S の点（＝証人）が在る？"}
  W -- "在る" --> T["真——∃ は単調。証人の存在は<br/>未知データに依存しない（註釈不要）"]
  W -- "無い" --> C{"窓が S の註釈区間に交差する？"}
  C -- "する" --> O["範囲外——filter では点を落として註釈<br/>（読んだ窓の全域へ拡幅＝判断 7・F75）"]
  C -- "しない（窓が実効被覆域内）" --> F["偽——偽の確定は覆域の完全性に依存<br/>（真との非対称が規範）"]

  5. tz の静的検査: S の整列が市民時グリッド（tz 名つき）で、w の要素グリッドの tz 名と不一致なら 静的エラー（幅・位相は不問＝所属だから細分は許す。tz だけは日付座標系そのもの——等値の \ で ADR-36 判断 6 が止めていたクロス tz の黙った 1 日ずれ〈F54 級〉を、免除系の裏口から再開させない）。 S の整列「なし」（時刻付き・混合）は検査不能——coincides は chronos 所属であり「同じ日付 ラベル」ではない（クロス tz の日付ラベル所属は F69 の再錨の領分）。

  6. 整列要求（同一 G）は課さない——所属は区間所属であり ADR-36 判断 7 の免除系に加える（改訂）。 d が w のどの窓にも属さない場合は ADR-37 の分類器（判断 6 の失敗種列挙に「coincides の 窓所属」を追記＝改訂）。I7: d の窓は有限区間で S をその区間だけ読む（オンライン）。I8: フィルタ層の カレンダー依存＝合法。

  7. filter 輸送行の精密化（ADR-37 判断 4 の改訂）: 述語が読むのは d 自身でなく d の窓の全域なので、 輸送は「述語が読んだ領域（窓）の逆像へ拡幅」と一般化する（選択子行と同型）。これは coincides 固有で なく、データ由来窓越しの ordinalIn を述語に使う既存形にも潜在していた過小近似の穴（F75）—— coincides が強制事例になった。

  8. 使い分けの整備が導入とセット: day 整列同士の例外日は従来どおり結合子（schedule \ blackoutDays）が 正で、coincides への書き換えは悪化（整列検査の合法な迂回路を育てる）。規範は「同じ点なら 結合子〈不整列は snapTo で整合〉・同じ所属（日）なら coincides」——ADR-36 の整列エラーの文言と reference（combinators/filter/snapTo/coincides）にこの分岐案内を載せる。導出型 （(bizDay \ closures) |> shift(+9, unit: hour) で書ける形）も前段差が簡明で、coincides の必然は テーブル直書き・混合・不規則時刻に絞られる。

  9. 糖衣は今回導入しない: except(B, within: day) 級の段は頻出が確認できたら標準糖衣（F1 の器）で 足す——core の最小性（ADR-23）と「還元で書けるものに専用記法なし」（ADR-27）を優先。 名は仮称（coincides。ほか hits〈読みやすい〉・anyIn〈所属述語 in と近接——利点にも混同の 芽にもなる〉・sharesWindow を比較候補に記録。引数順は ordinalIn(u, w, d) と同型の 〈対象, 窓, 点〉——ただし第 1 引数の型が一族で唯一ストリームである点は §4.9 の表で明示）。

B. stride は入力相対（F70）

  1. stride(n, from:) は入力ストリームの点を数える。軸引数を持たない——§1.9 の「在圏 axis: （on: で上書き）」は削除（表面の削減。コーパスの使用例は全て入力相対・on: 上書きの使用例ゼロ・ reference と impl も入力相対。F32 の sekkiInstants |> stride(2, from:) は入力相対でのみ意味を 成す実例）。「3 営業日ごと」の正準形は先に filter——everyDay |> filter(on: bizDay) |> stride(3, from: …)。何を数えるかは前段が決める。

  2. from: の規約: 「from: 以上の最初の入力点が数え起点（第 0 歩＝残る）」。from: が入力の点で あることは要求しない（位相の取り違えは F32 で踏んだ危険域——規約を正本に置く）。

  3. n の域: 1 以上の整数。さもなくば静的エラー（従来の実装は stride(0) が剰余の JS 意味論で 黙って空になる——根絶対象の故障クラス。F70 と独立にも直す価値のある検証の発見）。

  4. ADR-36 の stride 整列検査は削除（ADR-36 判断 3 の改訂）: stride は入力しか読まないので突合が 無い。軸との整列は filter(on:) の段が既に検査している。傍証: ADR-37 判断 4 の stride 輸送行 （歩行の交差）も入力相対を暗黙前提に書かれ実装・テスト済み。呼称「軸相対カウント」は 「入力カウント」へ（strideBy との対は「点で数える／幅で刻む」）。

  5. 二判断はセット: 軸で数えて入力へ当てる形は (axis の stride 列) & input〈day 整列〉または filter(d => coincides(stride 列, day, d))〈時刻付き〉で常に合成可能——後者は判断 A に依存する。

背景: F68＝時刻付き・混合スケジュールへの例外日適用が等値の結合子では書けない（snapTo は発火 時刻を潰す・従来は黙って空振り・ADR-36 で安全側の静的エラーに顕在化）。F70＝stride の数え方の二義 （§1.9 の字面は軸相対・文書と実装は入力相対）。candidate 設計（draft §1.21）を 3 視点並列の検証 （整合性・コーパス全数掃引・敵対＋実装）に掛け、証人規則・tz 検査・S/w の型の縁・filter 輸送の 逆像拡幅（F75）・stride の n 域と from: 規約を精密化した上で、設計者裁定 2 件（受け皿＝値述語一語・ 入力相対＝いずれも推奨案）で確定した。

却下した案:

帰結:

改訂（2026-07-09・ADR-41 帰結＝F76 の解消）: 判断 8 の正準例「毎営業日 9 時」 （bizDay |> shift(+9, unit: hour)）は経過時間側の書き方であり、「日の開始から 9 経過時間」で あって壁時計の 09:00 ではない（DST 切替日に割れる——切替日が営業日に落ちる tz・週末構成では 壁 10:00 に着地。40-examples/06 で実測＝F76）。営業時間は壁時計概念なので、正準は宣言側へ 差し替える——実体が 9:00 開場を宣言していれば bizOpen（ADR-41 の標準導出）、開場と無関係な 時刻は壁時計 tick（時刻付き anchor の grid〈ADR-31 改訂 2〉か strideBy(1d, from: …T09:00)）＋ coincides(bizDay, day, t)。経過形は「n 経過時間後」が意図のときの明示形として残る（reference の 当該例は差し替え・但し書きを追記）。coincides 本体の意味論（判断 1〜7）は不変。

改訂 2（2026-07-09・純命名の確定＝F51）

This site is open source. Improve this page.