2

I am typing setting some big step semantics using the package semantic and its command \inference.

I use the LuaLaTeX compiler.

However, when I compose more inference commands, and one of them represents an axiom, i.e. a rule without any premises, the other premise starts floating. It looks like it is trying to do some vertical alignment.

Here is an example:

\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}

screenshot

2

In the OP's example, the baseline is being preserved across the large "numerator". While one may argue that is the proper way to do it, one can override that default with \abovebaseline[-\dp\strutbox]{...} applied to the ED-Skip inference.

\documentclass{article}
\usepackage{semantic,amsmath,stackengine}
\begin{document}
\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \abovebaseline[-\dp\strutbox]{\inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }}
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}
\end{document}

enter image description here

  • Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you. – Einar Mar 15 at 10:53
  • @Einar Consider the numerator. With the \overset{<over>}{<baseline>} macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, the EC-Skip also sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the <skip,>\downarrow text being set below this axis line. – Steven B. Segletes Mar 15 at 11:11
  • @Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the <b,>\downarrow false wants to sit at the same vertical height as EC-Skip. – Steven B. Segletes Mar 15 at 11:12
  • @Einar The macro \abovebaseline says to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of -\dp\strutbox is the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text. – Steven B. Segletes Mar 15 at 11:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.