日本語 · English（未訳）

ADR-45: 空テーブルリテラル——「点ゼロだが覆域は主張したい」の一次形（F98）

判断: 空リスト [] は covering: が後置されたときに限り時間ストリーム定数（空テーブル）に 昇格する（F98。実装系からの還流ルート初便の綻び＝発報層は DB 未投入でも boot が通る合法ソースを 要し、データ供給層の「まだ何も無い」は初回 boot・年替わりの定常状態。候補設計 draft §1.26＝ 3 視点検証済み・設計者裁定 2026-07-13〈候補 3 形から本形を選択〉を経た ADR 化）。

1. 昇格ゲート＝covering: 後置（ADR-26 改訂）。covering の無い [] の型は従来どおり空の値 リスト（値位置では合法）で、ストリーム期待位置に置くと静的エラー（誘導文言つき＝「covering: を 付ければ空テーブル」）。labels: だけ付けた [] も誘導つき静的エラー（「空テーブルは covering: を明示する」）。根拠: 省略既定「列の端＝閉区間 [先頭要素, 末尾要素]」（ADR-37 判断 1）は空列で 定義できない——覆域の主張なしに空テーブルは書けない（うるさい側が安全側＝ADR-37 判断 9 の 省略既定と同じ統治）。segmentBy(labels:) の空リスト不可（ADR-39＝窓列側）と cycle/split 等の リスト引数は射程外・従来どおり。

2. 静的検査は空虚に成立。包含（列の全要素 ⊆ covering）・昇順/重複・labels: 同長（labels: [] は 0=0 で合法・空でない labels は同長違反の静的エラー）——いずれも全称検査で空虚に真。帰結: ソース生成器はテーブル直書き生成に限り行数 0..N で同一の出力形になる（F98 の実駆動が消える。 segmentBy＋labels: 生成形の空マーカーは従来どおり硬エラー＝射程外・需要が立てば別綻び）。

3. 整列＝空虚適合（vacuous conformance）の第三状態（ADR-36 改訂）。空テーブルは全ての整列に 空虚に適合する（違反しうる点が無い）。「なし」（主張できない＝検査に落ちる）とは別の状態で、 検査には通る: (a) ADR-36 判断 3 の検査は相手が「なし」でも通す、(b) 判断 4 の和・&/\ の 出力整列は相手側を継承、(c) 保存系の段（filter・選択子・shift 窓語・roll・snapTo・rebase 〈点ゼロは恒等〉）は空虚適合を保存、(d) カレンダー実体の day 整列要件（ADR-35 正体判定）も 空虚に通る＝空 nonWorking の実体が boot し bizDay = everyDay（覆域内。覆域外は範囲外註釈＝ 「退化するが観測可能」）、(e) tz 名検査（ADR-36 改訂 2）は市民グリッド同士の規定のため掛から ない（点ゼロに 1 日ずれは起き得ない）。

4. covering の意味論は不変。「範囲内は完全・範囲外は未知」の二面の主張（ADR-37 判断 1）の 空列読み＝範囲内に点が無いことは知識。範囲外評価は範囲外註釈・被覆サマリ〔源・covering・ asof・残走路〕——回避形（恒偽 filter＋束縛後置の被覆主張）と動的観測で等価で、runway 即負の 運用信号が一次形で書ける。束縛名射影の失敗分類は ADR-37 判断 6 のまま不変——完全主張は 分類を軟化しない（覆域内の sekki(d) 失敗は硬エラー＝取り違え検出）。開端 [] covering: .. は 「全時間で恒空」の完全主張（単発除外テーブルの双対・判断 9 の統治がそのまま掛かる。boot 用途は 閉端で書く作法——残走路信号を恒久に消さない）。区間リスト covering・tz: 宣言必須も従来どおり。

5. EBNF は変更なし。list-literal の要素列は既に省略可能（spec §5.6）で、空を弾いていたのは 意味層。「空⇒covering 必須」も静的検査に置く（文法エラーは誘導を語れない）。§5.6 の意味論注記を 二点改稿——「型が要素で決まる」に空の場合分け（covering: の有無で決まる）・束縛後置注記 「テーブルの属性と同義」→「テーブル属性として読む」（空テーブルで両読みが乖離するため）。

背景: 発報層実装からの第一次還流（適用検討 03・非公開）。回避形 (everyDay |> filter(d => 1 == 2)) covering: … は動くが、恒偽が迂遠で意図が読めず、ソース生成器に 行ゼロ分岐を強いた（F98）。候補 3 形の比較（90-open-questions 記録）から設計者裁定で本形を選択。

却下した案:

• empty 生成子（新語一語＋束縛後置 covering）。「規則（恒空）」に被覆主張を付ける形になり 「データの器に行が無い」という出自の意味とずれる・生成器の行ゼロ分岐も残る。
• 恒偽の標準述語（never 級）。迂遠さの緩和のみで分岐も残る（実質、生成子案の劣化形）。
• 裸の [] の昇格（covering 省略可）。省略既定が定義できず、「黙って完結扱い」はデータ切れの 黙認になる（ADR-37 判断 9 と同じ理由で棄却）。

限界の明記: 整列は字面ベース（ADR-36 テーブル規則）のため、0 行→1 行で整列が変わる—— 空虚適合は初データ投入で市民日グリッド（日付字句）または「なし」（時刻付き）へ変わり、通っていた 静的検査が割れうる。空リテラルは将来の要素の字面を知り得ないため、どの静的割当でも逆向きの割れが 出る原理的性質（エラーは再実体化時にうるさく出る＝黙らない）。時刻付きの列に育つ器を合成に使う 生成器は、明示の再整列（snapTo）を挟む作法。規則性（endless）は有限＝テーブル由来が正で、回避形 （規則由来＝無限）との唯一の静的差（ADR-39 の規則マーカー検査で正しい側に倒れる）。

検証（2026-07-13・3 視点＝整合性/コーパス全数掃引/敵対的・実装可能性、詳細は draft §1.26）: 構造欠陥 0・要修正 7（候補設計に反映済み）・注記 4。副産物＝F99: roll の空軸で依存像 （ADR-37 判断 4 roll 行）の早期 return が保守拡張を殺し、「有限 covering＝空＋註釈」と「開端＝ 註釈なしの空」の観測差が消えていた既存 impl 欠陥を発見・修正（本 ADR と独立の欠陥・90-findings）。

帰結:

• 既存の式の意味は変わらない（静的エラーだった形の合法化＝追加拡張。回避形の挙動も不変）。
• spec: §2.1（昇格の但し書き）・§3.8（空テーブル＝covering 必須・意味論）・§4.5（整列表に空虚適合の 行・検査と継承の規則）・§5.6（意味論注記の二点改稿）・glossary（テーブルリテラル・covering・ 整列の各項）。reference/table-literal.md（形・空形の doctest・落とし穴）・reference/README （#=> 行なし＝点ゼロの期待、の明文化）・reference/combinators.md（空虚適合の但し書き）。
• ADR-26（昇格ゲート）・ADR-36（整列第三状態）・ADR-39（空リスト不可の窓列側への限定）に改訂節。
• impl: evalList の昇格分岐・整列タグ vacuous・結合子の継承・rebase 恒等・誘導エラー文言 2 種・ F99 修正（dependImageAnn の早期 return 削除）。empty-table.test.ts 23 本（全消費位置の掃引・ F99 回帰込み）。

This site is open source. Improve this page.