# HG changeset patch # User atton # Date 1486974705 -32400 # Node ID ed6719c301fcb0180a44e133aa6e14d670d6b1f4 # Parent d731f2d0947dd4a0ecd05cb82509211b4f65adab Update slide diff -r d731f2d0947d -r ed6719c301fc presentation/images/akashaPut.graffle Binary file presentation/images/akashaPut.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/akashaPut.pdf Binary file presentation/images/akashaPut.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/akashaPut.svg --- a/presentation/images/akashaPut.svg Mon Feb 13 17:15:10 2017 +0900 +++ b/presentation/images/akashaPut.svg Mon Feb 13 17:31:45 2017 +0900 @@ -74,7 +74,7 @@ - + @@ -83,7 +83,7 @@ - + @@ -120,7 +120,7 @@ - + @@ -142,7 +142,7 @@ - + diff -r d731f2d0947d -r ed6719c301fc presentation/images/cs.graffle Binary file presentation/images/cs.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/cs.pdf Binary file presentation/images/cs.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/cs.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/cs.svg Mon Feb 13 17:31:45 2017 +0900 @@ -0,0 +1,86 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r d731f2d0947d -r ed6719c301fc presentation/images/csds.pdf Binary file presentation/images/csds.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/csds.svg --- a/presentation/images/csds.svg Mon Feb 13 17:15:10 2017 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,107 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff -r d731f2d0947d -r ed6719c301fc presentation/images/ds.graffle Binary file presentation/images/ds.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/ds.pdf Binary file presentation/images/ds.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/ds.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/ds.svg Mon Feb 13 17:31:45 2017 +0900 @@ -0,0 +1,107 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r d731f2d0947d -r ed6719c301fc presentation/images/mcs.graffle Binary file presentation/images/mcs.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/mcs.pdf Binary file presentation/images/mcs.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/mcs.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/mcs.svg Mon Feb 13 17:31:45 2017 +0900 @@ -0,0 +1,162 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r d731f2d0947d -r ed6719c301fc presentation/images/mds.graffle Binary file presentation/images/mds.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/mds.pdf Binary file presentation/images/mds.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/mds.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/mds.svg Mon Feb 13 17:31:45 2017 +0900 @@ -0,0 +1,162 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r d731f2d0947d -r ed6719c301fc presentation/images/meta.graffle Binary file presentation/images/meta.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/put.graffle Binary file presentation/images/put.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/put.pdf Binary file presentation/images/put.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/put.svg --- a/presentation/images/put.svg Mon Feb 13 17:15:10 2017 +0900 +++ b/presentation/images/put.svg Mon Feb 13 17:31:45 2017 +0900 @@ -53,7 +53,7 @@ - + @@ -90,7 +90,7 @@ - + diff -r d731f2d0947d -r ed6719c301fc presentation/images/rbtree.graffle Binary file presentation/images/rbtree.graffle has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/rbtree.pdf Binary file presentation/images/rbtree.pdf has changed diff -r d731f2d0947d -r ed6719c301fc presentation/images/rbtree.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/rbtree.svg Mon Feb 13 17:31:45 2017 +0900 @@ -0,0 +1,103 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r d731f2d0947d -r ed6719c301fc presentation/slide.html --- a/presentation/slide.html Mon Feb 13 17:15:10 2017 +0900 +++ b/presentation/slide.html Mon Feb 13 17:31:45 2017 +0900 @@ -86,7 +86,7 @@ @@ -167,7 +167,7 @@
  • CodeSegment どうしを接続することによりプログラム全体を作る
    • -

    goto

    +

    cs

    @@ -184,7 +184,7 @@ -

    csds

    +

    ds

    @@ -212,9 +212,10 @@
    • メタ計算を行なう CodeSegment
    • 通常の CodeSegment どうしの接続の間に入る
      • -
    • TODO: 図
    +

    mcs

    +
    @@ -223,9 +224,10 @@
    • メタ計算用の DataSegment
    • 通常の DataSegment を含むような DataSegment
      • -
    • TODO: 図
    +

    mds

    +
    @@ -252,9 +254,10 @@
  • ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定
    • -
  • TODO: 図
    • +

    rbtree

    +
    @@ -444,7 +447,10 @@ goto cs1(a+b); } -
    cs0 : CodeSegment ds0 ds1
+
    data CodeSegment (A B : Set) : Set where
+  cs : (A -> B) -> CodeSegment A B
+
+cs0 : CodeSegment ds0 ds1
 cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
 
    
 
diff -r d731f2d0947d -r ed6719c301fc presentation/slide.md
--- a/presentation/slide.md	Mon Feb 13 17:15:10 2017 +0900
+++ b/presentation/slide.md	Mon Feb 13 17:31:45 2017 +0900
@@ -42,7 +42,7 @@
     * 入力と出力を持つ
 * CodeSegment どうしを接続することによりプログラム全体を作る
 
-![goto](./images/goto.svg){:width="50%"}
+![cs](./images/cs.svg){:width="50%"}
 
 
 # DataSegment
@@ -51,7 +51,7 @@
     * CodeSegment の入出力にあたる
     * 接続元の Output DataSegment は接続先の Input DataSegment
 
-![csds](./images/csds.svg){:width="50%"}
+![ds](./images/ds.svg){:width="50%"}
 
 # メタ計算
 * とある計算を実現するための計算
@@ -65,12 +65,14 @@
 # Meta CodeSegment
 * メタ計算を行なう CodeSegment
 * 通常の CodeSegment どうしの接続の間に入る
-* TODO: 図
+
+![mcs](./images/mcs.svg){:width="50%"}
 
 # Meta DataSegment
 * メタ計算用の DataSegment
 * 通常の DataSegment を含むような DataSegment
-* TODO: 図
+
+![mds](./images/mds.svg){:width="50%"}
 
 # 並列に信頼性高く動作する GearsOS
 * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
@@ -84,7 +86,8 @@
     * ルートノードと葉ノードの色は黒
     * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)
     * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定
-* TODO: 図
+
+![rbtree](./images/rbtree.svg){:width="50%"}
 
 # GearsOS における赤黒木の利用例(ノードの挿入)
 * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
@@ -184,6 +187,9 @@
 }
 ```
 ```
+data CodeSegment (A B : Set) : Set where
+  cs : (A -> B) -> CodeSegment A B
+
 cs0 : CodeSegment ds0 ds1
 cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
 ```
diff -r d731f2d0947d -r ed6719c301fc presentation/slide.pdf.html
--- a/presentation/slide.pdf.html	Mon Feb 13 17:15:10 2017 +0900
+++ b/presentation/slide.pdf.html	Mon Feb 13 17:31:45 2017 +0900
@@ -70,7 +70,7 @@
 
 
@@ -151,7 +151,7 @@
   
  • CodeSegment どうしを接続することによりプログラム全体を作る
    • 
 
 
-
    goto
    
+
    cs
    @@ -168,7 +168,7 @@ -

    csds

    +

    ds

    @@ -196,9 +196,10 @@
    • メタ計算を行なう CodeSegment
    • 通常の CodeSegment どうしの接続の間に入る
      • -
    • TODO: 図
    +

    mcs

    +
    @@ -207,9 +208,10 @@
    • メタ計算用の DataSegment
    • 通常の DataSegment を含むような DataSegment
      • -
    • TODO: 図
    +

    mds

    +
    @@ -236,9 +238,10 @@
  • ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定
    • -
  • TODO: 図
    • +

    rbtree

    +
    @@ -428,7 +431,10 @@ goto cs1(a+b); } -
    cs0 : CodeSegment ds0 ds1
+
    data CodeSegment (A B : Set) : Set where
+  cs : (A -> B) -> CodeSegment A B
+
+cs0 : CodeSegment ds0 ds1
 cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))