Ich arbeite derzeit daran, Beweisbäume für reguläre Ausdrücke in Scheme zu erstellen. Die in meinem Kurs vorgeschlagene Schreibweise ist die folgende, die ich manuell in TeX eingegeben habe.
Dies ist jedoch ein langwieriger Prozess, insbesondere bei langen Ausdrücken. Ich suche also nach einer raffinierten Möglichkeit, den oben gezeigten Beweisbaumtyp zu erstellen, oder vielleicht nach einer Alternative, die dasselbe erreichen kann.
Bearbeiten:
Hier ist mein Code. Ich habe nichts dagegen, ihn in den Baum einzutippen, aber dieser Weg ist wirklich sehr, sehr langsam. Wenn es also ein Paket gibt, das einen Teil der Positionierungsarbeit für mich übernehmen kann, wäre ich ein glücklicher Mensch.
\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))))))
Bearbeitung 2:
Ich habe mit dem Paket keine Lösung gefunden bussproofs, aber es ist immer noch nicht optimal. Es sieht etwas seltsam aus, wenn die Prooftrees groß werden.
Mein Code zum Erstellen lautet:
\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}