読み取り専用の呼び出し

ツール呼び出し $(n, x)$ が読み取り専用であるとは、すべての $e \in E$ について $\mathrm{exec}_n(x, e)$ の第 2 成分が $e$ であることをいう。このとき $\mathrm{exec}_n(x, e) = (\rho_{n,x}(e), e)$ と書ける。