Skip to content

Milestones

List view

  • Admissibleな簡約形を全列挙する

    [目標] 与えられた任意の(+,-の)記号列の admissibility を判定する。 [公理] 簡約規則の前後で admissibility は変わらない。 （Coq で未証明ですが、待遇をとることで証明できるかもしれない） [定理] 簡約形の形は制限されている。 （証明済） したがって、 [目標’] したがって簡約形の上で admissibility を判定する admissibility を調べるのですから簡約形が　admissibisile かどうかはわかりません。 ただし、rotation difference (記号列に含まれる+,-の個数の差) が 3 以下だという 条件が加わります。 [公理] rotation difference が 4 以上のときは non-admissible である （一般の回転角の性質からこれは公理として認める。論文でもそうしている。） [補題] 簡約形の長さが 8 以上ならば rotation difference は 4 以上になる。 [定理] 簡約形の中で rotation difference が 3 以下のものは（同値類を考えると）11種類である。

    No due date
    •4/4 issues closed
    100% complete0 open4 closed

  • Proposition 3a. reduced form

    ReduceDirをこれ以上できないまで行った最終形が必ず次のような形をしていることを示す: (一つまたはゼロ個の `+`) (一つ以上の連続する`-`の列) (一つまたはゼロ個の `+`) またはその `+`と `-` を逆にしたもの

    No due date
    •6/6 issues closed
    100% complete0 open6 closed

  • Proposition 4. ReduceDirの local confluence 局合流性

    強正規化性が成り立つ (https://github.com/proof-ninja/coq-scurve/milestone/1) ため、局合流性(弱チャーチロッサー性)だけ示せば十分。 ```coq Notation have_common_reduce ds1 ds2 := exists ds', ReduceDir ds1 ds' /\ ReduceDir ds2 ds'. Lemma ReduceDir_local_confluence ds ds1 ds2: ReduceDir_step ds ds1 -> ReduceDir_step ds ds2 -> have_common_reduce ds1 ds2. ```

    No due date
    •8/8 issues closed
    100% complete0 open8 closed

  • Proposition 1. RecuceDirの停止性

    ```coq Lemma termination : forall x, exists final, ReduceDir x final /\ ~ CanReduceDirStep final. Proof. ... Qed. ```

    No due date
    •10/10 issues closed
    100% complete0 open10 closed