Kairos 1 級教本 — 運用意味論 / Operating Kairos (Grade 1 Textbook)

版: v1.1（2026-08-03・言語 RC5 準拠・spec_head: 44493ad——外部レビュー第 7 回 E1 処置＝第 1 章の covering 解釈を正本に整合・boot 作法の対比例を新設）。1 級のねらい＝本番運用で裏切られないスケジュール定義を設計できるようになる——読める（3 級）・書ける（2 級）の先にあるのは、データの鮮度・結果の信頼度・実行系との分業まで含めた運用の意味論。正本は常に言語仕様—— 本書は運用の道筋を示すだけで、仕様を再定義しない。

本書の読み方: 1 級の理解は本文と章末演習で完結する。参照リンクは正本の確認用（実例から入るなら reference）。本文の「動かして読む」の例はすべて実行検証済み（# eval: が評価範囲・直後のブロックが実際の出力）。各例の下の「▶ Playground で開く」から、ブラウザでそのまま実行・改変できる（インストール不要・kairos-lang.org/playground）。1 級の主役は発火点列の 下に付く行——# ⚠ の註釈と # 被覆サマリ。3 級・2 級で読み飛ばしてきたこの数行が、本章からは本文になる。

第 1 章データの鮮度を宣言する——covering と「正当な空」

祝日・営業日・節気——スケジュールの材料の多くは計算で出せず、データで持ち込むしかない。そしてデータには必ず「ここまでしか知らない」という端がある。Kairos はこの端を covering: で宣言させる——「この列は、この範囲について完全」という主張であり、値には触れない （範囲内に点を足しも引きもしない）。

宣言の力が最も分かるのは空のとき。空テーブル [] covering: 範囲 は「点ゼロだが覆域は主張したい」の一次形（ADR-45）——そして covering の読みは空でも変わらない。 [] covering: 2027..2027 は「2027 年を完全に把握しており、祝日はゼロ」という主張である:

動かして読む——空テーブル＋広い covering は「祝日ゼロ」の完全主張:

# eval: 2027-01-04..2027-01-11
premise JP {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
}

@JP
holidays2027 = [] covering: 2027..2027
satSun = everyDay |> filter(d => weekday(d) == Sat or weekday(d) == Sun)
bizDay = everyDay \ (satSun | holidays2027)

bizDay

2027-01-04
2027-01-05
2027-01-06
2027-01-07
2027-01-08
# 被覆サマリ
#   holidays2027 covering 2027-01-01..2027-12-31 残走路 355 日

▶ Playground で開く

月〜金の 5 点が無註釈で発火し、被覆サマリは残走路 355 日と告げる。主張の内側だから註釈は出ない——それがこの形の危うさでもある。もし実態が「2027 年の祝日データがまだ届いていない」なら、この式は過大主張だ: 実在の祝日 2027-01-01（元日）が無註釈で営業日として発火し、+355 日の残走路は偽の安心を返す。覆域は知らないことまで語ってしまえる—— 広げるほど主張は強くなる。

「まだ届いていない」の正しい書き方は観測日当日のみの最小主張——覆域を、実際に確認した日までに絞る:

動かして読む——同じ空テーブルでも、正直な覆域なら註釈と負の残走路が「データを入れよ」と告げる:

# eval: 2027-01-04..2027-01-11
premise JP {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
}

@JP
holidays2027 = [] covering: 2026-08-02..2026-08-02
satSun = everyDay |> filter(d => weekday(d) == Sat or weekday(d) == Sun)
bizDay = everyDay \ (satSun | holidays2027)

bizDay

2027-01-04
2027-01-05
2027-01-06
2027-01-07
2027-01-08
# ⚠ 範囲外 2027-01-04..2027-01-11（holidays2027 covering 2026-08-02..2026-08-02）
# 被覆サマリ
#   holidays2027 covering 2026-08-02..2026-08-02 残走路 -161 日

▶ Playground で開く

点列そのものは同じでも、範囲外註釈が「この結果は祝日データの外で退化している」と並走し、残走路は即負——「尽きる前に」ではなく「もう尽きている」を機械可読で告げる（退化するが 観測可能、が Kairos の約束）。これが空テーブルの boot 作法——点ゼロでも、覆域は知っている範囲だけ（reference/table-literal の「落とし穴」）。逆に covering の末尾を開端（covering: 2027-01-01..）にすると「それ以降 ずっとこの列で完結」という最強の主張になり（残走路 ∞）、残走路信号は恒久に消える—— 完結を本当に主張できるデータにだけ使う。

まず読む: reference/table-literal（covering の形一式）
正本の確認用: 仕様 §3.8（テーブルリテラル）・§4.10（covering の主張）
演習: L1-002 空テーブルと「正当な空」

第 2 章空を読み分ける——実効被覆域の三分岐

結果が空のとき、Kairos は「なぜ空か」を出力の形で区別する。三つの顔がある:

実体化地平線——計算範囲の端に当たった。horizon-clip 警告で知らせる（「評価 to＋400 日」はリファレンス実装の定数であって言語の地平線ではない—— 実装が違えば幅も違う。評価範囲の設計を見直す）。
実効被覆域の外——データが「知らない」区間に踏み込んだ。範囲外註釈（# ⚠ 行）が並走する（未知——供給を更新すれば点が出るかもしれない）。
完結データの正当な尽き——該当が無いことが確定している。何も付かない、ただの空（何もしなくてよい）。

動かして読む——同じ「点ゼロ」の ② と ③。違いは covering の宣言だけ:

# eval: 2027-01-01..2027-06-01
premise JP {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
}

@JP
sekkiA = [2026-02-04, 2026-05-05] covering: 2026..2026
([2027-03-01] covering: ..) |> roll(Following, on: sekkiA)

# ⚠ 範囲外 2027-01-01..2027-06-01（sekkiA covering 2026-01-01..2026-12-31）
# 被覆サマリ
#   (無名テーブル) covering ..（完結主張） 残走路 ∞
#   sekkiA covering 2026-01-01..2026-12-31 残走路 -151 日

▶ Playground で開く

# eval: 2027-01-01..2027-06-01
premise JP {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
}

@JP
sekkiB = [2026-02-04, 2026-05-05] covering: 2026-01-01..
([2027-03-01] covering: ..) |> roll(Following, on: sekkiB)

# 被覆サマリ
#   (無名テーブル) covering ..（完結主張） 残走路 ∞
#   sekkiB covering 2026-01-01..（完結主張） 残走路 ∞

▶ Playground で開く

運用の分岐がそのまま対応する: ① は評価範囲を見直す・② は供給を更新する・③ は何もしない。「空だから異常」でも「空だから正常」でもなく、空の種類を出力が語る——これを機械可読のまま監視へ流せることが、if 文と祝日テーブルで組んだシステムとの決定的な差になる。

正本の確認用: 仕様 §4.10（実効被覆域の分類器）
演習: L1-015 空の三分岐

第 3 章註釈と残走路は運ばれる——運用信号の設計

範囲外註釈は演算子を通り抜けて運ばれる（輸送）。shift(90, unit: day) は点を 90 日動かすだけでなく、「知らない区間」も 90 日先へ写す——未知の像が評価範囲に掛かれば、そこに註釈が立つ。

動かして読む——契約データの 2027 年分が未取得（covering に中抜け）。2028 年前半を評価すると:

# eval: 2028-01-01..2028-06-01
premise JP {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
}

@JP
dues = [2026-03-01, 2026-09-01] covering: 2026..2026, 2028..2028
dues |> shift(90, unit: day)

# ⚠ 範囲外 2028-01-01..2028-03-31（dues covering 2026-01-01..2026-12-31, 2028-01-01..2028-12-31）
# 被覆サマリ
#   dues covering 2026-01-01..2026-12-31, 2028-01-01..2028-12-31 残走路 214 日

▶ Playground で開く

点はゼロ、しかし註釈が「1〜3 月の発火は未取得の 2027 年後半の契約から来ていたかもしれない」と告げる。点が出ないことと、出ない理由が信用できることは別——後者を註釈が担う。

もう一つの運用信号が残走路（被覆サマリの「残走路 N 日」）。基準は評価範囲の終端から covering の終端まで——今日からではない。負なら評価がすでにデータの端を越えている。実務では「残走路 < 75 日で警告」のような閾値監視に流し、データが尽きる前に更新を促す（尽きてから気づく祝日テーブル運用からの卒業が、この一行の意味）。

第 4 章決定性——rolling horizon に耐える定義

発報層（実行系）は Kairos の式を一度だけ評価するのではない。評価窓をずらしながら繰り返し 実体化する（rolling horizon）。この運用が成り立つ条件が決定性——同じ定義・同じデータ （asof が版を担い、external は同一スナップショット相対）・同じ範囲なら同じ結果、そして 窓を動かしても重なる範囲の点列は一致する（§7.8。データを更新すれば結果が変わるのは決定性の破れではなく供給の更新）。

動かして読む——隔週月曜を二つの評価窓で。重なり区間 [1/15, 2/1) の点はどちらも 1/19 だけ:

# eval: 2026-01-01..2026-02-01
premise JP {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
}

@JP
everyDay |> filter(d => weekday(d) == Mon) |> stride(2, from: 2026-01-05)

2026-01-05
2026-01-19

▶ Playground で開く

# eval: 2026-01-15..2026-03-01
premise JP {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
}

@JP
everyDay |> filter(d => weekday(d) == Mon) |> stride(2, from: 2026-01-05)

2026-01-19
2026-02-02
2026-02-16

▶ Playground で開く

これを支えるのが「位相は評価窓でなく式が持つ」という設計——stride の from: が必須なのはこのため（窓の先頭から数え起こすと、評価のたびに隔週の位相が揺れる）。分業の線引きも決定性から引かれる: 言語は決定的な点列の列挙まで・停止中の取りこぼし（missed-fire）の検出・遅延実行・冪等化は発報層の責務。決定性があるから、発報層は「前回どこまで発火したか」だけ覚えれば取りこぼしを列挙できる。

正本の確認用: 仕様 §7.8（消費ループ・決定性）・reference/stride
演習: L1-008 発報層との分業・L1-012 決定性

第 5 章「まだ無い」と「壊れた」——供給の境界

データを外部システムから注入するのが external——「この束縛の中身は実行時に解決される」という宣言で、解決子（resolver）は実装系が差す。ここで運用意味論の最後の区別が要る:

まだ無い——解決は成功し、中身が空（第 1 章の空テーブルと同じ「正当な空」の器）。
壊れた——解決そのものが失敗した（SupplyError）。空への読み替えはしない。

動かして読む——解決子の無い環境で external を評価すると、黙って空になるのではなく:

# eval: 2026-01-01..2026-02-01
premise HRDB {
  calendar-system: Gregorian
  tz: "Asia/Tokyo"
  wkst: Mon
  source: "hr-db/holidays"
  holidays = external(kind: dates)
}

@HRDB
holidays

供給エラー: 解決子がない——external HRDB.holidays（source: "hr-db/holidays"）は解決できない（ADR-46 判断 7 (a)）

▶ Playground で開く

「祝日ゼロの日々」として営業日計算が走ってしまう——のが if 文システムの典型事故で、Kairos は 型で止める。「まだ無い」は点ゼロで評価が続き（残走路が更新を促す）、「壊れた」は評価自体が供給エラーになる（発報層は前回の解決値で劣化運転するか、止めるかを選べる）。同じ「祝日が出てこない」でも、続けてよい空と続けてはいけない失敗を出力の型が分ける——第 2 章の三分岐と合わせ、これが「黙って壊れない」の全体像になる。

まず読む: reference/external（宣言と解決子の器）
正本の確認用: 仕様 §3.8（external・ADR-46）
演習: L1-003 SupplyError の型区別

巻末——1 級の到達確認

covering を「値に触れない主張」として設計できる（開端の重みを含む。第 1 章）
空の三分岐を出力から読み分け、運用の分岐（見直す・更新する・何もしない）に写せる（第 2 章）
註釈の輸送と残走路を監視信号として設計できる（第 3 章）
rolling horizon に耐える定義（位相は式が持つ）を書け、分業の線引きを説明できる（第 4 章）
「まだ無い」と「壊れた」を型で区別し、供給障害時の運転を設計できる（第 5 章）

ここまで来ると、Kairos の出力のすべての行（点・# ⚠・# 被覆サマリ・供給エラー）に運用上の意味が読めるはず。それが 1 級——スケジュールを書く人ではなく、スケジュールが裏切らないシステムを設計する人の水準。

Kairos 1 級教本 — 運用意味論 / Operating Kairos (Grade 1 Textbook)

第 1 章 データの鮮度を宣言する——covering と「正当な空」

第 2 章 空を読み分ける——実効被覆域の三分岐

第 3 章 註釈と残走路は運ばれる——運用信号の設計

第 4 章 決定性——rolling horizon に耐える定義

第 5 章 「まだ無い」と「壊れた」——供給の境界

巻末——1 級の到達確認

第 1 章データの鮮度を宣言する——covering と「正当な空」

第 2 章空を読み分ける——実効被覆域の三分岐

第 3 章註釈と残走路は運ばれる——運用信号の設計

第 4 章決定性——rolling horizon に耐える定義

第 5 章「まだ無い」と「壊れた」——供給の境界