book集

!txt default.formel — Formel の綴り（既定）
!txt
!txt 本が `word` で紹介できないもの＝変数・定数・引数をとる記号の綴りを書く。
!txt （`word` で紹介するもの＝語の表は DB が持つ。ここには書かない。）
!txt
!txt 印は Formel のもので、ここでは選べない：
!txt   `|` 前置＝対象言語の記号（定数）／無ければ変数
!txt   `?` `?_` 前置＝各引数の型（`?`＝集合(s)・`?_`＝クラス(c)）を引数の個数だけ並べる（1つ・2つ）
!txt   `_` 後置＝クラス（c）／`^` 後置＝命題（p）／無印＝集合（s）
!txt   ★2026-09-14＝引数の印を `.`/`_` 前置（2026-08-07〜09-11）から `?`/`?_` 前置へ変更した
!txt     （須田さん指示。`0_tutorial/2.book`「arityが正の変数・定数」節にあった `?`/`?_` 草稿を
!txt     正として書き換え。旧 `.`/`_` 前置は受理しなくなる＝意味は不変、綴りだけが変わった）。
!txt
!txt ★2026-08-23 に現行の判定をそのまま書き写した。揃っていない所もそのまま写してある
!txt   （cal は変数の s と c だけ・greek は `var p` に無い 等）。
!txt   ★2026-08-28＝**prime は英字の変数・定数・記号のどれにも書ける**ようになった
!txt     （定数を `word (,s)` `(,c)` `(,p)` の正規表現へ移した回。greek には今も prime が無い）。
!txt   ★2026-09-08＝`name cal calA-calZ` は退役した＝`cal` は「`cal`+`[lDP]`」という**合成の
!txt     literal prefix**として書く方式に変わり、`name` の類として引く箇所が無くなった（④参照）。

!txt ① 名前に使える綴り
name letter A-Z a-z
!txt ★2026-08-23 に greek を Unicode 1文字へ移した（須田さん）。大文字の Rho（Ρ）は外した
!txt   （`\Rho` は LaTeX に無い命令・実使用0件）。小文字 rho（ρ）は残す。
!txt   tex（`\alpha`）と Prover9 名（`Aalpha`）は common.php の GREEK_NAME が持つ＝綴りだけが動いた。
name greek  α β γ δ ε ζ η θ ι κ λ μ ν ξ π ρ σ τ υ φ χ ψ ω Γ Δ Θ Λ Ξ Π Σ Υ Φ Ψ Ω

!txt ② この Formel で使える Form 型（従来どおり、集合・クラス・命題をすべて使う）
form s c p

!txt ③ TeX表示にだけ使い、syntax計算では無視するword
word tex_only \, \; \! !, { } _ ^

!txt ④ wordの種類と綴りの正規表現
!txt   英字v-Formは「英字1文字 → 数字0個以上 → prime 0個以上」。正規表現は常に綴り全体に適用される。
!txt   ★2026-08-27＝v_-Form（クラス変数）も同じ形へ移した（もとは下の `var c letter prime index`）。
!txt     印（`_`）は Formel のものだが、この行は**綴り全体**を書くので末尾に `_` まで書く。
!txt     これで s と c の並びが揃った（どちらも 名前 → 数字 → prime）。
!txt   ★2026-09-08＝**`[lDP]`（letter Digit Prime）という macro を導入**（須田さん
!txt     「[lNP]/[lDP] を .formel で使えるように」）。中身は `[letter][0-9]*'*`＝①の `name letter`
!txt     への参照そのもの（規約3・二重に書かない）。下の6行の重複がこの1行に集約される。
[lDP] [letter][0-9]*'*
word v-Form [lDP]
word v_-Form [lDP]_
word v^-Form [lDP]\^
!txt   ★2026-08-28＝**対象言語の記号（定数）も同じ形にした**（須田さん「他の記述に合わせて」）。
!txt     綴りの名前はライブラリの word紹介と同じ言い方＝`word(,s)` `word(,c)` `word(,p)`。
!txt     `|` 前置が「変数ではなく記号」の印。**正規表現では `|` が選択肢の印なので `\|` と書く**
!txt     （裸で書くと空の綴りにも当たり、v-Form が丸ごと定数として受理される＝入口で拒否する）。
word (,s) \|[lDP]
word (,c) \|[lDP]_
word (,p) \|[lDP]\^

!txt ⑤ この Formel の語（2026-08-27 須田さん）
!txt   ここに書いた語は、本が `word` で紹介しなくても読める（＝紹介済みとして査読へ渡る）。
!txt   語彙は compile ではなく**査読**が測る（08-25）ので、届け先は紹介査読と Thm査読の2つ。
!txt   ★★**`default` の語彙は `first` の語彙より広くなければならない**（2026-08-27 須田さん）。
!txt     `default` は `form s c p`＝`first`（`form s p`）を含む広い方の Formel なので、
!txt     狭い方で書けるものが書けないのは筋が通らない。下の5行は `first.formel` の並びそのまま
!txt     （＝もとは 1_basis/1_logic.book:8〜12。08-25 にあの本を消したとき `first` にだけ移した）。
!txt     守り手＝mathelia/test_mathel_spec.php の「`default` の語彙は `first` を含む」。
!txt   ★★2026-09-11＝須田さん決定＝**上のword行（論理のword）を撤回し、Book + importへ移した**
!txt     （「基本的なwordは.formelに書く、という方針を撤回します。Bookに書いてimportする形にします」）。
!txt     08-27の決定（.formelに書く）はこの日付までの記録として読む。移した先＝
!txt     `mathelia/common/word_logic.book`（利用する側は `import /common/word_logic` で取り込む）。
!txt     経緯は共有メモリ`project_formel_word_import_policy_20260911.md`。
!txt   ★★★2026-09-13＝続けて、この Formel が持っていた abbr 規則（∀ ∃ ∀+ ∃+ col chain ∀_ ∃_ cls cls+）と
!txt     lower 規則（{/} and_ ⟹ ⟺）も撤回し、同じ `common/word_logic.book` へ移した。
!txt     理由＝`.formel` 側の `lower` 宣言は紹介査読へ配線されておらず実質何もしていなかった
!txt     （`abbr` は `MatheliaIntroductionReviewer` が読んでいたが `lower` は読み手が無かった）。
!txt     動く場所（Book側の `abbr`/`lower` 行）へ移すことで、書いてあることと実装が一致するようにした。
!txt     経緯は共有メモリ`project_formel_capability_declaration_20260913.md`。
!txt   ★ここから下は `default` だけが持つ語＝**c-Form を使うこの Formel の語**。
!txt     `1_basis/1_class.book` の本文が「(first.formel の word の他に)次の word も登録されています」と
!txt     この3行を指している（`∈_` ＝クラスの所属／`∀_ ∃_` ＝クラスの量化／`=_` ＝クラスの等号）。
!txt   ★2026-08-27＝`⟹ ⟺ and_` は上の論理記号の行へ移した（`first` と同じ並び）。
!txt     同日いちど「本が紹介する」として外したが、須田さんが「基本的な語は `.formel` に書く」と決め直した。
!txt   ★2026-09-04＝`=_` を足した（`=` と対になる c 側の等号なのに抜けていた。須田さん指示
!txt     「=_ は .formel で紹介して」）。`min.formel` は元から `=` `=_` を並べて持っている。
!txt   ★2026-09-06 須田さん「default.formel には \cls などが登録されていなければなりません」＝
!txt     `\{ cls x | P \}`（内包記法）を足した。`1_basis/1_formel.book`が`word \cls`/`abbr cls`/
!txt     `abbr cls+`として本で紹介していたのと同じ語・同じabbr規則（実測で確認した内包記法の
!txt     フレーム語＝`tr0.php::form_decent0()`が`cls`/`cls+`のどちらかで`tr_abbr()`を呼ぶ）。
!txt   ★★2026-09-11＝`∀_ ∃_` `=_`（論理のword）も撤回し `1_basis/word_logic.book` へ移した
!txt     （上と同じ須田さん決定。`∈_`/`\cls` は非論理記号・記法なのでここに残る）。
!txt   ★★★2026-10-01＝須田さん「その仕様は止める。Bookに書かないといけないことにする」＝
!txt     残っていた `word ∈_` `word \cls` も外した＝**この `.formel` は語を紹介しない**。
!txt     使う本が自分で（または import した本で）`word ∈_` `word \cls` と紹介する（例 `common/word_basis.book`）。

!txt ⑤ まだ正規表現へ移していない綴り（word の定数だけ。2026-09-08＝**`var` は退役した**・下記）
!txt   index ＝ 数字を0個以上（名前 → index の順）
!txt   word s  |α            word c  （無し）        word p  |α^
!txt   （英字の定数は上の `word (,s)` `word (,c)` `word (,p)` が受け持つ）
!txt   `?f` `??f` `|?f` `|??f` と `?p^` `??p^` `|?p^` `|??p^` は下の `word ?f` `word ?p^` が受け持つ
!txt   （旧 `sym`。2026-09-04＝`sym` は命令語で無くし、正規表現へ移した）。
!txt   ★2026-09-08＝クラスを返す引数つき記号（`1_class.book`「新しい定数」節・`2.book`の`\cls-elim`）
!txt     `?c_` `?_?c_` `?_?_c_` `|?c_` など＝下の `word ?c_` が受け持つ。引数は `?`(集合) `?_`(クラス) を
!txt     1〜2個並べる（`?f`/`?p^`と違いクラス引数も書ける。返り値がクラスの記号だけの特別扱い）。
!txt   ★2026-09-11＝**`?p^`（述語記号）も引数にクラスを書けるようにした**（須田さん指示・
!txt     schema instantiationの未実装2点のうち1点）。`?c_` と同じ形＝引数は `?`(集合) `?_`(クラス) を
!txt     1〜2個並べる（`?_R^` は1引数・クラス1つの述語変数、`?_?R^` は集合→クラスの2引数 等）。
!txt     返り値の印（末尾 `^`＝命題）は変わらない＝`?c_` は「返り値がクラス」、この行は「返り値が命題」
!txt     で、引数の型の書き方だけ揃えた。`symbol_spelling_gram()`（data.php）は元から
!txt     `(?:\?_?){1,2}` を読める形だったので、ここを広げるだけで gram 計算まで通る（規約0＝
!txt     綴りの受理を広げるだけで、意味の変換は書き換えていない）。
!txt   ★2026-09-14＝**引数の印を `.`/`_` 前置から `?`/`?_` 前置へ書き換えた**（須田さん指示。
!txt     `0_tutorial/2.book`「arityが正の変数・定数」節の `?`/`?_` 草稿を正として実装を合わせた）。
!txt     旧 `.f`/`..p^`/`.c_` 系の綴りは受理しなくなる。意味（gram・bar の有無・返り値の印）は不変。
!txt   ★2026-09-08＝**`var` という命令語は .formel から退役した**（須田さん決定）。
!txt     cal の変数（もと `var s/c cal index`）は `cal` ＋ `[lDP]` の合成に置き換えた＝
!txt     須田さん「cal[lNP] もv-Formに指定する.formelも出てくるはず」の形そのもの。
!txt     ★この合成は旧仕様より**広い**（cal 変数にも prime が書け、`cal` の直後は大文字に限らない）＝
!txt     letter 全体を prime まで含めて揃えた今回の趣旨と合わせた（須田さん決定）。
!txt     greek の変数（もと `var s/c greek index`）は `[greek][0-9]*` に置き換えた（②の `name greek`
!txt     への参照。prime はまだ付けていない＝将来 `[greek][0-9]*'*` を `[gDP]` として
!txt     切り出す予定と須田さんから聞いている。今回は範囲を広げない）。
word v-Form  cal[lDP]
word v-Form  [greek][0-9]*
word v_-Form cal[lDP]_
word v_-Form [greek][0-9]*_
word s  greek         index
word p  greek         index
word ?f  \|?\?{1,2}[lDP]
word ?p^ \|?(?:\?_?){1,2}[lDP]\^
word ?c_ \|?(?:\?_?){1,2}[lDP]_

common/default.formel

`common/default.formel`