Up 3.5.2.1 理論の定式化  

　二進数の加算の妥当な等式を生成する理論が，つぎのように定義できる。

  1. 二進数の加算の等式を，文生成システムG＝（NＶ,TＶ,Ｐ,SEN）の生成するものと見なす。ここで，
    NＶ：
    SEN：等式生成に関する
    TRM：項生成に関する
    NUM(註1)：数生成に関する
    STR(註2)：数記号の列の生成に関する

    TＶ＝｛1，0，＋,＝｝
    Ｐ：
    SEN→TRM＝TRM
    TRM→TRM＋NUM
    TRM→NUM
    NUM→0
    NUM→1STR
    STR→STR0
    STR→STR1
    STR→ε


  2. Hは，GのNＶに
    Ｕ ：一位数生成に関する
    を追加し，Ｐに
    Ｕ → 0
    Ｕ → 1
    を追加したもの。

  3. Hのシェマシステム S＝( H,σ, R) では，

    1. H＝( NＶ, TＶ, Ｐ, SEN) は，
      NＶ：
        SEN：等式シェマ生成に関する
        TRM：項シェマ生成に関する
        NUM：数生成に関する
        STR：数記号の列の生成に関する
        Ｕ：Ｕに対応

      TＶ＝TＶ∪{φ,ν,ｍ,ｎ,ｓ,ｔ｝

      Ｐ：
      SEN → TRM＝TRM
      TRM → TRM＋NUM
      TRM → NUM
      NUM → 0
      NUM → 1STR
      STR → STR0
      STR → STR1
      STR → ε
      SEN → φ
      NUM → ν
      STR → ｓ
      STR → ｔ
      Ｕ → ｍ
      Ｕ → ｎ

    2. σ：
      SEN → SEN
      NUM → NUM
      STR → STR
      Ｕ → Ｕ

    3. 代入規則は原初的代入規則。


  4. D＝(ＶD,Ｄ) を，つぎのように定義する：

    1. ＶD＝｛＄，＃，1｝
    2. Ｄ：
      (00)　ε→1＝1
      (01)　＝→＋1＝1＋
      (a1)　＾ｓ＋ｔ＝→＾＄ｓ＋ｔ＄＝
      (a2)　＾ｓ＋ｔ＋→＾＄ｓ＋ｔ＄＋
      (a3)　＝ｓ＋ｔ/→＝＄ｓ＋ｔ＄/
      (a4)　＝ｓ＋ｔ＋→＝＄ｓ＋ｔ＄＋
      (a5)　＋ｓ＋ｔ＋→＋＄ｓ＋ｔ＄＋
      (b1)　＄ｓｍ＋ｔｎ＄→＄ｓ＋ｔ＃ｍ＋ｎ＃＄
      (b2)　＄ｓｍ＋ｔｎ＃→＄ｓ＋ｔ＃ｍ＋ｎ＃
      (c1)　＃0＋ｎ＃→＃ｎ
      (c2)　＃1＋0＃→＃1
      (c3)　＃1＋1＃→1＃0
      (d1)　＋1→＋1
      (d2)　01→1
      (d3)　11→10
      (e1)　＄ｓ＋＃→＄ｓ
      (e2)　＄＋ｓ＃→＄ｓ
      (e3)　＄＋＃→＄
      (f)　＄ｓ＄→ｓ

      ここで“/”は，式の端を示すメタ記号である（変形補助記号ではない)。


  5. Sは， S#＝( H#,σ#, R＃) の H#に対し，終端記号に
    txt，1
    を追加し，プロダクションに
    TXT →TXT1
    TXT → txt
    を追加したもの。

  6. Dは，D#と同じ。



（註１） NUM は,“NUMber(数)"。

（註２） STR は,“STRing(記号列)"。