kframework - 円周率計算における変数置換エラー

Question

私は言語 K を学んでいるので、K を使って円周率計算を少し実装し始めましたQ[Z/Y]。以下のプログラムで置換が機能しない理由がわかりません。

私のプログラムは次のとおりです: (m(z) . m ! z) | (m ! 4 . m(x))(2 つのスレッド間のピンポン)、以下の K セマンティックを使用すると、次の出力が得られます。

</thread> <thread>
    <k>
      m ! z ~> .
    </k>
  </thread> <thread>
    <k>
      m ( x ) ~> .
    </k>

でもz代用されない。私はこの出力を期待します：

</thread> <thread>
    <k>
      m ! 4 ~> .      <---The 2nd z take the value of 4
    </k>
  </thread> <thread>
    <k>
      m ( x ) ~> .
    </k>

これが、円周率計算の K セマンティックです。send 構造のx!y代わりに使用していることに注意してください。x<y>

require "substitution.md"

module PI-SYNTAX 
    imports DOMAINS-SYNTAX
    imports KVAR-SYNTAX

    syntax Val ::= KVar  [binder]
                | Int

    syntax Proc ::= "(" Proc ")"        [bracket]
                | Send
                | Receive
                | None
                | Replication
                > Proc "." Proc         [left]
                > Par

    syntax None ::= "None"

    syntax Par ::= Proc "|" Proc        [left]

    syntax Receive ::= Id "(" Val ")"   

    syntax Send ::= Id "!" Val

    syntax Replication ::= "!" Proc

endmodule

module PI
    imports PI-SYNTAX
    imports DOMAINS
    imports SUBSTITUTION

    syntax KResult ::= Int | Bool

      configuration <T color="yellow">
                        <thread multiplicity="*" type="Set" color="blue">
                            <k color="green"> $PGM:Proc </k>
                        </thread>
                    </T>

    // Parallel composition:
    rule <thread> <k> P1:Proc | P2:Proc => . ... </k> </thread>
        (.Bag => <thread> <k> P1 </k> </thread>)
        (.Bag => <thread> <k> P2 </k> </thread>)

    // Communicate reduction: x ! y . P | x(y) . Q => P | Q[z/y]
    rule
        <thread> ... <k> X:Id ! Y:Val . P:Proc => P </k> ... </thread>
        <thread> ... <k> X:Id ( Z:Val ) . Q:Proc => Q[Z/Y] </k> ... </thread>
endmodule

前もって感謝します。