LaTeX 上进程代数的过渡语义

LaTeX 上进程代数的过渡语义

正如标题所述,我正在努力寻找一种方法来在 LaTeX 上为硕士论文编写以下过渡语义。

在此处输入图片描述

有人能帮助我吗?

编辑1:正如评论中所建议的,我尝试逐一编写过渡规则,但结果不佳:

Tau $\overline{\langle\tau . P, \rho\rangle \stackrel{\tau}{\longrightarrow}\langle P, \rho\rangle}$
$O u t_{C} \frac{v=\llbracket e \rrbracket}{\langle c ! e . P, \rho\rangle \stackrel{c ! v}{\longrightarrow}\langle P, \rho\rangle}$
Out $_{Q} \overline{\langle c ! q . P, \rho\rangle \stackrel{\mathrm{c!} q}{\longrightarrow}\langle P, \rho\rangle}$
Meas $\frac{M=\sum_{i \in I} \lambda_{i} E^{i}, p_{i}=\operatorname{tr}\left(E_{\tilde{r}}^{i} \rho\right)>0}{\langle M[\tilde{r} ; x] . P, \rho\rangle \stackrel{\tau}{\longrightarrow} \sum_{i \in I} p_{i}\left\langle P\left\{\lambda_{i} / x\right\}, E_{\tilde{r}}^{i} \rho E_{\tilde{r}}^{i} / p_{i}\right\rangle}$
$\operatorname{Com}_{C} \frac{\left\langle P_{1}, \rho\right\rangle \stackrel{c ? v}{\longrightarrow}\left\langle P_{1}^{\prime}, \rho\right\rangle,\left\langle P_{2}, \rho\right\rangle \stackrel{c ! v}{\longrightarrow}\left\langle P_{2}^{\prime}, \rho\right\rangle}{\left\langle P_{1} \| P_{2}, \rho\right\rangle \stackrel{\tau}{\longrightarrow}\left\langle P_{1}^{\prime} \| P_{2}^{\prime}, \rho\right\rangle}$

ETC...

问题主要有两个:我无法将转换的名称和“分形”对齐,并且我不知道如何“插入”第二列转换。

编辑2:

正如 KersouMan 的出色建议(向您致敬),他的方法有效,以下是完整的代码:

\begin{align*}
    Tau & \quad\frac{}{\langle\tau.P,\rho\rangle\xrightarrow{\tau}\langle P,\rho\rangle} 
        & Op & \quad \frac {}{\langle\mathcal{E}[\tilde{r}] . P, \rho\rangle \stackrel{\tau}{\longrightarrow}\left\langle P, \mathcal{E}_{\tilde{r}}(\rho)\right\rangle}\\ 
    Inp_C & \quad\frac{v\in\mathsf{Real}}{\langle c?x.t,\rho\rangle\xrightarrow{c?v}\langle t\{v/x\},\rho\rangle} 
        & Out_{C} & \quad\frac{v = \llbracket e\rrbracket}{\langle c!e.P,\rho\rangle\xrightarrow{e!v}\langle P,\rho\rangle} \\
    Inp_{Q} & \quad\frac{r\not\in qv(x?q.P)}{\langle c?q.P,\rho\rangle\xrightarrow{c?r}\langle P\{r/q\},\rho\rangle} 
        & Out_{Q} & \quad \frac{}{\langle c ! q . P, \rho\rangle \stackrel{\mathrm{c!} q}{\longrightarrow}\langle P, \rho\rangle}\\
     Meas & \quad \frac{M=\sum_{i \in I} \lambda_{i} E^{i}, p_{i}=\operatorname{tr}\left(E_{\tilde{r}}^{i} \rho\right)>0}{\langle M[\tilde{r} ; x] . P, \rho\rangle \stackrel{\tau}{\longrightarrow} \sum_{i \in I} p_{i}\left\langle P\left\{\lambda_{i} / x\right\}, E_{\tilde{r}}^{i} \rho E_{\tilde{r}}^{i} / p_{i}\right\rangle}
        & Par & \quad  \frac{\left\langle P_{1}, \rho\right\rangle \stackrel{\alpha}{\longrightarrow} \mu, q b v(\alpha) \cap q v\left(P_{2}\right)=\emptyset}{\left\langle P_{1} \| P_{2}, \rho\right\rangle \stackrel{\alpha}{\longrightarrow} \mu \| P_{2}}\\
    Com_{C} & \quad \frac{\left\langle P_{1}, \rho\right\rangle \stackrel{c ? v}{\longrightarrow}\left\langle P_{1}^{\prime}, \rho\right\rangle,\left\langle P_{2}, \rho\right\rangle \stackrel{c ! v}{\longrightarrow}\left\langle P_{2}^{\prime}, \rho\right\rangle}{\left\langle P_{1} \| P_{2}, \rho\right\rangle \stackrel{\tau}{\longrightarrow}\left\langle P_{1}^{\prime} \| P_{2}^{\prime}, \rho\right\rangle}
        & Com_{Q} & \quad \frac{\left\langle P_{1}, \rho\right\rangle \stackrel{\mathrm{c} ? r}{\longrightarrow}\left\langle P_{1}^{\prime}, \rho\right\rangle, \quad\left\langle P_{2}, \rho\right\rangle \stackrel{\mathrm{c} ! r}{\longrightarrow}\left\langle P_{2}^{\prime}, \rho\right\rangle}{\left\langle P_{1} \| P_{2}, \rho\right\rangle \stackrel{\tau}{\longrightarrow}\left\langle P_{1}^{\prime} \| P_{2}^{\prime}, \rho\right\rangle}\\
    Rel & \quad \frac{\langle P, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu}{\langle P[f], \rho\rangle \stackrel{f(\alpha)}{\longrightarrow} \mu[f]} 
        & Sum & \quad \frac{\langle P, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu}{\langle P+Q, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu}\\
    Res & \quad \frac{\langle P, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu, c n(\alpha) \cap L=\emptyset}{\langle P \backslash L, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu \backslash L} 
        & Cho & \quad \frac{\langle P, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu, \llbracket b \rrbracket=\mathrm{tt}}{\langle\text { if } b \text { then } P, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu}\\
    Def & \quad \frac{\langle t\{\tilde{v} / \tilde{x}, \tilde{r} / \tilde{q}\}, \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu, A(\tilde{x}, \tilde{q}):=t, \tilde{v}=\llbracket \tilde{e}]]}{\langle A(\tilde{e}, \tilde{r}), \rho\rangle \stackrel{\alpha}{\longrightarrow} \mu}
\end{align*}

最后一个问题是,现在我无法将整个块与中心对齐,并且它不适合页面:

在此处输入图片描述

我显然尝试使用经典命令:\begin{align}...\end{align但它不起作用,有什么建议吗?

答案1

根据编辑后提出的问题,我建议使用环境align来获取两列。\quad这里的命令只是为了在转换名称和“分数”之间添加间距。stmaryrd这里的包用于\llbracket\rrbracket命令(使用双方括号)。

此外,原作者遇到的一个问题是,对于某些转换,分数线无法与转换名称对齐。这是由于在\overline第一个转换中使用了 (例如)造成的,但使用\frac空分子是完全可以的。这样,上部为空的转换将与同时具有上部和下部的转换完全对齐。

\documentclass{article}

\usepackage{amsmath}
\usepackage{stmaryrd}

\begin{document}

\begin{align*}
    Tau & \quad\frac{}{\langle\tau.P,\rho\rangle\xrightarrow{\tau}\langle P,\rho\rangle} & Inp_C & \quad\frac{v\in\mathsf{Real}}{\langle c?x.t,\rho\rangle\xrightarrow{c?v}\langle t\{v/x\},\rho\rangle}\\
    Out_{C} & \quad\frac{v = \llbracket e\rrbracket}{\langle c!e.P,\rho\rangle\xrightarrow{e!v}\langle P,\rho\rangle} & Inp_{Q} & \quad\frac{r\not\in qv(x?q.P)}{\langle c?q.P,\rho\rangle\xrightarrow{c?r}\langle P\{r/q\},\rho\rangle}
\end{align*}

\end{document}

建议的代码产生以下结果:

在此处输入图片描述

编辑

为了在转换(Tau、Inp、...)的名称中获得更好的字母间距,这些名称可以封装在\textit\mathit命令中,如\textit{Inp}_{C}\mathit{Inp}_{C}

答案2

要调整方程的大小,您可以尝试以下示例:

\documentclass[a4paper,14pt]{extreport}
\usepackage{amsmath}
\usepackage{graphicx}

\begin{document}
\resizebox{.4\textwidth}{!}{$\dot{\rho}= \dfrac{x^3}{45a^9-23b}$}
\resizebox{.2\textwidth}{!}{$\dot{\rho}= \dfrac{x^3}{45a^9-23b}$}
\resizebox{.1\textwidth}{!}{$\dot{\rho}= \dfrac{x^3}{45a^9-23b}$}
\resizebox{.05\textwidth}{!}{$\dot{\rho}= \dfrac{x^3}{45a^9-23b}$}
\end{document}

在此处输入图片描述

相关内容