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

[c.a.rowley at open.ac.uk]

James

Good morning!

Everyone,

This message starts from our sparring and moves towards supporting the K&D
extension to OM3 ... But maybe not sharing their reasoning!  Presumably
this restores normality by putting me at odds with David C again:-).

On the way it expresses some concerns about universally parametrised
expressions and their expressivity for 'mathematics as we (or I) know it'.


chris

>>>
On Mon, March 23, 2009 12:07 am, c.a.rowley at open.ac.uk wrote:
>
>
> Well spotted, James: but you are making an (entirely reasonable)
> assumption
> about the measure.
>
> Add |cos z| = 1 to the domain if you wish but then you will complain that
> it is (assuming z is a 'real variable', of course).
Which I did since $z<0$. I (subconsciously) played Axiom in my head and
looked for an ordered set with a cos functions.
>>>

... maybe not you, but I would have started from the assumtion that z -->
'complex variable' until, as you found, that becomes untenable and starting
to 'calculate the universal element in some subcategory'.

The moral (or executive summary) being that this is exactly how many
mathematical formulas communicate their meaning: both by using assumptions
about deductions that the reader will make and/or by (more or less
implicitly) pointing out that the assumptions may be wrong.

This shows both the communicative (to humans) power of such very
abbreviated maths notations and the fact that much of it works only with
humans who make exactly the correct deductions about unstated assumptions
(particularly about 'variables').

The question is whether the 'mathematical semantics' can be said to be
captured without making explicit certain features that are often, but not
always, absent or very much implicit in the notation typically used.  They
probably can in the computational and logical sense of semantics but is
this level of expressivity:

-- all that OM3 is trying to achieve?

-- sufficient for the 'semanticly rich encoding of mathematical material'

For example, when encoding useful, concrete 'mathematical semantics' in the
21C, is the concept of an:

  expression in a 'universal' or 'unconditional' bound variable

sufficient to encode 'a function' or only a 'template for a collection of
functions'?

Further if it is the only the latter, what has this got to do with concrete
mathematics as she is done and taught by many mathematicians?

Thus it is the (apparently or actually) 'unconditioned variables' that
worry me: they are great for symbolic logic but that is not much of
'mathematics as we know it'.  Even 19C (and probably 17-18C) 'variables'
were not 'universal' but are (possibly by assumption) 'real' or 'complex'
variables or integers (or often more concretely 'quantities').

As soon as the variables get conditioned then one gets some idea of the
'domain over which they range': something that is essential if they are in
fact being used to 'describe a function'.  And in anything I would describe
as 'every day mathematics' such function-like things, with definite domains
available when needed, are (and have been at least since Cauchy)
fundamental and omni-present.

Hence I want all 'bindings' in OM to require a 'condition on the bound
variables'.  Syntactically this can, perhaps, be omitted but with an
assumed default value.

Manifesto: a pure, context-free lambda-expression neither describes a
mathematical function nor expresses any 'mathematical semantics'.

---------------------------------------------------------------------------
The Open University is incorporated by Royal Charter (RC 000391), an exempt
charity in England & Wales and a charity registered in Scotland (SC 038302)