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

[Professor James Davenport]

On Mon, March 23, 2009 12:51 pm, David Carlisle wrote:
>> 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.
> It's perfectly reasonably (but a big change) to want to base things on a
> typed (or conditioned) system rather than an untyped one. (Not sure that
> OM could survive the surgery required, but it's certainly something that
> could be considered).
A very good statement. I wonder what the ECC people have to say?
> But that seems a more or less completely separate issue from
> James/Michael's proposal, which doesn't add a distinguished syntactic
> component to OMBind for conditions (such as the once proposed OMC element)
> but rather just adds an open ended list of expression terms to be
> included in the binding, which may (on a symbol-by-symbol basis) be
> taken to be conditions on the bound variable, or constituent subterms
> of the expression being bound or anything else.
That's true, though the symbol would have to state (via STS, and we
haven't discussed the necessary extension to STS) WHETHER it accepted them
at all, and the FMP would presumably say something about them, though
that's certainly a pretty weak presumption.
Another difference is that a 'condition' in JHD/MK, is also rather
different from a type. \forall n\in\N (which doesn't need JHD/MK) is
pretty learly a type as well as a condition, but (x,y,z)\in ellipsoid ((4)
in JHD/MK) is harder to view as a type, though there are type theorists
who could.

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