未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
0_tutorial/2.book
ヘッダ
行番号
title Formel author admin formel /common/default
section Formel の基本 subsection wordとForm txt ヘッダで .formelファイル を指定すると <i>Formel</i> が使用できます。 txt このBookでは <span style="color:brown">formel /common/default</span> とあり default.formel が読み込まれます。 br txt <i>Formel</i> で使われる記号を<b>word</b>と言い、「wordの列」のうち<note>文法をみたすもの<?>Formの正確な定義をしようとするととても長くなります…私たちは機械で言語を扱っています。だから実用的には「Form checkをしてOKならForm」です。</note>を<b>Form</b>と言います。 txt default.formelでは <span style="color:brown">form s c p</span> とあります。Formに <note>s-Form, c-Form, p-Form<?>set, class, proposition</note> があるという宣言です。 txt <span style="color:brown">s p</span> は必ず含めなければなりません。<span style="color:brown">s c p</span> 以外の種類は今のところありません。 txt Formは <span style="color:red">高階{s,c}ソート言語</span> になります（一階部分しか使わないことが多いでしょうが）。 subsection wordの基本 txt 通常、wordは <i>DB</i> に登録されているものを呼び出し、Bookで「紹介」してから使用します。 txt ソースで <code>word ∈</code> のように word で始まる行を書くと紹介できます。次の行がそれです。 word ∈ txt (ss,p) はgramです。wordはtexというデータも持ち、`∈` のtexは \in です。 txt gramやtexは<i>DB</i>に保存されています。自分でwordを作るときは、gramとtexも用意する必要があります。 txt gram (〇,△) の〇の文字数を arity と言うことがあります。`∈` のarityは2です。 br txt <span style="color:red">texが同じでも異なるwordがありますので、こまめにクリックをして確認して下さい。</span>次のwordも<i>DB</i>にあります。 word ∈_ br txt gramが同じwordはまとめて紹介できます。例えば次の2項命題結合子があります。 word and or ⇒ ⇔ txt wordは表記法（詳しくは下の「いろいろな表記法」）というデータも持っており、紹介時にgramの右に付くことがあります。次の R など。 word ∀ subsection 正規表現 txt 英字1文字を <span style="color:brown">[A-Za-z]</span>、数字を <span style="color:brown">[0-9]</span> のように表します。 txt <span style="color:brown">*</span> は0個以上の繰り返しを意味します。10進法での自然数とは <span style="color:brown">[1-9][0-9]*</span> と言えます。 txt letter Digit Prime <span style="color:brown">[lDP]</span> = <span style="color:brown">[A-Za-z][0-9]*'*</span> txt 全角letter Digit Prime<span style="color:brown">[ｌDP]</span> = <span style="color:brown">[Ａ-Ｚａ-ｚ][0-9]*'*</span> txt ギリシャ文字 greek = [αβγδεζηθικλμνξπρστυφχψωΓΔΘΛΞΠΣΥΦΨΩ] section 色々なwordとForm subsection 変数・定数 txt 変数は特別なwordであり.formelに登録されます。default.formelには次が登録されています。 txt v-Form (gramは(,s)) … <span style="color:brown">[lDP]</span> txt v_-Form (gramは(,c)) … <span style="color:brown">[lDP]_</span> txt v^-Form (gramは(,p)) … <span style="color:brown">[lDP]^</span> txt `x ∈ X`, `x ∈_ X_` はp-Formですが `x_ ∈_ X_` はFormでないです。`∀ x P^` はp-Formです。 txt （表示では3つとも同じに見えます。ソースではそれぞれ <code>x ∈ X</code>・<code>x ∈_ X_</code>・<code>x_ ∈_ X_</code> です。∈_ の左にはs-Formしか置けず、x_ はc-Formなので3つ目はFormになりません。） txt v^-Formは高階言語の記号です（一階論理の通常の教科書ではメタ記号という扱い）。 txt v^-Form や下の ?v-Form を含む Thm も、prf で p;（prover+）に投げられます。投げる前に定数へ置き換えて一階のThmにします（3.book「高階変数の定数化」）。 br txt 定数も登録されています。変数の先頭に | を付けるだけです。 txt word(,s) … <span style="color:brown">|[lDP]</span> txt word(,c) … <span style="color:brown">|[lDP]_</span> txt word(,p) … <span style="color:brown">|[lDP]^</span> txt `|x ∈ X`, `x ∈_ |X_` もp-Formです。`∀ |x P^` はFormでないです。 subsection いろいろな表記法 txt Formのtxtにおいて半角スペースがwordの区切りになります。 txt ただし `(` `)` の前後だけは、半角スペースを省略できます。例 `x ∈ (X)` br txt wordの結合力の差は自然に利用されます。例 `x = y ⇒ y = x` ≈ `(x = y) ⇒ (y = x)` txt 結合力の等しいものは通常は左から読まれます。例 `P^ and Q^ and R^` ≈ `(P^ and Q^) and R^` txt 表記法がRのwordは右結合で、例えば `∀ x ∀ y P^` ≈ `∀ x (∀ y P^)` txt 量化子がどこまで及ぶか迷うときは、`∀ x (x ∈ A ⟹ x ∈ B)` のように範囲を括弧で囲みます。 txt 表記法がFのword \({\tt w}\) は \({\tt w}\)(\({\tt x}_1\) , … , \({\tt x}_n\)) の形で使用されます。 txt 仮に自分のBookで `∈` を word(ss,p)F としたら、常に `∈ (x , X)` のように使用しなければなりません。 subsection arityが正の変数・定数 txt arityが正(i.e. 引数を持つ)変数も準備されています。これも高階言語の記号です txt ? はs-Formを引数、?_ はc-Formを引数とすることを表します。例えば txt ?v-Form (gramは(s,s)) … <span style="color:brown">?[lDP]</span> txt 表記法はFです。`?f (x)` はs-Formです。 br txt |をつければ定数になります。例えば txt word(sc,p)F … <span style="color:brown">|??_[lDP]^</span> newpage section 高レベルの表現 subsection 穴 txt 数学は記号列を変形していくゲームです。「記号列の変形の規則」もまた表現されます。 txt 「規則が使用される際にFormが代入されるもの」を「Formの穴」と言い、次が使用されます。 txt Formの穴 … <span style="color:brown">$[lDP]</span> txt 例えば「`or` の前後をひっくり返す」という規則は `$P or $Q` → `$Q or $P` br txt v-Formの穴 … <span style="color:brown">[ｌDP]</span> txt v_-Formの穴 … <span style="color:brown">[ｌDP]_</span> txt wordの列の穴 … <span style="color:brown">$_[lDP]</span> subsection tex計算とFCL変換 txt ★<i>Formel</i> はFormの入力に対し2方向の処理をします。tex表記の計算 と <code>FCL</code>(Formel Core Language)への変換 です。FCLは略記などを処理し終えた形で、backendに渡す式はFCLから翻訳して作られます。 txt default.formelには \, \; \! !, { } _ ^ が <span style="color:brown">word tex_only</span> に登録されています。 txt これらはtex表示のためだけに使われます(<code>FCL</code>変換では無視)。例 `x { ∈ } X` br txt 一般に<b>word+</b>として紹介されるwordは高度な表現の為にあり、<code>FCL</code>変換では<b>lower</b>という規則で処理されます。 txt 最も簡単な例に<b>alias word</b>があります。何らかの目的で作られた「<code>FCL</code>変換では同一視されるword」です。次の例はtexが異なるだけの `and` のaliasです。 txt word+(pp,p) … <note>\(\text{and}\)<?>and*</note> txt lower … <note>\(P \mathop{\text{and}} Q\)<?>$P and* $Q</note> ≃ `$P and $Q` subsection 結合力が異なるだけの論理記号 alias word and_ ⟹ ⟺ lower and_ lower ⟹ lower ⟺ br txt 実はarityが1以上のwordにはprecedというデータも付きます。 txt 大小関係が意味を持ち、 `¬` < `⇒` `⇔` < `and` `or` < `⟹` `⟺` < `and_` となっています(precedが大きいほど結合力が弱い)。 txt 例 `P^ ⇒ Q^ ⟺ ¬ P^ or Q^` ≃ `(P^ ⇒ Q^) ⇔ (¬ P^ or Q^)` txt <b>注意</b>：`⇒` は `and` より強く結合します（ふつうの数学の書き方と逆です）。<code>P^ and Q^ ⇒ R^</code> は <code>P^ and (Q^ ⇒ R^)</code> と読まれます。「P かつ Q ならば R」は <code>P^ and Q^ ⟹ R^</code>（⟹ は and より弱い）と書くか、括弧を付けます（どちらも査読で確かめました）。 !txt 正確には<code>FCL</code>変換の結果は、機械に扱いやすい prefix形・入れ子配列 です。 !txt 現状ではwordのprecedを操作する機能はありません… !txt .formelでの機能宣言 <span style="color:brown">lower on</span> にする？ subsection 省略表現 txt 省略表現も使用可能です。<code>FCL</code>変換では<b>abbr</b>という規則で処理されます。 abbr col txt `\n` は自然数が代入されるものです。`\n-1`なども利用できます。 txt 例 `[ x ; y col ∈ A ]` ≈ `x ∈ A and y ∈ A` txt abbr は、word と同じように紹介してから使います。col と ∀ などの abbr は <code>import /common/word_logic</code> で紹介済みなので、その Book を import すれば書かずに使えます（書いても構いません）。 br txt 量化子の省略表現も用意されています。 abbr ∀
表示（保存しません）
保存にはMatheliaへのログインが要ります。