0

I have a macro called \logic which helps me write logical formulas faster by simplifying some common logical symbols. So when I write $\logic{p -> q}$ I obtain $p \to q$.

Here's the code:

\documentclass{article}

\makeatletter
%
% Command to format a formula with a succinct and natural syntax
%
\usepackage{xparse}
\usepackage{xstring}% for \StrSubstitute
\usepackage{pgffor}% for \foreach

% the strange `\iffalse{\fi` thing is a 'brace hack', to make this work inside
% `tabular`-like envs. See https://tex.stackexchange.com/questions/452442
\NewDocumentCommand\logic{+m}{\iffalse{\fi
  \def\gt@formula{#1}%
  \saveexpandmode
  \saveexploremode
  \expandarg
  \exploregroups
  \foreach \gt@keyword/\gt@operator in \gt@logic@operators {%
    \StrSubstitute{\gt@formula}{\gt@keyword}{\gt@operator}[\@temp]%
    \global\let\gt@formula\@temp
  }%
  \restoreexploremode
  \restoreexpandmode
  \ensuremath{\gt@formula}%
\iffalse}\fi}

\def\gt@logic@operators{}

\NewDocumentCommand\RegisterLogicOperators{m}{
  \def\gt@logic@operators{#1}
}

\makeatother

\RegisterLogicOperators{
  !/\neg,
  &&/\land,
  &/\land,
  \&/\land,
  ||/\lor,
  |/\lor,
  <->/\longleftrigtharrow,
  ->/\to,
  ~>/\leadsto,
  <-/\impliedby,
  <</\llangle,
  >>/\rrangle,
  <=/\le,
  >=/\ge,
  ==/\equiv,
  [[/\llbracket,
  ]]/\rrbracket,
}


\begin{document}

This is a logic formula: $\logic{((p -> q) & p) -> q}$.


\end{document}

However, the macro is very slow. You don't notice when you use it once, but in a paper with heavy usage the compilation time goes up very quickly. I suppose the bottleneck here is the \StrSubstitute macro from the xstring package, which seems a bit overkill for what I have to do, but I do not know how to obtain the same result faster. Also note that the real-world usage has a much longer list of replacements in the call to \RegisterLogicOperators.

Is there a way to improve the performance of this macro?

2

You can try this solution in LaTeX3, which converts the entire string in one go. I tried to convert 1000 expressions at once, and it takes less than 5 seconds.

\documentclass{article}
\usepackage[T1]{fontenc}
\usepackage{amsmath, amssymb}
\usepackage{expl3}

\ExplSyntaxOn
\prop_new:N \g_symbol_conv_prop
\prop_gset_from_keyval:Nn \g_symbol_conv_prop {
  !=\neg,
  &&=\land,
  &=\land,
  \&=\land,
  ||=\lor,
  |=\lor,
  <->=\longleftrightarrow,
  ->=\to,
  ~>=\leadsto,
  <-=\impliedby,
  <<=\llangle,
  >>=\rrangle,
  {<=}=\le,
  {>=}=\ge,
  {==}=\equiv,
  [[=\llbracket,
  ]]=\rrbracket
}

% convert keys to string
\prop_new:N \g_str_symbol_conv_prop
\prop_map_inline:Nn \g_symbol_conv_prop {
  \prop_put:Nxx \g_str_symbol_conv_prop {\tl_to_str:n {#1}} {\exp_not:n {#2}}
}

\cs_set:Npn \mult_level_lookup_name:n #1 {
  __g_symbol_lookup_\int_to_alph:n{#1}_seq
}

% find longest symbol
\int_new:N \g_longest_symbol_len_int
\int_set:Nn \g_longest_symbol_len_int {0}
\prop_map_inline:Nn \g_str_symbol_conv_prop {
  \int_set:Nn \l_tmpa_int {\str_count:n {#1}}
  \int_set:Nn \g_longest_symbol_len_int {
    \int_max:nn {\g_longest_symbol_len_int} {\l_tmpa_int}
  }
}

% create multi-level look up tables
\int_step_inline:nn {\g_longest_symbol_len_int} {
  \seq_new:c {\mult_level_lookup_name:n {#1}}
}

% fill multi-level lookup tables
\prop_map_inline:Nn \g_str_symbol_conv_prop {
  \str_set:Nn \l_tmpa_str {#1}
  \int_step_inline:nn {\str_count:N \l_tmpa_str} {
    \seq_push:cx {\mult_level_lookup_name:n {##1}} {
      \str_item:Nn \l_tmpa_str {##1}
    }
  }
}

\tl_new:N \l_logic_result_tl
\int_new:N \l_current_level_int
\str_new:N \l_current_logic_str
\str_new:N \l_current_symbol_str

\msg_new:nnn {logic} {invalidsymbol} {"#1" is not a valid symbol}
\cs_generate_variant:Nn \tl_rescan:nn {nV}


\cs_set:Npn \logic_conv:n #1 {
  \str_set:Nn \l_current_logic_str {#1}
  \int_set:Nn \l_current_level_int {1}
  \tl_clear:N \l_logic_result_tl
  \str_clear:N \l_current_symbol_str
  
  \bool_do_until:nn {\str_if_empty_p:N \l_current_logic_str} {
    % pop first item
    \str_set:Nx \l_tmpa_str {\str_head:N \l_current_logic_str}
    \str_set:Nx \l_current_logic_str {\str_tail:N \l_current_logic_str}
    
    % check if this item can be found in the look up table
    \seq_if_in:cVTF {\mult_level_lookup_name:n {\l_current_level_int}} \l_tmpa_str {
      % if it can be found, advance level and store it into \l_current_symbol_str
      \int_incr:N \l_current_level_int
      \str_put_right:NV \l_current_symbol_str \l_tmpa_str
    }
    {
      % if it cannot be found, it could be the end of a symbol
      % or just a normal string
      \str_if_empty:NF \l_current_symbol_str {
        % if \l_current_symbol_str is not empty, it is the end of a symbol
        % we need to insert the correct symbol and reset variables
        \prop_get:NVNTF \g_str_symbol_conv_prop \l_current_symbol_str \l_tmpa_tl {
          \int_set:Nn \l_current_level_int {1}
          \str_clear:N \l_current_symbol_str
          \tl_put_right:NV \l_logic_result_tl \l_tmpa_tl
        } {
          \tl_put_right:NV \l_logic_result_tl \l_current_symbol_str
          \int_set:Nn \l_current_level_int {1}
          \str_clear:N \l_current_symbol_str
        }
      }
      \tl_put_right:NV \l_logic_result_tl \l_tmpa_str
    }
  }
  % output last item
  \prop_get:NVNTF \g_str_symbol_conv_prop \l_current_symbol_str \l_tmpa_tl {
    \tl_put_right:NV \l_logic_result_tl \l_tmpa_tl
  } { \tl_put_right:NV \l_logic_result_tl \l_current_symbol_str }
  
  %\tl_show:N \l_logic_result_tl
  \tl_rescan:nV {} \l_logic_result_tl
}

\newcommand{\logic}[1]{
  \logic_conv:n {#1}
}


\ExplSyntaxOff

\begin{document}

$\logic{((p -> q) & p | !r) <= >= == -> <- c | d \phi || \sigma}$

\end{document}
  • Thanks! If I try to compile your code I get some undefined control sequence errors, such as: ! Undefined control sequence. \__prop_pair:wn #1\s__prop #2->\prop_put:Nxx \g_str_symbol_conv_prop {\tl_to... l.32 } – gigabytes Oct 13 '20 at 18:46
  • @gigabytes Probably the Nxx variant is only added in latest expl3. I have modified the code. – Alan Xiang Oct 13 '20 at 19:04
  • Thanks, now TeX stops on this: \l_logic_result_tl=((p \to q) \land p \lor \neg r) \le \ge \equiv \to \impliedby c \lor d. <recently read> } l.125 ...((p -> q) & p | !r) <= >= == -> <- c | d} ` $` – gigabytes Oct 13 '20 at 19:23
  • This is just showing what the content of \l_logic_result_tl is for debug purposes. You can simply skip it or comment out \tl_show:N \l_logic_result_tl . – Alan Xiang Oct 13 '20 at 19:49
  • Ok, now it compiles fine! However, it does something different. If I say for example \logic{\phi -> \psi} I get the -> translated correctly, but \phi and \psi appear as "\phi" and "\psi" on the typeset output! In my version, everything that is not in the list of translated tokens is left as is. Here it seems as if it was passed to \string. Can it be fixed somehow? Unfortunately, expl3 is completely opaque to me – gigabytes Oct 13 '20 at 20:23

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.