日本語 · English（未訳）

ADR-39: 窓列への並行ラベル列——labels: の一般化と同長性検査

判断: 並行値リストと窓列の結び（F62）の器を次のとおり確定する（draft §1.22 の候補設計＝ 2 視点検証・設計者裁定 2 件（2026-07-08）を経た ADR 化）。

1. 受け皿はテーブルの labels:（ADR-30・確定語）の窓列への一般化——新しい語はゼロ:

   lunarMonth = day |> segmentBy(lunarStart, edges: drop, empties: error, labels: monthNos)
   

   読みは束縛名射影（ADR-30/34 と同じ規則）: lunarMonth(d) が点 d の属する窓のラベル（月番号）を 返す。従来イディオム monthNos[epochOrdinal(lunarMonth, d)] の別名束縛は不要になる。窓もラベルを 格納しない（ADR-30 の原理の窓版——窓列は区間のみ・ラベルは束縛に付く射影の定義データ）。これで 三つのラベル源の対称が完成する: テーブル＋labels:＝点のデータラベル（ADR-30）・窓＋label: ラムダ＝窓の規則ラベル（ADR-34）・窓＋labels: リスト＝窓のデータラベル（本 ADR）。cycle （無限律動）を含め、読みは一様に 束縛名(d)。ラベル値の型域は ADR-34 判断 3 と同一（スカラー値・ 等質のリスト・リテラルまたはリスト束縛名。空リストは不可）。

2. 同長性検査が F62 の器: リスト長 == 窓数。窓数は覆域基準で数える——実効被覆域内の マーカー起点の窓数（＝マーカー数。ADR-37 の覆域端確定の最終窓を含む。kyureki なら 38）。評価範囲や 実体化範囲に依存しないので、検査は近似でなく正確に立つ。ずれは期待/実際つきのエラー。 検査の時点は窓束縛の評価（実効被覆域の確定）と同時——射影が起きるかに依らず走る（ADR-34 の label: 射影時遅延とは干渉しない: 長さ検査はラベル値を評価しない）。with 派生でマーカーや リストを上書きすれば premise 実体化ごとに再走（ADR-36 の検査層の準用）。

3. 整列は専用の窓列序数——意味論は定義的等式一行 名前(d) ≡ labels[窓列序数(d の属する窓)]。 窓列序数は実効被覆域内の先頭マーカー起点の窓が 0。epochOrdinal（F60）とはマーカー列が紀元に 届かない場合に一致するが、紀元を跨ぐ歴史データでは epochOrdinal が負になるのに対し窓列序数は常に 0 起点——相乗りしない（検証で確定した分離）。

4. 前提条件と締め（整列を崩す形はすべて静的エラー・裁定確定）:
   • マーカー点列は有限（導出構造で静的判定——テーブル由来は有限・生成子由来は無限。ADR-36 の 整列計算と同型の保守近似）。規則マーカーの segmentBy（stdlib の week・isoWeek）は静的エラー ——無限の窓列は有限リストで覆えない。エラー文言が正しい形へ誘導する: 周期ラベルは cycle・ 計算番号は ordinalIn か label: ラムダ。開端 covering（covering: ..）の有限列テーブルは 合法（覆域は無限でも点列は有限・最終窓の幅が無限になるだけ）。
   • マーカー流の実効被覆域は全マーカー点を包む単一の無註釈区間であること。合成マーカー （t1 | t2）の註釈域には未知のマーカーがあり得て窓数が確定しない（先頭側が註釈なら窓 0 自体が 不定）——確定しないときは安全側エラー（ADR-37 判断 6 細則と同じ据え方。合成には束縛後置の 被覆主張で覆域を確定してから）。
   • edges: clip と組めない——擬似窓（マーカー起点でない窓）が窓列序数とリスト添字の対応を 黙ってずらす。ティティ（40-examples 05 §5.1）の現行 clip 形は「頭擬似窓が番号 0 を占める偶然」に 依存しており、edges: drop＋labels: [1, 2, 3, 4, 5, 6, 7] で期待値不変に移行できることを 検証済み（偶然依存の除去を兼ねる。数値の範囲略記は list-elem に無い——範囲リテラル a..b は 日付専用）。真に clip 窓のラベルが要る実例が出たら再訪。
   • empties: drop と組めない——空窓の除去は序数を詰め、どのラベルが落ちたか判別できない。 empties: keep の空窓はラベル対象——空窓のラベルの読み口は区間所属なので窓区間内の任意の点、 実用上はマーカー点そのもの（tithiB |> filter(t => tithiW(t) == 6)＝欠ティティの番号が立つ）。
   • label: ラムダとの同居は静的エラー（ラベル源の二重化＝束縛名射影の一意性。ADR-34 が cycle×label: を締めたのと同じ面）。cycle・grid/span/split への labels: も静的エラー。あわせて 未知の名前付き引数を黙って捨てない検査を規定する（従来の実装は未知キーを黙殺——タイポの 検査面が無かった。本 ADR の静的エラー群の執行にはこの検査が前提）。

5. 複数の並行列は別束縛が正準（labels: は一列＝束縛名射影の一意性）:

   lunarMonth = day |> segmentBy(lunarStart, edges: drop, empties: error, labels: monthNos)
   kyuMonth   = day |> segmentBy(lunarStart, edges: drop, empties: error, labels: monthNames)
   

   マーカー共有で重複は軽く、検査が二重に効く（従来イディオムでは monthNames 側が無検査だった）。 二重束縛の相互整合（両リストが同じ窓を指すこと）は本検査の射程外——正準はマーカーの束縛名を 共有すること（将来の警告級検査の候補）。「既存の窓束縛へのラベル後置」（kyuMonth = lunarMonth labels: monthNames 級）は将来候補として記録（ADR-34 帰結「within で被せた別名からは読まない」との 線引きの再整理が要るため見送り）。ADR-34 の label: ラムダ経由は「labels: に乗らない計算ラベル 用」に位置づけを降格して残す（ADR-30 改訂節で判断 5 の補助束縛パターンを再配置）。

6. 守備範囲の較正: 本検査が守るのは長さのみ——同長の位置ずれ（先頭に朔を足しラベルを末尾に 足す誤更新）は通る。中身の照合は従来どおり doctest（旧正月照合）と coincides（閏月検出＝ADR-38）の 分担。生の list[epochOrdinal(w, d)] は値式として合法のまま（一般の添字は禁じられない）——F62 の 処置は「解消」でなく「検査を運ぶ器と正準形の確定」（ordinalIn 還元・ADR-27 と同じパターン）。

背景: F62（stdlib 拡充で新出）。旧暦の monthNos[epochOrdinal(lunarMonth, d)] は値リストと窓列の 結びが書き手の頭の中にしかなく、リストが窓数より長い方向のずれは黙って全月番号がずれる（短い方向は 添字外の硬エラー）。優先度は二度上がった——ADR-37 の覆域端確定で実際に窓が 37→38 になり monthNos の 追記が要り（実例）、ADR-38 の coincides が中身の照合の道具を提供した。候補設計（draft §1.22）を 2 視点検証（整合性＋敵対・コーパス＋実装、指摘 22 件）に掛け、epochOrdinal 相乗りの紀元跨ぎ矛盾・ 規則マーカーの穴・合成マーカーの三値の縁・窓数の覆域基準化・主張の較正を反映し、設計者裁定 2 件 （受け皿＝labels: 一般化・締め＝全部静的エラー。いずれも推奨案）で確定した。

却下した案:

• マーカーテーブルの点ラベルを窓へ継承: lunarStart = newMoons |> snapTo(day) の変換で点と ラベルの対応が剥がれる（ラベルはテーブルに付き点は格納しない＝ADR-30）。変換を挟まない特例は 規則の二重化。
• 使用点での自動照合: 一般の値式 list[expr] から「並行」の意図は読めない。宣言なしの検査は 原理的に立たない。
• 値レベルの表明（assert length(…) == windowCount(…) 級）: 検査専用の値関数二つと表明文の 新設が要り宣言形より表面が大きい。窓数が覆域依存であることの説明も難しい。
• clip 擬似窓はラベルなし・読みは硬エラー（緩め案）: 黙ってずれる面は防げるが、擬似窓の有無で 読める範囲が変わる複雑さが残り、ティティは drop 移行で足りるため実需なし。

帰結:

• spec: §4.2（segmentBy に labels: 引数——前提条件と締めの列挙）・§4.9（ラベル源の表に窓データ ラベル・窓列序数の定義的等式）・glossary（labels: 行の適用先更新）。EBNF は変更なし（labels は param-key に登録済み・引数位置の式で書ける）。
• ADR-30 に改訂節（labels: の適用先一般化・判断 5〈補助束縛パターン〉の再配置＝「labels: に乗らない 計算ラベル用」）。
• stdlib/kyureki を正準形へ書き換え（lunarMonth/kyuMonth の labels: 化・lunarMonthNo の削除・ rokuyoNo の書き換え・§7(4) は「同長は言語が検査・中身は doctest＋coincides」の分担明示へ反転・ §7(5) は計算ラベル用に降格）。doctest 期待値は全ブロック不変。40-examples 05 §5.1（ティティ）は drop＋labels: へ・03 §3.1/3.2（節月・F23 の擬似コード）は labels: の実コードへ。
• リファレンス実装: segmentBy の labels:（評価・型検査・同居/clip/drop/規則マーカーの静的エラー・ 覆域基準の同長検査）・束縛名射影の読み（label: と同じ分類器経路・遅延機構は不要）・未知 named-arg 検査。見積もり約 50 行＋テスト 12〜15 本・既存 208 テスト波及ゼロ。
• 90-open-questions: F64 の面積拡大を追記（labels: 束縛は窓語と射影名の二役が常態化——同名適用の 型規則の優先度を連動）。「窓束縛へのラベル後置」を将来候補に記録。

改訂（2026-07-13・ADR-45）: 判断 1 の「空リストは不可」は窓列（segmentBy の labels:）側の 規定に限定する——空テーブルリテラルの labels: []（ADR-45）は時点列と同長（0=0）で合法。 窓ゼロの窓列に labels: を張る需要は立っておらず、segmentBy 側は従来どおり（空マーカーは硬エラー）。

This site is open source. Improve this page.