--- a/slide/memo.md	Tue Feb 07 14:49:15 2023 +0900
+++ b/slide/memo.md	Sat Feb 11 22:49:20 2023 +0900
@@ -94,3 +94,37 @@
 # DPPの実装
 pidは哲学者をindexで管理するために必要
 どの哲学者がどのフォークを取るのか決まっているため
+
+# 直すところ
+
+AとかBはここでは型だけど、
+命題だと思っても良い
+並列実行はメタかな。可能な実
+Shinji Kono から全員に 03:40 PM
+引数の説明が雑だな
+TerminatingLoopS 自体の証明も
+コストが高い低いは正確性に欠
+並列実行の検証は難しいけど
+モデル検査自体が並列実行の定
+モデル検査はωオートマトンの実
+仕様は時相論理とかωオートマト
+それを満たすかどうかを証明に
+このdataは、G
+Code GearのProgram Counterみ
+Process (ここではContext)毎にあ
+pickup-lfork は目が潰れるが…
+-c と -p があるのか
+++ は　List の append
+zero 以外のコードは? 以下同様的な?!
+「乱数がでる」?
+分岐の数って、いくつ? 0,1,2 だけ?
+deadlock とかは時相論理の変数だな
+時相論理式を定義して持ち歩くべきだな
+普通は深さ優先探索と状態データベースだが…
+状態が変化し続ける場合はどうなるの?
+exclude-same-env は何を弾くの?
+モデル検査自体の停止性は示せるの?
+DPPでは何が有限なの?
+State List はRedBlack木が良いとは言えない
+
+Agdaでインタプリタではなくコンパイル