profiled substitutions の圏
ウーン、ちゃんと書かないとやばいよなー、と思いつつ、極めてラフなメモ。近日中になんとかして、より詳しい記述をしたい。
変数と項のペアを束縛と呼ぶことにする。x = t のようにイコールで書く。束縛の集合、ただし変数はすべて違うものを束縛セットと呼ぶ。束縛と束縛セットはその使用目的により色々な名で呼ばれる。
- assign, assignment
- 付置（valuation）
- 環境
- コンテキスト
- 置換、代入、展開
- モジュール
ここでは、置換（substitution）としての束縛セットを扱う。
変数セットVを固定すると、V上で定義された置換の全体は合成に対してモノイドとなる。このモノイドは「モノイドに出来る」ってだけであまり自然なモノとは思えない。
変数セットVを固定せずに、任意の有限集合を変数セットだとみなして置換を考えて、置換＝束縛セットXの左辺変数の全体をLVar(X)、右辺に出現する変数の全体を RVar(X) として、RVar(X)⊆ A、B⊆LVar(X) である集合 A, Bを組み合わせて (A→B)X または (B←A)X と書く。これがプロファイル付き置換。
プロファイル付き置換の全体は自明な方法で圏になる。有限集合の直和をモノイド積としてモノイド圏ともなる。
問題は、このモノイド圏にトレース構造を入れること。構文構造だけを使ってトレースを組み立てるのが面白い問題だが、意味論を持ち込んで、意味論を使いながらトレースを入れてもいい。これら二つの手法を比較するのが最も興味深いトピックだ。
