[obsidian] vault backup: 2023-08-25 17:56:00
This commit is contained in:
parent
6251f11943
commit
24ac94be14
@ -8,6 +8,7 @@
|
|||||||
- 神戸大学 [Coq による定理証明入門 髙橋真(2023)](http://herb.h.kobe-u.ac.jp/coq/coq.pdf)
|
- 神戸大学 [Coq による定理証明入門 髙橋真(2023)](http://herb.h.kobe-u.ac.jp/coq/coq.pdf)
|
||||||
- 千葉大学大学院 [定理証明支援系 Coq での 論理的なリーゾニング 集中講義 アフェルト レナルド(2017)](https://staff.aist.go.jp/reynald.affeldt/coq/riron.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)
|
- 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`が変数宣言
|
- `Inductive`が変数宣言
|
||||||
|
@ -2,6 +2,8 @@
|
|||||||
|
|
||||||
https://dl.acm.org/doi/10.1145/3471872.3472970
|
https://dl.acm.org/doi/10.1145/3471872.3472970
|
||||||
|
|
||||||
|
first author: [[Emilio Jesús Gallego Arias]]
|
||||||
|
|
||||||
## 概要
|
## 概要
|
||||||
|
|
||||||
ラムダ計算に`feed`という1サンプルフィードバックを導入する形式を取る
|
ラムダ計算に`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なインタプリタ
|
#### B:Imperativeなインタプリタ
|
||||||
|
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
#programming-language #research
|
#programming-language #research
|
||||||
|
|
||||||
|
|
||||||
## 先行令
|
## 先行例
|
||||||
|
|
||||||
[[Faust]]
|
[[Faust]]
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user