Keigo Imai
@keigoi.bsky.social
プロセス計算のトレースで表示的意味論を作るやつ。ドメインとしてなんらかのposetを選び、演算子の意味はその上の単調関数にする。オートマトンだと受理する語の集合とその包含関係だけど、プロセス計算ではトレース*1のprefix closureとその包含関係を使う。ループX=F(X)の意味は最小不動点µX.F(X)とする。無限のトレースはprefix関係のlubを取れば得られるのでその情報自体は実質的にもとの集合に含まれている。
(*1オートマトンの文脈でいうMazurkiewiczトレースではなく単なるアルファベットの列。そもそもプロセス計算には陽な受理状態がないので語の概念もない)
(*1オートマトンの文脈でいうMazurkiewiczトレースではなく単なるアルファベットの列。そもそもプロセス計算には陽な受理状態がないので語の概念もない)
Bill Roscoe本p.36: It is natural to model an untimed CSP process by the set of all traces it can perform. It turns out that recording only finite traces is sufficient in the majority of cases – after all, if u is an infinite trace then all its finite prefixes (initial subsequences) are finite traces…
November 1, 2024 at 12:27 AM
プロセス計算のトレースで表示的意味論を作るやつ。ドメインとしてなんらかのposetを選び、演算子の意味はその上の単調関数にする。オートマトンだと受理する語の集合とその包含関係だけど、プロセス計算ではトレース*1のprefix closureとその包含関係を使う。ループX=F(X)の意味は最小不動点µX.F(X)とする。無限のトレースはprefix関係のlubを取れば得られるのでその情報自体は実質的にもとの集合に含まれている。
(*1オートマトンの文脈でいうMazurkiewiczトレースではなく単なるアルファベットの列。そもそもプロセス計算には陽な受理状態がないので語の概念もない)
(*1オートマトンの文脈でいうMazurkiewiczトレースではなく単なるアルファベットの列。そもそもプロセス計算には陽な受理状態がないので語の概念もない)
金田家だ Holbornからテクテクあるいた記憶
October 19, 2024 at 1:46 AM
金田家だ Holbornからテクテクあるいた記憶
Reposted by Keigo Imai
British traditional TonkotsuX
October 18, 2024 at 1:33 PM
British traditional TonkotsuX
OCaml: Deriving show for GADTs (wip) github.com/ocaml-ppx/pp...
Deriving show for GADTs (wip) by keigoi · Pull Request #290 · ocaml-ppx/ppx_deriving
(TBA)
github.com
October 16, 2024 at 4:01 PM
OCaml: Deriving show for GADTs (wip) github.com/ocaml-ppx/pp...
Blog: Looks like I am genuinely the first person to try and apply "Trees that grow" to OCaml cohost.org/prophet/post... 多相ヴァリアント以外のやつ (多相ヴァリアントのはでこれきさんの qiita.com/dico_leque/i...
Looks like I am genuinely the first person to try and apply
I've spend a lot of time trying to do this now, but I'm fairly convinced it's just not possible with modules.
Superficially, it seems like Trees That Grow would be an amazing fit for functors!
The a...
cohost.org
August 31, 2024 at 11:54 AM
Blog: Looks like I am genuinely the first person to try and apply "Trees that grow" to OCaml cohost.org/prophet/post... 多相ヴァリアント以外のやつ (多相ヴァリアントのはでこれきさんの qiita.com/dico_leque/i...
カードゲームのプロトコルをセッションタイプで…
June 29, 2024 at 3:13 AM
カードゲームのプロトコルをセッションタイプで…
subset constructionの汎用性よ
June 8, 2024 at 9:02 PM
subset constructionの汎用性よ
未だに最小不動点定理の説明に迷いが生じる。周りの人に話そうと突き詰めていくと、やはり無限集合の直観的な把握とそれをどうやって論理で捉えるかといったところで少し修行が足りてない。ある集合が「任意の無限部分集合についてlubやglbをとる操作がある」という集合であれば、単調な関数を使ってさまざまな不動点を使った構成が可能になる
May 31, 2024 at 7:54 PM
未だに最小不動点定理の説明に迷いが生じる。周りの人に話そうと突き詰めていくと、やはり無限集合の直観的な把握とそれをどうやって論理で捉えるかといったところで少し修行が足りてない。ある集合が「任意の無限部分集合についてlubやglbをとる操作がある」という集合であれば、単調な関数を使ってさまざまな不動点を使った構成が可能になる
lptk.github.io/programming/... Demystifying MLsub — the Simple Essence of Algebraic Subtyping
𝐖ell-𝚻yped 𝐑eflections
lptk.github.io
May 30, 2024 at 11:32 PM
lptk.github.io/programming/... Demystifying MLsub — the Simple Essence of Algebraic Subtyping
証明フェーズに入ったので脳内で帰納法を回そうとしたところ回らない。ちょっとゆるめないといかん
May 30, 2024 at 5:49 PM
証明フェーズに入ったので脳内で帰納法を回そうとしたところ回らない。ちょっとゆるめないといかん
無限ストリームを順序イデアルで扱うお話を学んだ. B. Möller, Ideal Stream Algebra, Prospects for Hardware Foundations (LNCS 1546), 1998 opus.bibliothek.uni-augsburg.de/opus4/26230
Ideal stream algebra
We provide some mathematical properties of behaviours of systems, where the individual elements of a behaviour are modeled by ideals, ie. downward closed directed subsets of a suitable partial order. ...
opus.bibliothek.uni-augsburg.de
May 29, 2024 at 11:59 PM
無限ストリームを順序イデアルで扱うお話を学んだ. B. Möller, Ideal Stream Algebra, Prospects for Hardware Foundations (LNCS 1546), 1998 opus.bibliothek.uni-augsburg.de/opus4/26230
放置してたThe Book of Traces (Diekert and Rozenberg, ed., 1995) を開いてる。似たようなトピックを扱うにも関わらずプロセス計算とは道具立てがかなり違う。オートマトン寄り？最初にinterleavingのアプローチの欠点が1ページ分くらいかけて載っていた。(1)排他的選択と独立した複数の実行を区別できない(≒causalityがわからない),(2)仕様から実装へのrefinementをうまく扱えない(これは根拠不明),(3)(説明はよくわからないが)fairness特別な扱いが必要,(4)理由(1)からDBのトランザクションの扱いがむずい
May 29, 2024 at 7:35 PM
放置してたThe Book of Traces (Diekert and Rozenberg, ed., 1995) を開いてる。似たようなトピックを扱うにも関わらずプロセス計算とは道具立てがかなり違う。オートマトン寄り？最初にinterleavingのアプローチの欠点が1ページ分くらいかけて載っていた。(1)排他的選択と独立した複数の実行を区別できない(≒causalityがわからない),(2)仕様から実装へのrefinementをうまく扱えない(これは根拠不明),(3)(説明はよくわからないが)fairness特別な扱いが必要,(4)理由(1)からDBのトランザクションの扱いがむずい
GADT, レンズ, 再帰モジュールなどの型マジックを使いすぎて本当に頭抱えてて2年が経った。整理してどこかに出さないといかん https://github.com/keigoi/ocaml-mpst
GitHub - keigoi/ocaml-mpst: Multiparty Session Types in OCaml
Multiparty Session Types in OCaml. Contribute to keigoi/ocaml-mpst development by creating an account on GitHub.
github.com
May 26, 2024 at 11:58 PM
GADT, レンズ, 再帰モジュールなどの型マジックを使いすぎて本当に頭抱えてて2年が経った。整理してどこかに出さないといかん https://github.com/keigoi/ocaml-mpst
Handbook of Process Algebra を開いている
May 23, 2024 at 10:19 AM
Handbook of Process Algebra を開いている
Algebraic Subtyping (Stephen Dolan, PhD thesis, 2016) (なぜか Cambridge にはない) www.cs.tufts.edu/~nr/cs257/ar... subtyping relation の lattice について調べていた。
www.cs.tufts.edu
May 17, 2024 at 12:31 AM
Algebraic Subtyping (Stephen Dolan, PhD thesis, 2016) (なぜか Cambridge にはない) www.cs.tufts.edu/~nr/cs257/ar... subtyping relation の lattice について調べていた。
業務でシーケンス図で仕様を書くのでセッション型活用の機運をひしひしと感じている。まだ書きたいことがあるぞー
April 21, 2024 at 6:15 AM
業務でシーケンス図で仕様を書くのでセッション型活用の機運をひしひしと感じている。まだ書きたいことがあるぞー
Reposted by Keigo Imai
シュタイフでかわいいカニ買ったから見て（上下どちらにひっくり返しても楽しめる）
September 22, 2023 at 8:51 PM
シュタイフでかわいいカニ買ったから見て（上下どちらにひっくり返しても楽しめる）
ロンドン2019年夏のあいだどう暑さをしのいでたのかあまり思い出せない。わりとUxbridge (Brunel) とかの郊外に居て暑さをあまり感じなかったのかもしれない。たまに車借りて海行ったり電車で周辺の街に行ったりしたけどやはり耐えられないくらい暑かった記憶はない。でもその前の年は暑すぎて公園の芝生が死に絶えそうだったとは聞いた。なんにせよ水はしっかり持ち歩いてた気はする…！
September 8, 2023 at 9:26 PM
ロンドン2019年夏のあいだどう暑さをしのいでたのかあまり思い出せない。わりとUxbridge (Brunel) とかの郊外に居て暑さをあまり感じなかったのかもしれない。たまに車借りて海行ったり電車で周辺の街に行ったりしたけどやはり耐えられないくらい暑かった記憶はない。でもその前の年は暑すぎて公園の芝生が死に絶えそうだったとは聞いた。なんにせよ水はしっかり持ち歩いてた気はする…！
1,2章と残りの章の間で無限に反復横跳びしてる
セッション型とかのような、TaPLでいう同値再帰型をちょっと深く理解するため時相論理でない純粋な(?) μ計算の本を探していて、しばらく前に誰かの論文から引用されているこの本 (Rudiments of μ-calculus) を発見したのだけど、今更ながらじっくり読み進めている。電子版じゃ駄目で、やはり物理本だね…
今日はパリティオートマトンが何であるかが分かった。ωオートマトンの受理条件の表現方法の一つということだった。何でこんなん思いつくんだ。
で欲しかった情報 (μ計算とオートマトンの対応関係; 最近のセッション型でも通信オートマトンとμ型の両方がよく使われる) もしっかり説明されてる
今日はパリティオートマトンが何であるかが分かった。ωオートマトンの受理条件の表現方法の一つということだった。何でこんなん思いつくんだ。
で欲しかった情報 (μ計算とオートマトンの対応関係; 最近のセッション型でも通信オートマトンとμ型の両方がよく使われる) もしっかり説明されてる
Amazon.co.jp: Rudiments of Calculus (Volume 146) (Studies in Logic and the Foundations of Mathematic...
Amazon.co.jp: Rudiments of Calculus (Volume 146) (Studies in Logic and the Foundations of Mathematics, Volume 146) : Arnold, A., Niwinski, D.: Foreign Language Books
www.amazon.co.jp
September 8, 2023 at 9:19 PM
1,2章と残りの章の間で無限に反復横跳びしてる
トレースに関する等式 X = F(X) \/ X を不動点で解釈すると最小不動点は X = F(X) と一致する(ほしい性質)のだけど有限のトレースしか取れない。一方、最大不動点は無限のトレースも取れるけどこの等式ではXがトップに「つぶれて」しまう。
September 4, 2023 at 7:53 PM
トレースに関する等式 X = F(X) \/ X を不動点で解釈すると最小不動点は X = F(X) と一致する(ほしい性質)のだけど有限のトレースしか取れない。一方、最大不動点は無限のトレースも取れるけどこの等式ではXがトップに「つぶれて」しまう。