[Om3] Being pragmatic about the semantics of, eg, variables and functions

[Professor James Davenport]

On Sun, March 22, 2009 8:19 pm, c.a.rowley at open.ac.uk wrote:
> I also have far too much to say about functions and integration, with
examples (only 1-dimensional) such as:
>
> \int _{ |\cos(z)| < 1  and z < 0 } ( sin \invisibletimes exp )
I'm not sure what this is intended to convey. Since $|\cos z|\le1$, we are
only excluding a set (admittedly infinite, but only finite over a finite
range) of isolated points.
>
> chris
>
> =================================================================== What
is (and will be) good semantic mark-up of real-world, ordinary
day-to-day mathematical exposition?
> -----------------------------------
>
> One thing to get clear (or at least admit to fudging it) is how close
such good semantic mark-up of mathematics 'should be' to the particular
'mathematical phraseology' in use at a particular time and place of
exposition.
>
> Here I say 'phraseology' rather than 'notation' for two reasons:
>
>   one needs to think about the phrase that one would use to give (in
speech or written text) the mathematical meaning of the notation;
>
>   often the 'complete formula' (the smallest unit which has useful
mathematical semantics) is not just the part using pure notation but
also contains such text as 'Let X be a wobbly foo with ... ' or '...
where X is the wobbly foo in Equation A (and hence has ...)'.
A very good point. MK and I admit this to some extent in (4) of our MKM
paper, which is restructed from a 'complete formula' in your sense, but,
of course, that's a real rationale for OMDoc.
> As we always knew, and are now painfully aware, things like
> 'multi-dimensional definite integration' have a long and continuing
history of ad hoc phraseologies (note the plural, although many are
closely related) that do an excellent job of describing
> its three essential constituents:
>
>    the domain of integration
>    the integrand
>    the measure
>
> (with, no doubt, some lack of clarity about the 'boundaries beteen these
three ingredients').
>
> In MathML we have:
>
> PMML, which confines itself to induividual bits of maotation, ignoring
the words in between;
>
> Pragmatic CMML, which tries to describe the semantics of some of the
isolated notation fragments that form part of some well-known
> phraseologies --- but to do this it often has to make assumptions about
what (or that something) is in the non-notational parts of those
phraseologies (see further below);
>
> Strict CMML which tries to ... (??) (I need one of those
> maction:fill-in-dots thingies here) and must 'align with' OM3,
> which tries to ... ??
>
> I am not even sure if these two '...' must have the same answer (for OM3
in general that is: they had better coincide on the part of OM£ that is
equivalent to Strict CMML).
>
> P-CMML (as it seems to me) therefore tries to describe the semantics
using a phraseology that is very close to the (presentation) structure
of the notation; this becomes more and more difficult and ad hoc as do
the notations being used.
>
> Some pertinent examples of common phraseologies within descriptions of
> 'the calculus of 1-dim real functions':
>
> Ph1: the use of (apparently unconditioned) 'mathematical (18/19C)
variables' and (untyped) expressions
>
> Ph2: the use of (20/21C) (single-valued, complete) functions with
(possibly implicit) well-defined domains and names (here $x^2$, and its
lambda-formalism, is simply the most common name given to many of the
'squaring functions'; there is no 'universal squarer' defined by an
(almost) untyped lambda-expression);
Possibly not EXPLICITLY, but I think people using it would agree that
there was A (universal) squaring function, evne though they didn't bother
to describe it explicitly.
> Ph3: the use of the notations and ideas from computational
> (mathematical, symbolic) logical with lamda-expressions and
> 'universality'.
Sorry - exactly what is the question?
But I do like the description of phases, and OM3, at least, has be AT
LEAST phase 2, and as far into phase 3 as is necessary, and i suppose that
is what we are debating.

James Davenport
Visiting Full Professor, University of Waterloo
Otherwise:
Hebron & Medlock Professor of Information Technology and
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009 IMU
Committee on Electronic Information and Communication