kframework - K で [バインダー] を使用するには?

Question

私は構文を持っています：

syntax Process ::= KVar "(" KVar ")" "." Process  [binder]
                 | "new" KVar "." Process         [binder]
syntax Program ::= KVar "(" KVarVec ")" "=" Process [binder]
syntax KVarVec ::= KVar | KVar "," KVarVec

2 つの構文には、異なるバインドを行う 3 つのプロダクションがあります。

1. a(x).P、ここでxは に拘束されてPいaますが、その用語に拘束されていない名前です。

2. new a.Pラムダのようにバインドaします。P

3. f(a,b,c) = Pinのベクトルa,b,cをバインドします。ベクトル内のそれぞれは にバインドされているはずです。KVarPKVarP

binderプロダクションで特定の変数をバインドするように指示するにはどうすればよいですか? 2番目がバインドされているはずだbinder(2)と伝えるようなものはありますか? KVarいくつかKVarの が別の構文で定義されている場合はどうなりますか?