tomoyanonymous/quartz-research-note
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[obsidian] vault backup: 2023-12-07 17:36:31[

Browse Source
This commit is contained in:
松浦 知也 Matsuura Tomoya 2023-12-07 17:36:32 +09:00
parent 0b9ccfcb7a
commit ef9c255f58
1 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
content/多段階計算.md
View File

@ -43,4 +43,11 @@ https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4
> Our goal is to define the function `vadd` of type $$Πn : Int.∀β.⊲β(Vector (\%_αn) → Vector (\%_αn) → Vector (\%_αn))$$ > 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. > .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.
この辺はなんかやりたいことに近そうな予感がする この辺はなんかやりたいことに近そうな予感がする
## [[Rust]]でのプログラム合成
https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-possible-in-rust.html
impl Return typeと組み合わせたらもっと派手なことできそう