[Om] Multistep "equation" symbol?
Professor James Davenport
jhd at cs.bath.ac.uk
Thu May 14 01:12:28 CEST 2009
On Wed, May 13, 2009 10:27 pm, Michael Kohlhase wrote:
> On 14.05.2009 0:03 Uhr, Professor James Davenport wrote:
>> On Wed, May 13, 2009 12:39 am, Michael Kohlhase wrote:
>> One can even have formalised reasons inside a CD - see logic3 for this.
> Ah, I was unaware of logic3, I will have to have a look at that. And of
> course, this corresponds very much to what we are using in OMDoc as
> "proof terms" via the Curry/Howard Isomorphism (CHI). And indeed using
> the CHI, one could interpret the equations as Proof terms (embedded
> into) mathematical discourse in general. As I said, I will have to think
> about an example here.
Please do - logic3 was intended as the start of a debate here.
>>> Now, this already points to a problem in OpenMath, we can _informally_
>>> say this in a CMP, but not formally in a FMP, since OM does not have a
>>> concept of sequence variables (or meta-level elision) that can be
>>> quantified over.
>> We've had this problem before, and maybe the time is coming to have this
>> debate more formally, maybe in a business session/panel at OM2009?
> I am not sure that the business section would be the right spot, but I
> think we may have to make a panel for open issues, which this certainly
> is. Given that I have been thinking about the "semantics of OpenMath",
> we also have to talk about the "linguistics of OpenMath", I think. It
> seems to me that formulae in mathematical texts are used and have a
> meaning on two levels (which is something we see in linguistics):
> 1. the "compositional" level (I do not have a good word for this, so
> I will try this). Here we have the formulae as interpreted
> objects, where we cannot look into them (therefore the word
> compositional, since there the meaning of a complex object is only
> determined by the meanings of the operator and arguments). The
> compositional meaning of 2+3 _is_ 5 (as an indivisible
> mathematical object).
But many OM-processors do not have this level of interpretation
(typesetters, data bases etc.).
> 2. the "representational" level, where an object is just a formula
> (tree) i.e. (almost) an OpenMath Object. Here we can talk about
> subterms (and names of bound variables in fact). This level is
> also used in Math, we can point to subformulae (that are
> inaccesible at the compositional level): e.g. in "... note that
> the second argument of the left hand side of the equation above is
> not in standard form, so..."
> I think that in a "discourse theory of mathematics" (as I am attempting
> to make in OMDoc) this is an important thing to understand. And I think
> that it may be important for OM as well.
> OK, I hope you are not too bored at my attempts of philosophy.
Not at all, but isn't level 1 what we have been calling "evaluation"
(perhaps better expressed, though).
Visiting Full Professor, University of Waterloo
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
More information about the Om