From: Julian Bradfield <jcb+unicode_at_inf.ed.ac.uk>

Date: Thu, 12 Jul 2012 23:10:51 +0100

Date: Thu, 12 Jul 2012 23:10:51 +0100

On 2012-07-12, Hans Aberg <haberg-1_at_telia.com> wrote:

*>On 12 Jul 2012, at 16:06, Julian Bradfield wrote:
*

*>> On 2012-07-12, Hans Aberg <haberg-1_at_telia.com> 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.
*

*>>> https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
*

*>>
*

*>> 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

\def\tetration#1#2{{}^{#2}{#1}}

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
*