From 24ac94be14f42f54d17aa2fbde6ba2e7a82ca170 Mon Sep 17 00:00:00 2001
From: "Tomoya Matsuura(MacBookPro)" <me@matsuuratomoya.com>
Date: Fri, 25 Aug 2023 17:56:00 +0900
Subject: [PATCH] [obsidian] vault backup: 2023-08-25 17:56:00

---
 content/Coqの勉強.md                          |  1 +
 ...of digital signal processing algorithms.md | 39 +++++++++++++++++++
 content/音楽プログラミング言語の形式化.md     |  2 +-
 3 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/content/Coqの勉強.md b/content/Coqの勉強.md
index 49b7e0b8..38bbab5a 100644
--- a/content/Coqの勉強.md
+++ b/content/Coqの勉強.md
@@ -8,6 +8,7 @@
 - 神戸大学 [Coq による定理証明入門  髙橋真(2023)](http://herb.h.kobe-u.ac.jp/coq/coq.pdf)
 - 千葉大学大学院 [定理証明支援系 Coq での 論理的なリーゾニング 集中講義 アフェルト レナルド(2017)](https://staff.aist.go.jp/reynald.affeldt/coq/riron.pdf)
 - IIJ技術研究所 [Coq を始めよう 池渕未来(2011)](https://www.iijlab.net/activities/programming-coq/coqt1.html)
+- [Real World Coq – An introduction to effective theorem proving](https://ejgallego.github.io/real-world-coq/) by  [[Emilio Jesús Gallego Arias]]
 ## 備忘録
 
 - `Inductive`が変数宣言
diff --git a/content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md b/content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md
index 94a8b1a5..629edcd5 100644
--- a/content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md	
+++ b/content/The w-calculus a synchronous framework for the verified modelling of digital signal processing algorithms.md	
@@ -2,6 +2,8 @@
 
 https://dl.acm.org/doi/10.1145/3471872.3472970
 
+first author: [[Emilio Jesús Gallego Arias]]
+
 ## 概要
 
 ラムダ計算に`feed`という1サンプルフィードバックを導入する形式を取る
@@ -46,6 +48,43 @@ and machine : type a . int → a expr → env → a =
 		|...
 ```
 
+ただし、リポジトリのCoqのコードでは別に相互再帰で実装されてるわけではない
+
+```ocaml
+Definition exprI n (pI : I n) : I n.+1 :=
+  fix eI k hk {Γ t} e {struct e} :=
+  match e in expr Γ t return env k Γ -> tyI k t with
+  | var v Γ idx      => fun Θ => nth (I0 k _) (hnth (hist0 k _) v Θ) idx
+  | add _ _  e1 e2   => fun Θ => eI k hk e1 Θ + eI k hk e2 Θ
+  | mul _ _  c  e    => fun Θ => c *: eI k hk e Θ
+  | pair _ _ _ e1 e2 => fun Θ => col_mx (eI k hk e1 Θ) (eI k hk e2 Θ)
+  | proj m _ i e     => fun Θ => \col__ (eI k hk e Θ) i ord0
+  | lam m _ _ e      => fun Θ v => eI k hk e (v, Θ)
+  | app _ _ _ ef ea  => fun Θ =>
+                        let efI : tyI k (tfun _ _) := eI k hk ef Θ in
+                        let eaI : hist k _ :=
+                            accI (fun k hk => eI k hk ea) hk Θ in
+                        efI eaI
+  | feed tn Γ e      => fun Θ =>
+                        let prev :=
+                            accF (fun k hk => pI k hk _ _ (feed e)) hk Θ in
+                        eI k hk e (prev, Θ)
+  end.
+
+(* Need to prove |acc_feed n.+1| =  acc_norm n ?? *)
+
+(* We build our step-indexed representation *)
+Fixpoint exprIn n {struct n} : I n.+1 :=
+  match n return I n.+1 with
+  | 0    => fun k hk Γ t e (Θ : env k Γ) =>
+            exprI (@IE0 _) hk e Θ
+  | n.+1 => fun k hk Γ t e (Θ : env k Γ) =>
+            exprI (@exprIn n) hk e Θ
+  end.
+
+```
+
+そしてCoqで証明されているのはここまで（MetaOCamlのReal-World exampleが欲しいよ）
 
 #### B:Imperativeなインタプリタ
 
diff --git a/content/音楽プログラミング言語の形式化.md b/content/音楽プログラミング言語の形式化.md
index 584c6086..531338bc 100644
--- a/content/音楽プログラミング言語の形式化.md
+++ b/content/音楽プログラミング言語の形式化.md
@@ -1,7 +1,7 @@
 #programming-language #research 
 
 
-## 先行令
+## 先行例
 
 [[Faust]]