Up

3.5.1.1 理論の定式化

---

加法の理論は，文生成システムGの上の理論 T＝(G,H,(S,D), (S, D)) としては，以下のように定義される。 Gを，加法に関する等式を生成するシステム (NＶ,TＶ,Ｐ,SEN) として，つぎのように定義する(註1)： NＶ： SEN ：等式生成に関する TRM(註2)，Ｎ ：項生成に関する TＶ＝｛1,＋,＝｝ Ｐ： SEN → TRM＝TRM TRM → TRM＋TRM TRM → Ｎ1 Ｎ → Ｎ1 Ｎ → ε Gと同値な文生成システムH＝(NＶ',TＶ,Ｐ',SEN) は， NＶ'：NＶに Ｌ,Ｒ：それぞれ，項の左，右につくことのできる文字列の生成に関する を追加。 Ｐ' ： SEN → TRM＝TRM TRM → TRM＋TRM TRM → Ｎ1 Ｎ → Ｎ1 Ｎ → ε Ｌ → TRM＋ Ｌ → TRM Ｌ → ε Ｒ → ＋TRM Ｒ → TRM Ｒ → ε Hのシェマシステム S＝( H,σ, R) では， H＝( NＶ, TＶ, Ｐ, SEN) は， NＶ＝： SEN ：SEN に対応 Ｔ, Ｕ, Ｎ, TRM ：項シェマ生成に関する Ｌ,Ｒ ：Ｌ,Ｒに対応 TＶ＝TＶ∪｛trm(註2)，1，λ，ρ｝ Ｐ： SEN → Ｔ＝Ｔ Ｔ → Ｔ＋Ｔ Ｔ → ＴＵ Ｔ → Ｎ1 Ｎ → Ｎ1 Ｎ → ε Ｔ → TRM TRM → TRM1 TRM → trm Ｕ → Ｎ Ｕ → TRM Ｕ → ε Ｌ → λ Ｒ → ρ σ： SEN → SEN TRM → TRM Ｌ → Ｌ Ｒ → Ｒ 代入規則は，原初的代入規則。 Dでは， 変形補助記号は無し。 変形規則は， (a0) ε → 1＝1 (a1) 11 → 1＋1 (a2) 11＋ → 1＋1 (a3) ＝ → 1＝1 Sは， S#＝( G#,σ#, R#) の G#に対し，終端記号に txt を追加し，プロダクションに TXT → TXT1 TXT → txt を追加したもの。 DはD#に同じ。即ち，φを txt＾ あるいは /，ψを ＾txt/ あるいは / ──但し，/ は，テクストの端を表わすメタ記号──とするとき(註3)，(4-2) の (a1) に対応して， Φ：φtrm＝λ11ρψ に対し， Φ → Φ＾trm＝λ1＋1ρ Φ：φλ11ρ＝trmψ に対し， Φ → Φ＾λ1＋1ρ＝trm (a2) に対応して， Φ：φtrm＝λ11＋trm1ψ に対し， Φ → Φ＾trm＝λ1＋1trm1 Φ：φλ11＋trm＝trm1ψ に対し， Φ → Φ＾λ1＋1trm＝trm1 (a3) に対応して， Φ：φtrm＝trm1ψ に対し， Φ → Φ＾trm1＝1trm1 （註１） これは，つぎのように述べられた“式の生成規則”と同じ(§1.6.2.1, 1.6.2.2参照)： 1°１は項である； 2°項Ｕに対し，Ｕ１は項である； 3°項Ｕ,Ｖに対し，Ｕ＋Ｖは項である； 4°項Ｕ,Ｖに対し，Ｕ＝Ｖは式である； 5°1°から4°を有限回適用して導かれる式のみが，式である。 （註２） TRM，trm は,“TeRM(項)"。 （註３） ここでのΦ,φ,ψは，メタ記号である。メタ記号を用いて記述が長くなるのを避けたわけであるが，メタ記号を排除して理論の本来の記述に直すことは，容易である。 　例えば，(a1)に対応する規則をきちんと書けば，つぎのようになる： txt＾trm＝λ11ρ＾txt1 → txt＾trm＝λ11ρ＾txt1＾trm＝λ1＋1ρ txt＾trm＝λ11ρ → txt＾trm＝λ11ρ＾trm＝λ1＋1ρ trm＝λ11ρ＾txt1 → trm＝λ11ρ＾txt1＾trm＝λ1＋1ρ trm＝λ11ρ → trm＝λ11ρ＾trm＝λ1＋1ρ txt＾λ11ρ＝trm＾txt1 → txt＾λ11ρ＝trm＾txt1＾λ1＋1ρ＝trm txt＾λ11ρ＝trm → txt＾λ11ρ＝trm＾λ1＋1ρ＝trm λ11ρ＝trm＾txt1 → λ11ρ＝trm＾txt1＾λ1＋1ρ＝trm λ11ρ＝trm → λ11ρ＝trm＾λ1＋1ρ＝trm