Mobility Workbench の Sigma, Bsigma, Pi

またも id:syd_syd さんに教えていただく。
しばらく遊んでいたところ Sigma, Bsigma, Pi の使い方は理解できたが、その意味はわかっていない。やっぱり本を読んで勉強しないといけない。
直感的には、 Sigma は送信データにマッチし、 Bsigma はプロセス内でνされて外側からは見えない値を送信する時のデータにマッチし、 Pi は受信データにマッチする、と考えればいいと思われる。 'a< b > を 'a と < b > に分けて考えるのがポイント。 'a のとこが < 'x > にマッチし、 < b > のとこが Sigma あるいは Bsigma にマッチする。

例として a(b).b.0 というプロセスを考えてみると、 a から受信したデータに b という名前をつけてその後の動作(b.0)を行う、と読める。つまりこのプロセスは、 a で受信を行ったあと b という名前のところに引数をもらって動作する関数みたいな動きをする。*1

ちなみにこれを abstraction という(lambda abstraction みたいな)。その反対の動作で、関数に引数を与える動作を concretion というっぽい(abstraction <-> concretion)。このへんは非常に怪しいので信用しないでくださいな。

適当な例。

agent P(a,b) = 'a<b>.b.0
check P(a,b) <'x>(x=a & Sigma x.(<y>(y=x)))
check P(a,b) <'x>(x=a & Bsigma x.(<y>(y=x)))

agent Q(a) = (^b)'a<b>.b.0
check Q(a) <'x>(x=a & Bsigma x.(<y>(y=x)))

agent R(a) = a(b).b.0
check R(a) <x>(x=a & Pi x.(x=b))
check R(a) <x>(x=a & Pi x.<y>(y=x))

Mobility Workbench さんの答え。

MWB>input "sigma.mwb"
input "sigma.mwb"
Yes! (6 inferences)
No. (4 inferences)
Yes! (6 inferences)
No. (5 inferences)
Yes! (6 inferences)
MWB>

予想通りの動作だけど、よくわからない。

• -

適当にググってたら

P is a process if its standard form has arity 0,
a concretion if it has arity <0,
and an abstraction if it arity >0.

とあった。アリティが 0 より小さくなることもあるのか。

*1:引数を受ける (b) のとこに Pi x の x がマッチする。