Natural language annotations in general

[Jazzpirate]

Example sentence

"A natural number $N$ is even, if its square is even."

• Let \operator a semantic macro that takes n arguments.
  e.g.: \implication, n=2.
• In mathmode, \operator behaves as usual (e.g. $\implication{A}{B}$ expands to (ignoring semantics) $A \Rightarrow B$ - see Symbolic notations #3)
• Let p=(p_1,...,p_m) a phrase that represents an application of \operator to arguments arg_1,...,arg_n
  e.g. p = "A natural number $N$ is even, if its square is even."
  arg_1="its square is even",
  arg_2="A natural number $N$ is even"

Requirements

• \operator in text mode needs n arguments. The n arguments are subsequences of p in arbitrary order, interleaved with subsequences that do not represent an argument.
  e.g. first argument of \implication is "its square is even",
  second argument is "A natural number $N$ is even", and
  ", if" does not represent an argument - these are considered verbalization components of \operator.
• arguments can be invisible.
  e.g. the second argument of \natpow in "its square" is 2, which is not explicitly represented in the text.
• each argument has to contain a uniquely identifiable subsequence that represents the actual term
  e.g. in "A natural number $N$", the argument to \even is "$N$", not "natural number"!
• variables: If declared, not compositional. If not declared, the scope needs determining ("is this still the same $N$ as this one?"),
  its quantification (universally/existentially) and "type" (optionally) provided, and all of these ideally at most once, even if the variable
  occurs multiple times.

Ideas

• Macro \operator takes n {} arguments, representing the operator arguments, interleaved with optional [] arguments in between (including leading and trailing) representing verbalization components.
  e.g. \even{its square}[is even] => "its square" is the argument, "is even" is just a verbalization component.
• An argument prefixed by *[k] indicates that what follows is the k-th argument rather than the next one.
  e.g. \implication*[2]{A natural number $N$ is even}[, if]{its square is even} indicates that the second argument comes first.
• An argument prefixed by * is invisible
  e.g. \natpow{its}[ square]*{2} == \natpow{its}*{2}[ square] == \natpow*[2]*{2}{its}[ square]

=> \implication*[2]{\even{A \NaturalNumbers[natural number] $N$}[ is even]}[, if]{\even{\natpow{its}*{2}[ square]}[ is even]}.

Remaining questions

1. Both "A natural number $N$" and "its" represent OMV(N), where N has type \NaturalNumbers and is universally quantified.
   How to represent this? (see Variables (scopes, quantification,...) #5 )
2. Binding applications (see Variable bindings in binding operators #8 )
3. Sequences (see Sequences and sequence arguments for flexary (associative) operators #7 )

[Jazzpirate]

Update: Things get tricky with associative arguments.

Possible solution 1: \operator just takes arbitrarily many arguments in general (via \ifnextchar[ and \ifnextchar{ - need to check whether the latter works even). Inelegant, but would probably work.

Possible solution 2: an associative argument takes arbitrarily many comma-separated arguments, every other of which is considered a verbalization component. E.g. for flexary \plus, an application could look something like
\plus[the sum of ]{a,{,},b, and ,c}