☰

Scheme 証明ツリー

tag-icon • tag-icon trees
Scheme 証明ツリー

現在、Scheme で正規表現の証明木を作成中です。私が受講しているコースで推奨されている記述方法は次の通りで、これを TeX に手動で入力しました。

証明ツリー

しかし、これは面倒なプロセスであり、特に長い式の場合は面倒です。そこで私が探しているのは、上記のような証明ツリーを作成する巧妙な方法、または同じことを達成できる代替手段です。

編集:

これが私のコードです。ツリーに入力するのは構いませんが、この方法は非常に時間がかかります。そのため、位置合わせ作業の一部を実行できるパッケージがあれば、とても助かります。

\phantom{ATOM}\ \ \ \ \ 1 is a Scheme integer\qquad\qquad\qquad (\%regexp (atom 2))\\
ATOM ---------------------\qquad\qquad SEQ ------------------------------------------------------------\\
\phantom{ATOM} (\%regexp (atom 1)) \qquad\qquad\qquad\ \ (\%regexp (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty)))\\
\phantom{A}SEQ ---------------------------------------------------------------------------------------------\\
\phantom{ATOM} (\%regexp (seq (atom 1) (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty))))))

編集2: パッケージで解決策が見つからなかったのですbussproofsが、それでも最適ではなく、証明木が大きくなると見た目が少しおかしくなります。

プルーフツリー

これを作成するためのコードは次のとおりです。

\begin{prooftree}
\def\ScoreOverhang{1pt} 
\def\extraVskip{6pt}
\def\defaultHypSeparation{\hskip .2in}
\def\ruleScoreFiller{\hbox to1.1mm{\hss\vrule width0.9mm height0.4pt depth0.0pt\hss}}
\AxiomC{1 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 1))}
\AxiomC{2 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 2))}
\AxiomC{3 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 3))}
\AxiomC{4 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 4))}
\AxiomC{}
\LeftLabel{EMPTY}
\UnaryInfC{(\%regexp (empty))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 4) (empty)))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 3) (seq (atom 4) (empty))))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty)))))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 1) (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty))))))}
\end{prooftree}

関連情報