Keigo Imai

Signals and Threads Podcast Listen in on Jane Street’s Ron Minsky as he has conversations with engineers working on everything from clock synchronization to reliable multicast, build systems to reconfigurable hardware. Get a pee...

signalsandthreads.com/future-of-pr...

The Future of Programming with Richard Eisenberg ポッドキャストのエピソード · Signals and Threads · 2023/05/18 · 1時間

podcasts.apple.com/jp/podcast/s...

そうすると先の「aの無限列の途中でb」みたいなやつはµX.(aX + bµY.aY)のトレース集合として自然に計算できるようになる。最初µX.(aX + b)と思ったけどこれだとaの有限列もトレース集合に入ってくる（bのあとに暗黙の「正常終了」プロセスがあり、そっちが選ばれると終了する）(というかimage finitenessの問題がある?)

この追い越しを認める逐次合成はweak sequencingと呼ばれ、シーケンス図(Message Sequence Chart)の意味論のために今でも研究しているグループがある。一方、sequencingに追い越しの機能を持たせるのではなく、プロセス計算のprefixingの流儀でweak prefixingというやつを考えてみる。そしてMazurkiewiczトレースのような事後的な並べ変えでなく、演算子の意味(生成するトレース集合)そのものに「追い越し」をハードコードする。

Mazurkiewiczトレースにおいては無関係なアクションの並べ替えでトレースを増やすけれども、これは無限のトレースとは相性がわるい。たとえばaが無限に続くa^ωと、それと無関係なアクションbをsequential compositionでつなぐと無限のトレースは「終わらない」ので通常は(a^ω・b)=a^ωが成り立つけれど、もしaとbが無関係で追い越せる場合は有限回のaの後にbがはさまる(a^ω・b)=a*ba^ωみたいなことになる。後ろにあるプロセスがb単体ならまだわかるけどa^ω・b^ωとかもっと複雑なやつがどうなるのかは無限トレースのための意味論をよく調べないとわからない

プロセス計算のトレースで表示的意味論を作るやつ。ドメインとしてなんらかのposetを選び、演算子の意味はその上の単調関数にする。オートマトンだと受理する語の集合とその包含関係だけど、プロセス計算ではトレース*1のprefix closureとその包含関係を使う。ループX=F(X)の意味は最小不動点µX.F(X)とする。無限のトレースはprefix関係のlubを取れば得られるのでその情報自体は実質的にもとの集合に含まれている。
(*1オートマトンの文脈でいうMazurkiewiczトレースではなく単なるアルファベットの列。そもそもプロセス計算には陽な受理状態がないので語の概念もない)

👀 discuss.ocaml.org/t/best-appro...

金田家だ Holbornからテクテクあるいた記憶

British traditional TonkotsuX

欲しい機能はできたのでドキュメントとテストをだな

Deriving show for GADTs (wip) by keigoi · Pull Request #290 · ocaml-ppx/ppx_deriving (TBA)

OCaml: Deriving show for GADTs (wip) github.com/ocaml-ppx/pp...

でこれきさんのが十分うまくいっている

読むとうまくいってないね

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...

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...

カードゲームのプロトコルをセッションタイプで…

帰納法回し学をやっています

subset constructionの汎用性よ

TAPLの再帰型の章また読み返してる

未だに最小不動点定理の説明に迷いが生じる。周りの人に話そうと突き詰めていくと、やはり無限集合の直観的な把握とそれをどうやって論理で捉えるかといったところで少し修行が足りてない。ある集合が「任意の無限部分集合についてlubやglbをとる操作がある」という集合であれば、単調な関数を使ってさまざまな不動点を使った構成が可能になる

なんらかのmetricを決めたら不動点が決まると思っていたけれど、そういうmetricが存在するような空間では不動点はuniqueになるってことなのか(???

例えば、のところが間違えている気がしてきた

lptk.github.io/programming/... Demystifying MLsub — the Simple Essence of Algebraic Subtyping

p.50, subtyping lattice上の単調関数について不動点をとると最小不動点と最大不動点は一般に一致しないと思う (例えば x = a.x + b は最小不動点をとるとb, 最大不動点をとると所望の無限木が得られる) んだけど、なんかBanachの不動点をとることで両者が一致してると言っていて、まだよくわからない

選択演算子なんだからトレースの和集合でしょという漠然としたイメージが少し修正された。なんらかのシミュレーション関係っぽい。構成をやりなおしか？

これがためにループの意味をプロセス計算のトレース集合の不動点でとると実はうまくいかないのか

たぶんこの枠組みでよくある証明テクなんだけど選択演算子で片方が選択されたときに射影後のプロセスではまだそれが反映されてないことがあって、グローバルなビューとローカルな実態が厳密な一対一対応を維持せず進行している。サブタイプ関係がついたまま進行する。

証明フェーズに入ったので脳内で帰納法を回そうとしたところ回らない。ちょっとゆるめないといかん

オートマトンっぽい本(Rudiments of µ-Calculus)を読んでたからwordの集合で考えてしまっていたけどプログラミング言語のトレースはこのように扱うのだな。正直prefix-closedにする意義が全然わかってなかったよ…(センスがない。

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…

CSPの表示的意味論のほか、著者の先行研究 doi.org/10.3233/FI-1992-163-402 もそんな感じ。一方、CCSやπ計算を触っているとトレース何それおいしいのになりがち