0

我正在学习语言 K，所以我开始用 K 实现一点 Pi-Calculus。我不明白为什么我的替换Q[Z/Y]在下面的程序中不起作用。

我的程序是：（(m(z) . m ! z) | (m ! 4 . m(x))两个线程之间的 ping/pong），并且使用下面的 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>

这是我对 Pi 演算的 K 语义。请注意，我使用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

先感谢您。

4

0 回答 0