From e0c3d9318fe8ea70fc6f062cfffffea787a8d6d7 Mon Sep 17 00:00:00 2001 From: "Tomoya Matsuura(MacBookPro)" Date: Wed, 30 Aug 2023 00:44:44 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-08-30 00:44:44 --- content/多段階計算.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/content/多段階計算.md b/content/多段階計算.md index 28f39ad7..a70048ee 100644 --- a/content/多段階計算.md +++ b/content/多段階計算.md @@ -31,3 +31,12 @@ http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf ## 依存型との組み合わせ [A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035) + +https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4 + +> Let’s consider an application, for example, in computer graphics, in which we have potentially many pairs of vectors of the fixed (but statically unknown) length and a function—such as vector addition—to be applied to them. +> This function should be fast because it is applied many times and be safe because just one runtime error may ruin the whole long-running calculation. +> Our goal is to define the function `vadd` of type $$Πn : Int.∀β.⊲β(Vector (\%_αn) → Vector (\%_αn) → Vector (\%_αn))$$ +> .It takes the length n and returns (β-closed) code of a function to add two vectors of length n. The generated code is run by applying it to ε to obtain a function of type $Vector\; n → Vector\; n → Vector\; n$ as expected. + +この辺はなんかやりたいことに近そうな予感がする \ No newline at end of file