[NTG-context] Re: Luametatex: nesting alignments in display math formulas

[Mikael Sundqvist <mickep@gmail.com>]

Hi,

On Sun, Nov 10, 2024 at 2:45 AM ntg-contextmailingli.expedited080---
via ntg-context <ntg-context@ntg.nl> wrote:
>
> I'm test driving luametatex. My needs usually extend to expressing formulas in TLA+ using nested display math formulas. Although I have suitable templates for doing this in Mark IV, I can't reproduce these satisfactorily in luametatex. For example, here's a formula from Leslie Lamport's 2006 "Lower Bounds for Asynchronous Consensus":
>
> ~~~~~~~~~~~ transitive_reduction.tex ~~~~~~~~~~~~~
>
> \define\lbr {\lbrace \mkern 0.9mu}
> \define\rbr {{}\mkern 0.9mu \rbrace}
> \define\∀ {∀\mkern1mu}
> \define\∃ {∃\mkern2mu}
>
> \startdocument
>
> \startplaceformula
> \startformula [split=yes, align=flushleft, margin=standard, interlinespace=1ex]
> \bgroup \setupinterlinespace [line=1ex]
> \startalign [n=1, align={left,left}]
>
>     \NC \text{\it TransitiveClosure}(R) ≜
>     \NR
>
>     \NC \quad
>     \bgroup \setupinterlinespace [line=1ex]
>     \startalign [n=2, align={left,left,left}, location=top]
>
>         \NC \text{\sc let} \quad
>         \NC \bgroup \setupinterlinespace [line=1ex]
>         \startalign [n=1, align={left,left}, location=top]
>
>             \NC \text{\it Dom} ≜ \lbr r[1]: r ∈ R \rbr
>             \NR
>
>             \NC \text{\it Rng} ≜ \lbr r[2]: r ∈ R \rbr
>             \NR
>
>             \NC \text{\it TC}[i ∈ ℕ] ≜
>             \NR
>
>             \NC \quad
>             \bgroup \setupinterlinespace [line=1ex]
>             \startalign [n=1, align={left,left}, location=top]
>
>                 \NC \text{\sc if}\ i = 0\
>                 \bgroup \setupinterlinespace [line=1ex]
>                 \startalign [n=2, align={left,left,left}, location=top]
>
>                     \NC \text{\sc then}\
>                     \NC R
>                     \NR
>
>                     \NC \text{\sc else}\
>                     \NC
>                     \bgroup \setupinterlinespace [line=1ex]
>                     \startalign [n=1, align={left,left}, location=top]
>
>                         \NC \lbr
>                             〈d, e 〉∈ \text{\it Dom} × \text{\it Rng}:
>                         \NR
>
>                         \NC \quad \∃ c ∈ \text{\it Dom} ∩ \text{\it Rng}:
>                         \bgroup \setupinterlinespace [line=1ex]
>                         \startalign [n=1, align={left,left}, location=top]
>
>                             \NC ∧ 〈d, c〉∈ \text{\it TC}[i-1]
>                             \NR
>
>                             \NC ∧ 〈c, e〉∈ R \,\rbr
>                             \NR
>                         \stopalign \egroup
>                         \NR
>                     \stopalign \egroup
>                     \NR
>                 \stopalign \egroup
>                 \NR
>             \stopalign \egroup
>             \NR
>         \stopalign \egroup
>         \NR
>
>         \NC \text{\sc in}\
>         \NC \text{\sc union}\ \lbr \text{\it TC}[i] : i ∈ ℕ \rbr
>         \NR
>     \stopalign \egroup
>     \NR
> \stopalign \egroup \stopformula \stopplaceformula
>
> \stopdocument
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
> The command
>
>     $ context --luatex transitive_reduction.tex
>
> produces the desired result, but
>
>     $ context transitive_reduction.tex
>
> rejects the alignments and centers the lines instead. Can anyone suggest how I might adapt such nesting of alignments to luametatex?
>

I must admit that I don't know what is the expected output and if I
did break any of the rules or missed what you want, but the following
could hopefully work as a start for you:

\define\lbr {\lbrace \mkern 0.9mu}
\define\rbr {{}\mkern 0.9mu \rbrace}
\define\∀ {∀\mkern1mu}
\define\∃ {∃\mkern2mu}

\definemathsimplealign
  [myalign]
  [align=left,
   location=top]

\definemathsimplealign
  [myouteralign]
  [align=left,
   location=center]

\definemathsimplealign
  [mydistancedalign]
  [align=left,
   distance=1em,
   leftmargin=1em]

\definemathsimplealign
  [mymarginedalign]
  [align=left,
   leftmargin=1em]

\startdocument

\startplaceformula
\startformula [align=flushleft]
\startmyouteralign
    \NC \mathtextit{TransitiveClosure}(R) ≜
    \NR

    \NC
    \startmydistancedalign
        \NC \mtext{\sc let}
        \NC
        \startmyalign
            \NC \mathtextit {Dom} ≜ \lbr r[1]: r ∈ R \rbr
            \NR
            \NC \mathtextit {Rng} ≜ \lbr r[2]: r ∈ R \rbr
            \NR
            \NC \mathtextit {TC\/}[i ∈ ℕ] ≜
            \NR
            \NC
            \startmymarginedalign
                \NC \text{\sc if } i = 0\
                \startmyalign
                    \NC \text{\sc then}\
                    \NC R
                    \NR

                    \NC \text{\sc else}\
                    \NC
                    \startmyalign
                        \NC \lbr
                            〈d, e 〉 ∈ \text{\it Dom} × \text{\it Rng}:
                        \NR

                        \NC \quad \∃ c ∈ \text{\it Dom} ∩ \text{\it Rng}:
                        \startmyalign

                            \NC ∧ 〈d, c〉 ∈ \mathtextit {TC\/}[i-1]
                            \NR

                            \NC ∧ 〈c, e〉 ∈ R \rbr
                            \NR
                        \stopmyalign
                        \NR
                    \stopmyalign
                    \NR
                \stopmyalign
                \NR
            \stopmymarginedalign
            \NR
        \stopmyalign
        \NR
        \NC \mtext{\sc in}
        \NC \mtext{\sc union } \lbr \mathtextit {TC\/}[i] : i ∈ ℕ \rbr
        \NR
    \stopmydistancedalign
    \NR
\stopmyouteralign
\stopformula \stopplaceformula

\stopdocument

/Mikael
___________________________________________________________________________________
If your question is of interest to others as well, please add an entry to the Wiki!

maillist : ntg-context@ntg.nl / https://mailman.ntg.nl/mailman3/lists/ntg-context.ntg.nl
webpage  : https://www.pragma-ade.nl / https://context.aanhet.net (mirror)
archive  : https://github.com/contextgarden/context
wiki     : https://wiki.contextgarden.net
___________________________________________________________________________________