Re: Too narrowly defined: DIVISION SIGN & COLON

From: Julian Bradfield <>
Date: Thu, 12 Jul 2012 23:10:51 +0100

On 2012-07-12, Hans Aberg <> wrote:
>On 12 Jul 2012, at 16:06, Julian Bradfield wrote:
>> On 2012-07-12, Hans Aberg <> wrote:
>>> On 12 Jul 2012, at 12:33, Julian Bradfield wrote:
>>>> In practice, no working mathematician is going to use the mathematical
>>>> alphanumerical symbols to write maths in (La)TeX, because it's
>> ..
>>>> the Unicode mathematical symbol model does not match how one uses
>>>> mathematical symbols.
>>> It is used by proof assistants such as Isabelle, and also in logic.
>> No it isn't.
>Yes, I posted before here some example of people using it.

I beg your pardon, you're right. I didn't read it closely enough.

>> Isabelle uses (essentially) TeX control sequences
>> internally, though it writes them as \<oplus> rather than \oplus .
>> A small number of these are mapped to Unicode code points for display
>> and input purposes, and that small number does not include any of the
>> mathematical alphanumerical symbols block.

You're right, it does default to using that block in Unicode mode.

>Latest version requires STIXFonts to be installed. Some other proof assistants use it.

However, that's not true. Isabelle does not need to use Unicode; it
runs happily in an ASCII terminal, because its internal representation
is tokens, not Unicode characters. The Unicode is syntactic sugar
that's part of the Emacs interface and the Scala interface.

>>> If your only objective is to achieve a rendering for humans to read, TeX is fine, but not if one wants to communicate semantic information on the computer level.
>> On the contrary, computers are very happy with TeX notation. There are
>> several useful mathematical online learning sites (such as, for
>> example, Alcumus) which use TeX syntax to interact with the students.
>TeX formulas are just for rendering. For example, if you want to have superscript to the left, you have to write ${}^x y$.

If you read any introduction to TeX, it will explain how you use
macros to provide a structured markup. If you were using that
notation, then you would define a suitable macro, say
and write $\tetration{y}{x}$.
This does not depend on any fancy Unicodery for its interpretation,
and also allows you to define semantic content for the computer.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Received on Thu Jul 12 2012 - 17:13:49 CDT

This archive was generated by hypermail 2.2.0 : Thu Jul 12 2012 - 17:13:55 CDT