From 9b0eedab1169a6aa6a6d983658727a43295277f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?= =?UTF-8?q?a?= Date: Thu, 29 Jan 2026 12:55:09 +0900 Subject: [PATCH] [obsidian] vault backup: 2026-01-29 12:55:09[ --- content/多段階計算.md | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/content/多段階計算.md b/content/多段階計算.md index ecef8095..df1285fc 100644 --- a/content/多段階計算.md +++ b/content/多段階計算.md @@ -16,7 +16,7 @@ https://logmi.jp/tech/articles/324146 MetaOCaml を使った自己反映言語のコンパイル 浅井 健一 (Black ) http://www.is.ocha.ac.jp/~asai/jpapers/ppl/asai14.pdf -メタプログラミングのための時相論理に基づく型付 λ 計算 湯瀬 芳洋 五十嵐 淳 +メタプログラミングのための時相論理に基づく型付 λ 計算 湯瀬 芳洋 [[五十嵐淳]] http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/papers/pdf/lambdaCB-PPL05.pdf 筑波大学　論理と計算（2） @@ -42,7 +42,21 @@ http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf **Cross-Stage Persistence**：基本的にステージ0/1でのコードはそれぞれステージ0/1の中でしか使えない。何らかの方法で両方のステージで跨いで使える仕組みを作れると便利 -**Run**プリミティブ： +[multi-stage-programs-in-context.pdf](https://mpickering.github.io/papers/multi-stage-programs-in-context.pdf) + +Path Based Persistence: グローバルレベルで定義されたシンボルはどのステージでも使えるようにする + +Serialisation-based persistence + +各プリミティブにliftという関数を用意して、値→値リテラルのコードを変換できるようにする。構造体などは各フィールドを再帰的にliftしたものになる。 + +問題は関数丸ごとリフトするような一般的な方法がないことである。 + +例えばこんなコードだったら + +``let x = `(x+1) `` + +``let x = `($(lift(x) + 1))` ``であってほしい。これは構文木を再帰的に辿れば一応できそう ## [[依存型]]との組み合わせ @@ -58,6 +72,15 @@ https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4 この辺はなんかやりたいことに近そうな予感がする +## [[モジュール]]システムとの組み合わせ + +[A Research Talk at FLOPS 2024: An ML-Style Module System for Cross-Stage Type Abstraction in Multi-Stage Programs - gfnweb](https://gfngfn.github.io/posts/2024-05-18-slides-flops2024/) + +[[Suwa Takashi]] + + + + ## [[Rust]]でのプログラム合成 https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-possible-in-rust.html