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

[Professor James Davenport]

On Mon, March 23, 2009 12:17 pm, c.a.rowley at open.ac.uk wrote:
> James, Good morning!
Thanks - apparently it's -7.
> 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.
Indeed. In particular, though not exclusively, there is a strong element
of what CS would call "type inference". AS you point out, we don't all do
this the same way, and I suspect even mine is not amenable to full logical
description.
> 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').
Quite so, and there is a (small) group of people who woryy about this in
CA, and distinguish between 'variables ' and 'unknowns'.
> 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'.
This is a (doubtless intentionally) provocative statement, with which I
have some sympathy. Of course, it is technically false, a "pure,
context-free lambda-expression" expresses the mathematical semantics of
such an object in the lambda-calculus. Whether this is relevant to much of
the rest of the mathematics is the question.

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