Binary file paper/final_thesis.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/_Fresh.agda	Mon Feb 15 03:51:35 2021 +0900
@@ -0,0 +1,211 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in
+-- "A Formalised Proof of the Soundness and Completeness of a Simply Typed
+-- Lambda-Calculus with Explicit Substitutions"
+------------------------------------------------------------------------
+
+-- See README.Data.List.Fresh and README.Data.Trie.NonDependent for
+-- examples of how to use fresh lists.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.List.Fresh where
+
+open import Level using (Level; _⊔_)
+open import Data.Bool.Base using (true; false)
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import Data.Product using (∃; _×_; _,_; -,_; proj₁; proj₂)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Function using (_∘′_; flip; id; _on_)
+open import Relation.Nullary      using (does)
+open import Relation.Unary   as U using (Pred)
+open import Relation.Binary  as B using (Rel)
+open import Relation.Nary
+
+private
+  variable
+    a b p r s : Level
+    A : Set a
+    B : Set b
+
+------------------------------------------------------------------------
+-- Basic type
+
+-- If we pick an R such that (R a b) means that a is different from b
+-- then we have a list of distinct values.
+
+module _ {a} (A : Set a) (R : Rel A r) where
+
+  data List# : Set (a ⊔ r)
+  fresh : (a : A) (as : List#) → Set r
+
+  data List# where
+    []   : List#
+    cons : (a : A) (as : List#) → fresh a as → List#
+
+  -- Whenever R can be reconstructed by η-expansion (e.g. because it is
+  -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we
+  -- do not care about the proof, it is convenient to get back list syntax.
+
+  -- We use a different symbol to avoid conflict when importing both Data.List
+  -- and Data.List.Fresh.
+  infixr 5 _∷#_
+  pattern _∷#_ x xs = cons x xs _
+
+  fresh a []        = ⊤
+  fresh a (x ∷# xs) = R a x × fresh a xs
+
+-- Convenient notation for freshness making A and R implicit parameters
+infix 5 _#_
+_#_ : {R : Rel A r} (a : A) (as : List# A R) → Set r
+_#_ = fresh _ _
+
+------------------------------------------------------------------------
+-- Operations for modifying fresh lists
+
+module _ {R : Rel A r} {S : Rel B s} (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where
+
+  map   : List# A R → List# B S
+  map-# : ∀ {a} as → a # as → f a # map as
+
+  map []             = []
+  map (cons a as ps) = cons (f a) (map as) (map-# as ps)
+
+  map-# []        _        = _
+  map-# (a ∷# as) (p , ps) = R⇒S p , map-# as ps
+
+module _ {R : Rel B r} (f : A → B) where
+
+  map₁ : List# A (R on f) → List# B R
+  map₁ = map f id
+
+module _ {R : Rel A r} {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where
+
+  map₂ : List# A R → List# A S
+  map₂ = map id R⇒S
+
+------------------------------------------------------------------------
+-- Views
+
+data Empty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
+  [] : Empty []
+
+data NonEmpty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
+  cons : ∀ x xs pr → NonEmpty (cons x xs pr)
+
+------------------------------------------------------------------------
+-- Operations for reducing fresh lists
+
+length : {R : Rel A r} → List# A R → ℕ
+length []        = 0
+length (_ ∷# xs) = suc (length xs)
+
+------------------------------------------------------------------------
+-- Operations for constructing fresh lists
+
+pattern [_] a = a ∷# []
+
+fromMaybe : {R : Rel A r} → Maybe A → List# A R
+fromMaybe nothing  = []
+fromMaybe (just a) = [ a ]
+
+module _ {R : Rel A r} (R-refl : B.Reflexive R) where
+
+  replicate   : ℕ → A → List# A R
+  replicate-# : (n : ℕ) (a : A) → a # replicate n a
+
+  replicate zero    a = []
+  replicate (suc n) a = cons a (replicate n a) (replicate-# n a)
+
+  replicate-# zero    a = _
+  replicate-# (suc n) a = R-refl , replicate-# n a
+
+------------------------------------------------------------------------
+-- Operations for deconstructing fresh lists
+
+uncons : {R : Rel A r} → List# A R → Maybe (A × List# A R)
+uncons []        = nothing
+uncons (a ∷# as) = just (a , as)
+
+head : {R : Rel A r} → List# A R → Maybe A
+head = Maybe.map proj₁ ∘′ uncons
+
+tail : {R : Rel A r} → List# A R → Maybe (List# A R)
+tail = Maybe.map proj₂ ∘′ uncons
+
+take   : {R : Rel A r} → ℕ → List# A R → List# A R
+take-# : {R : Rel A r} → ∀ n a (as : List# A R) → a # as → a # take n as
+
+take zero    xs             = []
+take (suc n) []             = []
+take (suc n) (cons a as ps) = cons a (take n as) (take-# n a as ps)
+
+take-# zero    a xs        _        = _
+take-# (suc n) a []        ps       = _
+take-# (suc n) a (x ∷# xs) (p , ps) = p , take-# n a xs ps
+
+drop : {R : Rel A r} → ℕ → List# A R → List# A R
+drop zero    as        = as
+drop (suc n) []        = []
+drop (suc n) (a ∷# as) = drop n as
+
+module _ {P : Pred A p} (P? : U.Decidable P) where
+
+  takeWhile   : {R : Rel A r} → List# A R → List# A R
+  takeWhile-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # takeWhile as
+
+  takeWhile []             = []
+  takeWhile (cons a as ps) with does (P? a)
+  ... | true  = cons a (takeWhile as) (takeWhile-# a as ps)
+  ... | false = []
+
+  takeWhile-# a []        _        = _
+  takeWhile-# a (x ∷# xs) (p , ps) with does (P? x)
+  ... | true  = p , takeWhile-# a xs ps
+  ... | false = _
+
+  dropWhile : {R : Rel A r} → List# A R → List# A R
+  dropWhile []            = []
+  dropWhile aas@(a ∷# as) with does (P? a)
+  ... | true  = dropWhile as
+  ... | false = aas
+
+  filter   : {R : Rel A r} → List# A R → List# A R
+  filter-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # filter as
+
+  filter []             = []
+  filter (cons a as ps) with does (P? a)
+  ... | true  = cons a (filter as) (filter-# a as ps)
+  ... | false = filter as
+
+  filter-# a []        _        = _
+  filter-# a (x ∷# xs) (p , ps) with does (P? x)
+  ... | true  = p , filter-# a xs ps
+  ... | false = filter-# a xs ps
+
+------------------------------------------------------------------------
+-- Relationship to List and AllPairs
+
+toList : {R : Rel A r} → List# A R → ∃ (AllPairs R)
+toAll  : ∀ {R : Rel A r} {a} as → fresh A R a as → All (R a) (proj₁ (toList as))
+
+toList []             = -, []
+toList (cons x xs ps) = -, toAll xs ps ∷ proj₂ (toList xs)
+
+toAll []        ps       = []
+toAll (a ∷# as) (p , ps) = p ∷ toAll as ps
+
+fromList   : ∀ {R : Rel A r} {xs} → AllPairs R xs → List# A R
+fromList-# : ∀ {R : Rel A r} {x xs} (ps : AllPairs R xs) →
+             All (R x) xs → x # fromList ps
+
+fromList []       = []
+fromList (r ∷ rs) = cons _ (fromList rs) (fromList-# rs r)
+
+fromList-# []       _        = _
+fromList-# (p ∷ ps) (r ∷ rs) = r , fromList-# ps rs

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/fresh_test.agda	Mon Feb 15 03:51:35 2021 +0900
@@ -0,0 +1,14 @@
+module fresh_test where
+
+open import Data.Nat
+open import Data.List.Base
+open import Data.List.Fresh
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
+open import Data.Product
+open import Relation.Nary using (⌊_⌋; fromWitness)
+
+ISortedList : Set
+ISortedList = List# ℕ ⌊ _>?_ ⌋
+
+ins : ISortedList
+ins = 8 ∷# 4 ∷# 2 ∷# 0 ∷# []

--- a/paper/src/agda/rbt_varif.agda	Sun Feb 14 21:23:12 2021 +0900
+++ b/paper/src/agda/rbt_varif.agda	Mon Feb 15 03:51:35 2021 +0900
@@ -1,4 +1,5 @@
 module rbt_varif where
+
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Binary
 open import Data.Nat hiding (_≤_  ; _≤?_)
@@ -6,6 +7,8 @@
 open import Data.Product
 open import Data.Nat.Properties as NP
 
+
+
 mutual
   data  right-List : Set where
     [] : right-List
@@ -27,7 +30,6 @@
   ... | tri< a ¬b ¬c = (y ∷> ys Cond p)
   ... | tri≈ ¬a b ¬c = (y ∷> ys Cond p)
   ... | tri> ¬a ¬b c = x ∷> (y ∷> ys Cond p) Cond c
-  
 
   data  left-List : Set where
     [] : left-List

--- a/paper/tex/.#rbt_verif.tex	Sun Feb 14 21:23:12 2021 +0900
+++ b/paper/tex/.#rbt_verif.tex	Mon Feb 15 03:51:35 2021 +0900
@@ -1,1 +1,1 @@
-soto@Szeleta.local.353
\ No newline at end of file
+soto@Szeleta.local.855
\ No newline at end of file

--- a/paper/tex/cbc_agda.tex	Sun Feb 14 21:23:12 2021 +0900
+++ b/paper/tex/cbc_agda.tex	Mon Feb 15 03:51:35 2021 +0900
@@ -13,8 +13,31 @@
 
 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg, firstline=6]{src/agda/cbc-agda.agda}
 
+1行目で Data Gear の定義を行っている。
+今回は 2つの数値の足し算を行うコードを実装するため、
+varx と vary の二つの自然数を持つ。
+
+7行目の plus-com が受け取っている値を定義している。
+Env と next と exit を受け取っている。
+
+next と next は Env → t となっているが、
+これは env を受け取って不定の型 (t) を返すという意味である。
+これで 次の関数遷移先を取れるようにしている。
+
+
+9行目から10行目では入ってきた varx で場合分けを行っており、varx が zero ならそのまま vary を返し、次の遷移先へ、
+varx が zero 以外なら varx から1を引いて、vary に 1 を足して遷移する。
+
+13行目でxがzero以外の値であった場合の遷移先を指定している。
+ここでは自身である plus-p をループするように指定した。
+CbCでは再起処理を実装することはできないが、自己呼び出しを行うことはできるので、
+それに合ったようにAgdaでも実装を行なう。
+
+17行目が実際に値を入れる部分になっています。
+Exitが実行の終了になるようにしています。
+
 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
-これがAgdaで表現された CodeGear となる。
+これがAgdaで表現された CodeGear となり、本論では Gears Agda と呼ぶ
 
 \subsection{agda による Meta Gears}
 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。

--- a/paper/tex/future.tex	Sun Feb 14 21:23:12 2021 +0900
+++ b/paper/tex/future.tex	Mon Feb 15 03:51:35 2021 +0900
@@ -1,18 +1,24 @@
-\chapter{今後の課題}
+\chapter{まとめ}
 
-\section{今後の課題}
-今後の課題として、以下が挙げられる。
-RedBlackTree の基本操作として insert や delete が挙げられる。
-通常は、再代入などを用いて実装を行うと思われるが、Agda が変数への代入を許していないため、
-操作後の RedBlackTree を再構成するように実装を行う必要がある。
-その際にどこの状態の検証を行うかが課題になっている。
+本論文では、Agda による CbCの検証方法と Gears Agda による
+Left Learning Red Black Tree の実装について述べた。
+したがって、Gears Agda で再起処理と再代入を含んだ
+複雑なアルゴリズムも記述できる事が判明した。
+今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで
+得られた知見は、今後の研究で大いに役立つと考える。
 
-先行研究にて、
-個々の Code Gear の条件を書いてそれを接続することは Agda で実装されている。
-しかし、接続された条件が健全であるか証明されていない。
+今後の課題として、検証を行う事が挙げられる。
+検証には、Meta Code Gear が Pre / Post Condition の条件を
+満たしているのか比較を行い、Hoare Logicに当てはめる事。
+そして接続された条件の接続と健全性の証明を行う必要がある。
+しかし、Imple を用いた Hoare Logic による証明は、
+While Loop でも かなり長いコードになっていた。
+これで Left Learning Red Black Tree の検証を
+行うのは難しいため、別の手法を模索することも念頭に入れる。
 
-証明されていない部分というのは、プログラム全体はいくつかの Code Gear の集まりだが、
-Code Gear 実行後の事後条件が正しく次に実行される Code Gear の事前条件として成り立っているか、
-それが最初からプログラムの停止まで正しく行われているかという部分である。
+展望としては、Gears Agda コードから CbC コードの変換をしたい。
+Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、
+CbC はC言語の下位言語であり、
 
-今後はこの接続された条件の健全性の証明から行っていく。
+
+

--- a/paper/tex/hoare.tex	Sun Feb 14 21:23:12 2021 +0900
+++ b/paper/tex/hoare.tex	Mon Feb 15 03:51:35 2021 +0900
@@ -34,6 +34,7 @@
   \label{hoare}
 \end{figure}
 
+\begin{comment}
 \section{CbCでの Hoare Logic を用いた検証}
 先行研究で行われている While Loop の Hoare Logic での検証を元に、
 実際の Hoare Logic を用いた検証手法について解説する。
@@ -51,5 +52,6 @@
 % Meta Data Gearのソースコードを貼る
 
 s1 が初期状態、
+\end{comment}
 
 

--- a/paper/tex/rbt_verif.tex	Sun Feb 14 21:23:12 2021 +0900
+++ b/paper/tex/rbt_verif.tex	Mon Feb 15 03:51:35 2021 +0900
@@ -10,15 +10,19 @@
 right node には大きい値が入る。これを検証する必要がある。
 
 大小関係を検証するにあたり、Fresh List を用いた検証手法が考えられた。
-Fresh Listの記述を以下に示す。
+Fresh Listの記述を\coderef{fresh}に示す。
 % ソースコードを載せる。
+\lstinputlisting[label=fresh, caption=Fresh List の定義, firstline=47,lastline=49] {src/agda/_fresh.agda}
+
+これを用いて Frash List への定数の insert を\coderef{fresh-test}に示す。
+\lstinputlisting[label=fresh-test, caption=Fresh List への定数のinsert, firstline=10,lastline=15] {src/agda/fresh_test.agda}
 
 Fresh Listは一つの値に対して、それより後の値との大小関係の証明が入っている。
-そのため、正確性が増すが、Fresh List への insert が困難であったため、
+そのため、正確性が増すが、関数内でFresh List への insert は困難であったため、
 証明付き Data 構造を持った List を \coderef{list_v}
 のように定義した。
 
-\lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=9,lastline=30] {src/agda/rbt_varif.agda}
+\lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=12,lastline=30] {src/agda/rbt_varif.agda}
 証明付き Data 構造を持った List の定義は right-List で行っている。
 List の Top と比較した際に、
 Topの値より大きい値でなければ insert できない。