日本語 · English

Kairos 言語仕様 — 3. premise 層

premise 層は、本体層が立つ前提——暦法・カレンダー・軸・ロール規約など——を組み立てて供給する層である。

3.1 premise とは

premise は、ある式・節・句の解釈が成立するための先行条件の総称である。含むもの: 暦法（calendar-system）・ 軸・カレンダー・ロール規約・粒度・TZ・asof・WKST・出所（source）。契約の前文（recitals）が以降の条項の立つ前提を 先に据えるのと同じ役割を、式に対して果たす。ストリーム（値）と演算子（動詞）は premise の上で評価されるが、 premise ではない。

3.2 前文（premise 宣言）

前文は本体式の前に置き、以降の式を統べる（次の前文まで有効）。同一の束縛操作に長短の三形がある。

定義（多行可） — @名前 が束ねる中身を定義する。

premise JP {
  calendar-system: Gregorian      # 暦法（構造）
  calendar:        TSE            # カレンダー（方針・営業日）
  tz:              "Asia/Tokyo"   # TZ・出所は文字列リテラル（ADR-32）
  wkst:            Mon
  asof:            latest
  source:          "cao.go.jp/official"
}

軽量形 — 定義済みの束を前文に敷く。@名前 は単一値の別名（@TSE）でも多メンバーの束（@JP）でも同じ参照。

@JP
monthEnd |> roll(Preceding, on: bizDay) |> shift(-3, unit: bizDay)

完全形インライン — 名前を付けずその場で前文にする。

premise { calendar-system: Gregorian; calendar: TSE; tz: "Asia/Tokyo"; wkst: Mon }

範囲を明示的に括るときはブロック形 @名前 { … }（中は束縛・本体式の並び）。段引数は最内で前文を上書きする。

3.3 メンバー枠と省略の統治

メンバーは暦法・カレンダー・軸・ロール・粒度・TZ・asof・WKST・出所。取り違えがサイレントな誤結果を生む 危険なメンバーは宣言必須寄り、安全なメンバーは既定可。前文でも段でも解決できない危険メンバーは静的エラー。

メンバー 省略時 危険性の根拠
calendar-system（暦法） 既定可（Gregorian） 取り違えは名前曖昧性で検出
calendar（営業日カレンダー） 宣言必須 万能な既定が無い／別日を黙って出す。値はカレンダー実体（正体判定・§3.9）
axis（軸） 宣言必須（言語既定なし） 軸取り違えで別結果（shift の 3 日／3 営業日）
roll（ロール規約） 宣言必須 無効点の寄せ方の取り違えはサイレント誤結果
wkst 宣言必須寄り 「第 N」の起点が反転
tz 宣言必須寄り ローカル日がずれる
source（出所） 宣言必須寄り 公式版／ローカル上書きの混同
granularity（粒度） 既定可（「日」） 明示でも既定でも結果不変が多い
asof 既定可（評価時点） 再現性重視なら宣言推奨

軸・ロールの畳み込み（スコープ既定）

on:（roll・filter）と unit:（shift）は、操作する軸を premise 相対に名指す （bizDay／day／hour…。cycle 名〈weekday〉はラベルでありストリームに解決されないので軸には立てない。 stride は入力相対＝軸を取らない——ADR-38）。 軸は在圏の calendar: に解決される（bizDay は @JP なら TSE の営業日）。 軸名は在圏 premise で有効点ストリームに解決されるので、導出したストリームをそのまま軸として渡してもよい （振替休日の roll(Following, on: nonHoliday) など。ADR-26）。軸位置に premise 名（on: TSE）が立ったら、 それがカレンダー実体であることを正体判定で要求し、「その段だけ calendar: を上書きして標準導出 bizDay を 読む」と読み替える（§3.9・ADR-35）。 複数段が同じ軸を書く冗長は、軸を前文メンバー axis: に一度だけ宣言して畳める。省略した段は在圏の axis: から 解決する。これはレキシカルなスコープ既定（既定 → 評価文脈 → ブロック宣言 → 段引数、最内優先）であり、後段推論 ではないため各段の局所性は保たれる。同じ機構でロール規約も前文メンバー roll:（束定義または軽量形の後置）に 一度宣言して段が継承できる。ただし危険メンバーゆえ規約は明示を推奨する。

# 明示（軸を各段に書く）
@JP
monthEnd |> roll(Preceding, on: bizDay) |> shift(-3, unit: bizDay)

# 畳んだ姿（軸の既定を後置で本体に与える）
@JP axis: bizDay
monthEnd |> roll(Preceding) |> shift(-3)

# その段だけ別軸（最内優先で上書き）
@JP axis: bizDay
monthEnd |> roll(Preceding) |> shift(-3, unit: day)

3.4 名前解決は premise 相対

名前は現在の premise の下で値に解決される。複数の premise が同名を与えるなら曖昧となり、修飾（Gregorian.month）を 要する。「意味は premise 相対」は値だけでなく名前にも及ぶ。一意なら裸名、曖昧なら上位存在で修飾、未解決はエラー。

3.5 値式・変数

premise 層は時間ストリームでない値式を持つ。演算子は結合子（&・|・\）と衝突しないよう選ぶ。

種別 記号
算術 + - * /、剰余 mod・整数除算 div（語）。div は floor 除算・mod は数学的剰余（負の被除数で trunc と食い違う。ADR-31 改訂・F63）
比較 < <= > >= == !=
論理 and・or・not（語。記号 &／\| は結合子に温存）
条件 三項 cond ? a : b
リスト リテラル [a, b, …]・添字 l[i]（0 起点）・所属述語 x in l
文字列 リテラル "…"（改行不可・エスケープなし。TZ・出所の値に使う。ADR-32）
束縛／等値 = は束縛（定義）、== は等値比較

値関数・値定数の束縛は premise ブロック内とファイル top-level の両方に書ける。top-level 束縛は糖衣定義 （§4.8）と同じく在圏 premise で遅延解決される——「= はどこでも同じ束縛」（ADR-28）。

ラムダと高階関数 — 演算子の中には、値そのものではなく関数を引数に取るものがある（高階関数）。 窓生成語 span/split（§3.6）とフィルタ filter（§4.6）は、いずれも「各要素をどう扱うか」を関数で受け取る 高階関数である（cycle はラベルのリストを取るので該当しない）。その場で渡す無名の関数をラムダと呼び、引数 => 式 で書く（矢印 => は型記法 -> と区別）。例えば y => y mod 4 == 0 は「暦年 y を受け取り 4 の倍数かを返す」関数。ラムダは名前を付けて 束縛でき（isLeap = y => …）、高階関数へその場で直接渡してもよい（filter(x => …)）。

述語と変数 — 述語（真偽を返すラムダ）は対象の各要素を束縛する。where は filter に統合し、filter が premise 述語（on:）と値式述語（ラムダ）の両方を取る。束縛名で参照するので入れ子でも曖昧にならない。

isLeap = y => y mod 4 == 0 and not(y mod 100 == 0 and y mod 400 != 0)

3.6 暦法の原始的定義

原始的定義（Gregorian 等・派生元を持たない根）は、連続基底 Chronos を窓へ刻んで暦法を組み立て、公開語を生む。 窓生成語は三系統＋一（窓を作る grid/span/split と、窓でなくラベルを生む cycle）。窓を作る三語は いずれもパーティション型窓（§4.2）を作り、網羅・無重複が構造的に保証される（I5）。本節は 原始的定義の書き方を Gregorian を例に説明する。Gregorian そのものの網羅的な解説（各語・weekday と WKST の 分離・スコープ）は stdlib/gregorian.md を参照。

依存はボトムアップ集約を主とする: 原子 day を month に束ね、その month を year に束ねる（month が 基本の括り）。year の従属窓（quarter）だけは year を split で割って作り、year の変化に自動追従させる。

語 種別 意味
grid(w) 一様分割 連続軸を幅 w で等幅にタイル。暦の原子を作る。w は市民時の幅規約（1d＝1 市民日で、固定秒数 86400s ではない。市民日は DST 切替日に 23〜25 時間になる。うるう秒はスコープ外＝chronos はうるう秒を持たない一様な理想化軸（UTC の各日＝86,400 秒）。ADR-11/12/33）。位相は既定で市民時幅＝在圏 tz: の各市民日の開始瞬間（通常日は真夜中。ADR-31 改訂）・経過時間幅＝紀元に整列し、anchor: で上書きできる（ADR-31）
span(f) 可変集約（ボトムアップ） 細かい単位の列を連続窓へ束ねる。f = n => 個数 は生成中の窓の序数 n（紀元起点）を束縛し束ねる単位個数を返す。個数は可変（month の日数）でも定数（year の 12）でもよい
split(g) by: u 可変分割（トップダウン） 親窓を連続部分窓へ割る。g = y => [幅…] は親の序数 y を束縛し部分窓幅のリストを返す。by: u は幅の単位を明示。幅総和が親に一致することは I5 で検査可能。従属窓に使う
cycle(labels) anchor: 並列ラベル 対象のパーティション窓に反復ラベルを付す。窓でなくラベルを生む。周期長は任意（7・10・12・60…）、適用先も任意の窓（day の曜日に限らず month・year も可。十二支は year cycle […]）。anchor: は時点で「属する対象窓が先頭ラベル」。束縛名は値式で「点 → ラベル」の値関数として読める（filter(d => weekday(d) == Mon)。解決は点 → 属する窓 → ラベルの二段。ADR-27）

閏は窓でなく値（依存方向を決める要）

「2 月は 28 日か 29 日か」は year という窓への依存に見えるが、実際には month の通し番号 m から算出できる 値依存である（m から暦年と月位置を割り出し isLeap で判定）。だから month を year 窓に依存させる必要が なく、month を基本の括り（day を束ねる）に置ける。もし month を year の子（year split）にすると、派生 （会計暦。§3.7）で year を month から束ね直すとき month ↔ year が循環する。閏を値依存と見て month を親に 置けば循環は最初から生じない——これが会計暦を一行で・回避策なしに書ける根拠になる。

公開語

ブロック top-level の束縛だけが公開され、Gregorian.month のように . で参照される。境界は本体層の選択子を 再利用して導く（新機構ゼロ）。生成子 monthEnd（暦日の月末を出す）の正体はこの公開境界語 month |> last そのもので、「生成子」は原始的定義の公開境界語である（別機構ではない）。

premise Gregorian {
  day     = chronos grid 1d                                 # 原子（連続軸を市民日で分割）
  weekday = day cycle [Mon, Tue, Wed, Thu, Fri, Sat, Sun] anchor: 2000-01-03

  isLeap      = y => y mod 4 == 0 and not(y mod 100 == 0 and y mod 400 != 0)
  daysInMonth = m => monthLengths(isLeap(yearOf(m)))[monthOf(m)]  # 閏は m から値計算（year 窓を見ない）
  month   = day   span daysInMonth label: (p => monthNo(p))        # 基本の括り：day を束ねる（year 非依存）
  year    = month span (_ => 12) phase: 0 label: (p => yearNo(p))  # month を 12 ずつ束ねる
  quarter = year  split (_ => [3, 3, 3, 3]) by: month       # year の従属窓（会計暦で自動追従）

  weekStart = day |> filter(d => weekday(d) == wkst)        # wkst は利用側前文の宣言を遅延解決
  week      = day |> segmentBy(weekStart, edges: clip, empties: error)

  monthStart = month |> first                               # 公開境界語（選択子の再利用）
  monthEnd   = month |> last
  yearStart  = year  |> first
}

補助値関数 yearOf(m)／monthOf(m)／monthLengths(bool) は month 序数 m から暦年・月位置・日数リストを返す 値式（year 窓を参照しない）。束縛は依存順に解決（day → month → year → quarter）。相互参照は可、循環はエラー。

窓序数 n・m の起点となる紀元は言語既定で 1970-01-01T00:00（在圏 tz）。別基準の暦法（火星暦等）は 原始的定義のメンバー epoch: で上書きできる（暦法に内在する値であり、利用側の前文には置けない。序数は 0 起点＝monthOf(m) = m mod 12 が成立する座標。ADR-31）。紀元は在圏 tz の写像の逆像なので、tz が違えば chronos 上の別の点——epochOrdinal・span 序数は premise 相対の座標である（ADR-33 判断 7）。

week は wkst:（前文メンバー）を右辺に参照し、利用側の在圏 premise で遅延解決される（糖衣定義 §4.8 と 同じ規則。wkst: 未宣言下での within(week) は静的エラー）。生成は segmentBy（区間列型）だが、weekday の 巡回により網羅・無重複が I5 検査で証明できるため within(week) に使える——パーティション性は生成語でなく 検査で立つ（stdlib/gregorian.md §4.5）。

premise 束縛の右辺には、値式・窓生成語に加えて本体層のストリーム式（上の weekStart のようなパイプ列・ segmentBy・テーブルリテラル §3.8）を書ける——「語彙は本体層と共有」（ADR-25）の帰結であり、公開語の型は 右辺の型で決まる（窓／ラベル／値／ストリーム。ADR-26）。

Gregorian は理想化された連続時間軸上の数学的モデルであり、歴史的事実（1582 年改暦の日付消失・重複、地域差、 うるう秒（正負とも。chronos の理想化＝ADR-33）、暦の有効範囲）は負わない。必要なら別 premise（歴史考証版）や asof/source 注釈で扱う。

tz: の発火点（ADR-33）: tz: は宣言必須寄りで、利用時に発火する（wkst: と同型）——日付リテラルの 錨・市民時幅の grid・snapTo(day) 等、chronos→市民座標の写像を要する評価が在圏で tz: を解決できなければ エラー。写像を使わない式は宣言なしで立つ。TZ の定義（写像・市民日・隙間/重複・うるう秒・版）は ADR-33。

3.7 暦法の派生的定義

派生的定義は、既存 premise の公開語を上書き・追加して新しい premise を作る（premise → premise の閉包）。core は with 上書き——base を土台に、指定した公開語だけ差し替え、残りは継承する。

premise Fiscal = Gregorian with {
  year = month span (_ => 12) phase: 3 label: (p => yearNo(p))   # 4 月始まり。label: は上書きに継承されない＝同時付与（F96）
  # month は触れないので暦月・月末は不動（Gregorian のまま継承）
  # quarter は継承定義（year split by month）が新 year に自動追従 → 会計四半期 Apr-Jun/…
}

名前解決（機構 A）:

日付は動かない（基底固定 I1） — 派生が動かすのは窓の切れ目だけ。暦日・day/month・monthStart は 不動。2026-03-01 は「3 月 1 日」のまま、所属する年窓だけが変わる（2025 年度＝Apr2025–Mar2026）。

パイプは糖衣、展開は span の位相ずらし一発 — 日常形は premise Fiscal = Gregorian |> rephase(+3, on: year, unit: month)。rephase は上の with へ展開する 糖衣で、展開規則は：

rephase(δ, on: W, unit: U)  ≡  W = U span (_ => k) phase: ((φ₀ + δ) mod k)   # 負の δ も法で正規化（F65）
#   k  = W が含む U の個数（year ⊃ month なら 12）
#   φ₀ = base での W の位相（Gregorian の year は 0）

W を「U を k 個ずつ束ねる span」と見て、その位相を δ 進めるだけ。k が定数でない組（month ⊃ day を day 単位でずらす等）は会計暦型の操作ではなく、rephase の射程外（必要なら別演算子）。

直交する別ノブ — 年度の番号付け（2025 年度＝開始暦年／US FY＝終了暦年）は窓の切断とは独立した序数・ラベルの 射影で、規約が国ごとに違う。rephase に埋め込まず、窓→値の射影一族（§4.9・ADR-27）のラベル付与側 （label: 付与式）に吸収する。付与式の束縛規則は ADR-34 で確定——ラムダは窓の先頭点を受け （label: (p => yearNo(p)) が開始暦年ラベル）、隣接窓参照は射程外（§4.9）。rephase は base の label: を保存して展開し（切断ノブとラベルノブは直交）、合成位相は k を法として正規化する（F65）。

3.8 データの持ち込み口（テーブルリテラル）

周期規則から生成できない列——官報告示の春分・秋分、朔（新月）、二十四節気、年限定の特例日——は、 テーブルリテラルで premise に持ち込む（ADR-26）。時点リテラルのリストは時間ストリーム定数に昇格する （構文は値リスト §3.5 と同一、型は要素で決まる）。列は昇順を要求（乱順・重複は静的エラー）。 空リスト [] は covering: が後置されたときに限り昇格する（空テーブル＝「点ゼロだが覆域は 主張したい」の一次形。ADR-45——供給層の「まだ何も無い」を合法ソースで書く器。要素が無いため型は covering: の有無で決まり、包含・昇順・labels: 同長〈labels: [] のみ合法〉の各検査は空虚に成立。 整列は空虚適合＝§4.5）。

premise JPGazette {
  source: "cao.go.jp/official"      # 出所（宣言必須寄り: データの出所取り違えは危険。文字列＝ADR-32）
  asof:   2025-02-03                # 版（この告示時点のデータ）
  tz:     "Asia/Tokyo"              # データの市民日を内側に固定（ADR-33 判断 10・F54）
  vernalEquinoxDay = [2025-03-20, 2026-03-20, 2027-03-21] covering: 2025..2027
}

命名の確定状況は §5.4: grid・span・split・cycle・anchor:・phase:・by:・with・chronos（基底の 字句名。ADR-29）・axis:（操作軸）に加え、RC2 で covering:・labels:・label:（テーブル・付与側）も確定。 命名は全語確定——最後の仮称も rephase に裁定済み〈2026-07-26・旧 shiftBoundary。F51 の一括確定〈2026-07-09〉と合わせ仮称ゼロ。§5.4〉。日付・幅リテラルの字句は確定済み（ADR-28/43・§5.5）。

3.9 カレンダー実体（ADR-35）

calendar: メンバーに与える実体（TSE・JPCal 等）は、予約公開語 nonWorking を持つ premise である。専用の宣言構文は無い——「ストリーム束縛＋source:/asof:」を束ねる構文は premise 定義（§3.2）と 層またぎ規則（§3.6 末尾・ADR-26）で既にあり、カレンダー実体に固有なのは「どの束縛が非稼働集合か」の 指名だけだからである。

premise TSE {
  calendar-system: Gregorian          # weekday の解決に要る（satSun の定義）
  tz:     "Asia/Tokyo"                # 非稼働「日」がどの市民日かを確定（内側固定・ADR-33）
  source: "jpx.co.jp/trading-calendar"
  asof:   2026-01-05

  satSun     = everyDay |> filter(d => weekday(d) == Sat or weekday(d) == Sun)
  holidays   = [2026-01-01, 2026-01-12, …] covering: 2026..2026
  nonWorking = satSun | holidays      # 予約公開語＝実体の「正体」
}

premise JP {
  calendar-system: Gregorian
  calendar:        TSE                # nonWorking を公開する premise だけがここに立てる
  tz:              "Asia/Tokyo"
  wkst:            Mon
}

3.9.1 細粒度層——営業時間の供給規約と標準導出（ADR-41）

実体は nonWorking に加えて対の予約公開語 sessionOpens・sessionCloses——開場列・閉場列 （時間ストリーム型・引数なし）——を宣言できる（任意。宣言は対＝片方だけは静的エラー・with 派生では継承込みで判定）。点は実体 tz の市民座標の事実（壁時計——「DST でずらすかそのままかは premise 層の文化の決まり」の執行形。規則は時刻付き anchor の市民グリッド〈§3.6・ADR-31 改訂 2〉か strideBy の市民時幅・例外は時刻付きテーブルの合成）。セッション＝半開区間 [open_i, close_i) の 和。深夜セッション（日跨ぎ）は合法・24 時間営業はこの器の外（日粒度の層で表す）。

整合性検査（データ相対の層・細粒度導出の初回使用時）: 定義域＝結合実効被覆域∩実体化範囲で 隣接マーカーの種別が交互（端の孤立 close/open は切り欠きとして合法）。同時刻の open/close は 両点とも存在し、順序は交互性の要件から一意（close→open＝連続営業／open→close＝幅 0）——同時 イベントの発火の扱いは発報層（スコープ外）。

標準導出（calendar: 在圏で予約・実体 C が対を宣言しているとき）: bizOpen＝C.sessionOpens のうち 開場日（C-tz の市民日）が C の営業日である点・bizClose＝各セッションの閉場点・isOpen(t)＝t が bizOpen セッションの区間の和に入るか（値述語）。導出は実体相対——判定材料（休日・tz）は実体の 文化で解決し、読み手の premise に依存しない（日粒度の bizDay＝利用側相対とは役割が違う）。 セッションの営業日性は開場日で読む（深夜セッションの尾部は開場日に従う）。覆域は証人規則の 三分岐（真＝非註釈の判定・範囲外＝sessionOpens/sessionCloses/nonWorking の註釈区間に依存・偽＝覆域完全。§4.10）。 bizHour 級の点列は導出しない——粒度は式の選択（hourly |> filter(t => isOpen(t))）。

This site is open source. Improve this page.