[Om3] Skype F2F for calculus3 and condition element in OpenMath
Michael Kohlhase
m.kohlhase at jacobs-university.de
Wed Oct 1 13:06:33 CEST 2008
Dear all,
we had the F2Fcall today, and I have pasted the chat protocol below. The
main outcomes are
1. we want to have a new CD for the differential calculus view of
differentiation and integration, which is closer to the MathML
view. James will continue/correct Michael's note and the
calculus3.ocd (name decision pending).
2. We will need some careful wording about the pragmatic-strict
mapping in Chapter 4 of the MathML spec. Michael will supply a
first draft. We are also worried about the general definability of
qualifiers in terms of <condition>
3. We have discussed, but not totally understood the second issue
addressed in Michael's note, namely the possibility to get by in
OpenMath and strict MathML without a <condition> element. This
needs some careful thinking about examples. The main sticky point
seems to be that in order to represent condition as an argument to
a complex binding operator, alpha conversion needs to be extended
to complex binding operators (currently not allowed).
4. To discuss these issues further, we will need to have another F2F
call. Michael will start a Doodle.
I think this is it, please reply to this mail with suggestions, comments
and corrections.
Michael
P.S. I will send the upper part of this e-mail to the MathML mailing
list for informational purposes.
-------------------------8<-------------------------------
JHD: I have pointed out that OM's calculus1 encodes 'hard analysis',
differentiation as an operator of functions, whereas MathML encodes
differnetial algebra. Perhaps we need two CDs.
Michael Kohlhase
12:10 PM
that is what I tried to do with the note
j.h.davenport
12:10 PM
It is possible to write FMPs which, in SOME cases, relate the two.
12:11 PM
It strikes me that MOST uses in 'casual' maths are the differential
algebra sort, whereas in an analysis text, we are largely takingthe OM view.
12:12 PM
I agree with MK that SOME teasing apart the DA view and the analysis
view might well help.
12:14 PM
Whatever we do will need to be documented carefully.
Michael Kohlhase
12:15 PM
I agree with david that the expressions cd would have a differentiation
operation of the form apply(x,x^2) --> 2x.
j.h.davenport
12:15 PM
So I'll work on Michael's paper to express this difference
Michael Kohlhase
12:16 PM
The note is in the repos at
http://svn.openmath.org/OpenMath3/doc/blue/noconds/note.tex
12:17 PM
The calculus3.ocd is also in the repository, it can be a starting point
for James
j.h.davenport
12:18 PM
The relation between 'log' as a function in transc1 and 'log' as
int(1/x) is a deep one.
Michael Kohlhase
12:20 PM
decision: we need a second CD for differential calculus view of
differentiation and integration. James is going to supply a first draft
and hte others comment
j.h.davenport
12:20 PM
I have suggeste dthat in parallel James works on the note to document
DA/analysis points of view, and the OM/MathML people work on the details
of the current calculus3
paul_libbrecht
12:21 PM
cdfiles2/contrib/cd/calculus2.ocd
12:21 PM
is the file we don't know the history of.
j.h.davenport
12:22 PM
Michael objects to confusing 'integral over a path' and 'integral over a
set'
Michael Kohlhase
12:23 PM
and we should be able to say \int_a^b= - \int_b^a without blushing
paul_libbrecht
12:24 PM
Paul: all these integrals are different concepts, they should be
different symbols!
j.h.davenport
12:25 PM
(all: are we coercing intervals into paths?).
12:25 PM
PL shouldn't we have different kinds of integrals?
12:27 PM
Isn't MK's exxample actually the DEFN of integrals when b<a?
paul_libbrecht
12:27 PM
(James, yes it is)
j.h.davenport
12:28 PM
MK - one answer is to delete the example!
12:28 PM
DC: but K12 needs that
Michael Kohlhase
12:28 PM
I would really not like to delete the example. but we should move it to
another symbol
j.h.davenport
12:30 PM
int_a^b = (if a<b then int(f,interval) else -int(f,interval))
12:33 PM
The differential algebra point of view really only deals with INDEFINITE
integration
paul_libbrecht
12:34 PM
(sure)
j.h.davenport
12:35 PM
It's still TRUE, whether or not it's decidable.
12:36 PM
intlimits_a^b = (if a<b then intset(f,interval(a,b)) else
-intset(f,interval(b,a)))
12:36 PM
Note that this relates two DIFFERENT concenpts, and probably two symbols.
12:38 PM
Decision: intlimits is different from intset
Michael Kohlhase
12:38 PM
I propose to add something like intlimits to calculus1.ocd
12:39 PM
DC: we need some careful words on the MathML side for this
12:41 PM
Decision: we will add the necessasry symbols and worry about the
pragmatic-to-strict mapping later.
davidcarlisle
12:41 PM
in particular mml2 allows the mapping of arbitrary symbols with
qualifiers with a defined normalisation of uplimit and friends to a
single condition
j.h.davenport
12:44 PM
OC: adding 'condition' changes the abstract model
Michael Kohlhase
12:45 PM
DC now arguments for an extension of OpenMath with <condition> in some way.
12:45 PM
on the grounds that for a lambda we cannot really encode the condition
in a general way
j.h.davenport
12:46 PM
DC is arguing that <condition> should be ALWAYS allowed, and SOMETIMES
defined??
12:47 PM
MK: a complex binding object can do the same task (see page 5)
Michael Kohlhase
12:49 PM
consider forall x>0. x>5
12:49 PM
x>0 is the condition
12:49 PM
represent this as bind(@(forall,x>0) x>5)
12:50 PM
sorry: bind(@(forall,x>0),bvar(x), x>5)
12:51 PM
sorry, this is a new forall, so consider
bind(@(forallcond,x>0),bvar(x), x>5)
paul_libbrecht
12:57 PM
btw... intergeo spec actually relies on constraints... pretty
condition-tasting.Olga Caprotti
12:01 PM
here
paul_libbrecht
12:02 PM
yes here.
j.h.davenport
12:02 PM
And James
Michael Kohlhase
12:07 PM
Do we have a scribe?
j.h.davenport
12:08 PM
Isn't chat itself a scribe?
12:10 PM
JHD: I have pointed out that OM's calculus1 encodes 'hard analysis',
differentiation as an operator of functions, whereas MathML encodes
differnetial algebra. Perhaps we need two CDs.
Michael Kohlhase
12:10 PM
that is what I tried to do with the note
j.h.davenport
12:10 PM
It is possible to write FMPs which, in SOME cases, relate the two.
12:11 PM
It strikes me that MOST uses in 'casual' maths are the differential
algebra sort, whereas in an analysis text, we are largely takingthe OM view.
12:12 PM
I agree with MK that SOME teasing apart the DA view and the analysis
view might well help.
12:14 PM
Whatever we do will need to be documented carefully.
Michael Kohlhase
12:15 PM
I agree with david that the expressions cd would have a differentiation
operation of the form apply(x,x^2) --> 2x.
j.h.davenport
12:15 PM
So I'll work on Michael's paper to express this difference
Michael Kohlhase
12:16 PM
The note is in the repos at
http://svn.openmath.org/OpenMath3/doc/blue/noconds/note.tex
12:17 PM
The calculus3.ocd is also in the repository, it can be a starting point
for James
j.h.davenport
12:18 PM
The relation between 'log' as a function in transc1 and 'log' as
int(1/x) is a deep one.
Michael Kohlhase
12:20 PM
decision: we need a second CD for differential calculus view of
differentiation and integration. James is going to supply a first draft
and hte others comment
j.h.davenport
12:20 PM
I have suggeste dthat in parallel James works on the note to document
DA/analysis points of view, and the OM/MathML people work on the details
of the current calculus3
paul_libbrecht
12:21 PM
cdfiles2/contrib/cd/calculus2.ocd
12:21 PM
is the file we don't know the history of.
j.h.davenport
12:22 PM
Michael objects to confusing 'integral over a path' and 'integral over a
set'
Michael Kohlhase
12:23 PM
and we should be able to say \int_a^b= - \int_b^a without blushing
paul_libbrecht
12:24 PM
Paul: all these integrals are different concepts, they should be
different symbols!
j.h.davenport
12:25 PM
(all: are we coercing intervals into paths?).
12:25 PM
PL shouldn't we have different kinds of integrals?
12:27 PM
Isn't MK's exxample actually the DEFN of integrals when b<a?
paul_libbrecht
12:27 PM
(James, yes it is)
j.h.davenport
12:28 PM
MK - one answer is to delete the example!
12:28 PM
DC: but K12 needs that
Michael Kohlhase
12:28 PM
I would really not like to delete the example. but we should move it to
another symbol
j.h.davenport
12:30 PM
int_a^b = (if a<b then int(f,interval) else -int(f,interval))
12:33 PM
The differential algebra point of view really only deals with INDEFINITE
integration
paul_libbrecht
12:34 PM
(sure)
j.h.davenport
12:35 PM
It's still TRUE, whether or not it's decidable.
12:36 PM
intlimits_a^b = (if a<b then intset(f,interval(a,b)) else
-intset(f,interval(b,a)))
12:36 PM
Note that this relates two DIFFERENT concenpts, and probably two symbols.
12:38 PM
Decision: intlimits is different from intset
Michael Kohlhase
12:38 PM
I propose to add something like intlimits to calculus1.ocd
12:39 PM
DC: we need some careful words on the MathML side for this
12:41 PM
Decision: we will add the necessasry symbols and worry about the
pragmatic-to-strict mapping later.
davidcarlisle
12:41 PM
in particular mml2 allows the mapping of arbitrary symbols with
qualifiers with a defined normalisation of uplimit and friends to a
single condition
j.h.davenport
12:44 PM
OC: adding 'condition' changes the abstract model
Michael Kohlhase
12:45 PM
DC now arguments for an extension of OpenMath with <condition> in some way.
12:45 PM
on the grounds that for a lambda we cannot really encode the condition
in a general way
j.h.davenport
12:46 PM
DC is arguing that <condition> should be ALWAYS allowed, and SOMETIMES
defined??
12:47 PM
MK: a complex binding object can do the same task (see page 5)
Michael Kohlhase
12:49 PM
consider forall x>0. x>5
12:49 PM
x>0 is the condition
12:49 PM
represent this as bind(@(forall,x>0) x>5)
12:50 PM
sorry: bind(@(forall,x>0),bvar(x), x>5)
12:51 PM
sorry, this is a new forall, so consider
bind(@(forallcond,x>0),bvar(x), x>5)
paul_libbrecht
12:57 PM
btw... intergeo spec actually relies on constraints... pretty
condition-tasting.Olga Caprotti
12:01 PM
here
paul_libbrecht
12:02 PM
yes here.
j.h.davenport
12:02 PM
And James
Michael Kohlhase
12:07 PM
Do we have a scribe?
j.h.davenport
12:08 PM
Isn't chat itself a scribe?
12:10 PM
JHD: I have pointed out that OM's calculus1 encodes 'hard analysis',
differentiation as an operator of functions, whereas MathML encodes
differnetial algebra. Perhaps we need two CDs.
Michael Kohlhase
12:10 PM
that is what I tried to do with the note
j.h.davenport
12:10 PM
It is possible to write FMPs which, in SOME cases, relate the two.
12:11 PM
It strikes me that MOST uses in 'casual' maths are the differential
algebra sort, whereas in an analysis text, we are largely takingthe OM view.
12:12 PM
I agree with MK that SOME teasing apart the DA view and the analysis
view might well help.
12:14 PM
Whatever we do will need to be documented carefully.
Michael Kohlhase
12:15 PM
I agree with david that the expressions cd would have a differentiation
operation of the form apply(x,x^2) --> 2x.
j.h.davenport
12:15 PM
So I'll work on Michael's paper to express this difference
Michael Kohlhase
12:16 PM
The note is in the repos at
http://svn.openmath.org/OpenMath3/doc/blue/noconds/note.tex
12:17 PM
The calculus3.ocd is also in the repository, it can be a starting point
for James
j.h.davenport
12:18 PM
The relation between 'log' as a function in transc1 and 'log' as
int(1/x) is a deep one.
Michael Kohlhase
12:20 PM
decision: we need a second CD for differential calculus view of
differentiation and integration. James is going to supply a first draft
and hte others comment
j.h.davenport
12:20 PM
I have suggeste dthat in parallel James works on the note to document
DA/analysis points of view, and the OM/MathML people work on the details
of the current calculus3
paul_libbrecht
12:21 PM
cdfiles2/contrib/cd/calculus2.ocd
12:21 PM
is the file we don't know the history of.
j.h.davenport
12:22 PM
Michael objects to confusing 'integral over a path' and 'integral over a
set'
Michael Kohlhase
12:23 PM
and we should be able to say \int_a^b= - \int_b^a without blushing
paul_libbrecht
12:24 PM
Paul: all these integrals are different concepts, they should be
different symbols!
j.h.davenport
12:25 PM
(all: are we coercing intervals into paths?).
12:25 PM
PL shouldn't we have different kinds of integrals?
12:27 PM
Isn't MK's exxample actually the DEFN of integrals when b<a?
paul_libbrecht
12:27 PM
(James, yes it is)
j.h.davenport
12:28 PM
MK - one answer is to delete the example!
12:28 PM
DC: but K12 needs that
Michael Kohlhase
12:28 PM
I would really not like to delete the example. but we should move it to
another symbol
j.h.davenport
12:30 PM
int_a^b = (if a<b then int(f,interval) else -int(f,interval))
12:33 PM
The differential algebra point of view really only deals with INDEFINITE
integration
paul_libbrecht
12:34 PM
(sure)
j.h.davenport
12:35 PM
It's still TRUE, whether or not it's decidable.
12:36 PM
intlimits_a^b = (if a<b then intset(f,interval(a,b)) else
-intset(f,interval(b,a)))
12:36 PM
Note that this relates two DIFFERENT concenpts, and probably two symbols.
12:38 PM
Decision: intlimits is different from intset
Michael Kohlhase
12:38 PM
I propose to add something like intlimits to calculus1.ocd
12:39 PM
DC: we need some careful words on the MathML side for this
12:41 PM
Decision: we will add the necessasry symbols and worry about the
pragmatic-to-strict mapping later.
davidcarlisle
12:41 PM
in particular mml2 allows the mapping of arbitrary symbols with
qualifiers with a defined normalisation of uplimit and friends to a
single condition
j.h.davenport
12:44 PM
OC: adding 'condition' changes the abstract model
Michael Kohlhase
12:45 PM
DC now arguments for an extension of OpenMath with <condition> in some way.
12:45 PM
on the grounds that for a lambda we cannot really encode the condition
in a general way
j.h.davenport
12:46 PM
DC is arguing that <condition> should be ALWAYS allowed, and SOMETIMES
defined??
12:47 PM
MK: a complex binding object can do the same task (see page 5)
Michael Kohlhase
12:49 PM
consider forall x>0. x>5
12:49 PM
x>0 is the condition
12:49 PM
represent this as bind(@(forall,x>0) x>5)
12:50 PM
sorry: bind(@(forall,x>0),bvar(x), x>5)
12:51 PM
sorry, this is a new forall, so consider
bind(@(forallcond,x>0),bvar(x), x>5)
paul_libbrecht
12:57 PM
btw... intergeo spec actually relies on constraints... pretty
condition-tasting.Olga Caprotti
12:01 PM
here
paul_libbrecht
12:02 PM
yes here.
j.h.davenport
12:02 PM
And James
Michael Kohlhase
12:07 PM
Do we have a scribe?
j.h.davenport
12:08 PM
Isn't chat itself a scribe?
12:10 PM
JHD: I have pointed out that OM's calculus1 encodes 'hard analysis',
differentiation as an operator of functions, whereas MathML encodes
differnetial algebra. Perhaps we need two CDs.
Michael Kohlhase
12:10 PM
that is what I tried to do with the note
j.h.davenport
12:10 PM
It is possible to write FMPs which, in SOME cases, relate the two.
12:11 PM
It strikes me that MOST uses in 'casual' maths are the differential
algebra sort, whereas in an analysis text, we are largely takingthe OM view.
12:12 PM
I agree with MK that SOME teasing apart the DA view and the analysis
view might well help.
12:14 PM
Whatever we do will need to be documented carefully.
Michael Kohlhase
12:15 PM
I agree with david that the expressions cd would have a differentiation
operation of the form apply(x,x^2) --> 2x.
j.h.davenport
12:15 PM
So I'll work on Michael's paper to express this difference
Michael Kohlhase
12:16 PM
The note is in the repos at
http://svn.openmath.org/OpenMath3/doc/blue/noconds/note.tex
12:17 PM
The calculus3.ocd is also in the repository, it can be a starting point
for James
j.h.davenport
12:18 PM
The relation between 'log' as a function in transc1 and 'log' as
int(1/x) is a deep one.
Michael Kohlhase
12:20 PM
decision: we need a second CD for differential calculus view of
differentiation and integration. James is going to supply a first draft
and hte others comment
j.h.davenport
12:20 PM
I have suggeste dthat in parallel James works on the note to document
DA/analysis points of view, and the OM/MathML people work on the details
of the current calculus3
paul_libbrecht
12:21 PM
cdfiles2/contrib/cd/calculus2.ocd
12:21 PM
is the file we don't know the history of.
j.h.davenport
12:22 PM
Michael objects to confusing 'integral over a path' and 'integral over a
set'
Michael Kohlhase
12:23 PM
and we should be able to say \int_a^b= - \int_b^a without blushing
paul_libbrecht
12:24 PM
Paul: all these integrals are different concepts, they should be
different symbols!
j.h.davenport
12:25 PM
(all: are we coercing intervals into paths?).
12:25 PM
PL shouldn't we have different kinds of integrals?
12:27 PM
Isn't MK's exxample actually the DEFN of integrals when b<a?
paul_libbrecht
12:27 PM
(James, yes it is)
j.h.davenport
12:28 PM
MK - one answer is to delete the example!
12:28 PM
DC: but K12 needs that
Michael Kohlhase
12:28 PM
I would really not like to delete the example. but we should move it to
another symbol
j.h.davenport
12:30 PM
int_a^b = (if a<b then int(f,interval) else -int(f,interval))
12:33 PM
The differential algebra point of view really only deals with INDEFINITE
integration
paul_libbrecht
12:34 PM
(sure)
j.h.davenport
12:35 PM
It's still TRUE, whether or not it's decidable.
12:36 PM
intlimits_a^b = (if a<b then intset(f,interval(a,b)) else
-intset(f,interval(b,a)))
12:36 PM
Note that this relates two DIFFERENT concenpts, and probably two symbols.
12:38 PM
Decision: intlimits is different from intset
Michael Kohlhase
12:38 PM
I propose to add something like intlimits to calculus1.ocd
12:39 PM
DC: we need some careful words on the MathML side for this
12:41 PM
Decision: we will add the necessasry symbols and worry about the
pragmatic-to-strict mapping later.
davidcarlisle
12:41 PM
in particular mml2 allows the mapping of arbitrary symbols with
qualifiers with a defined normalisation of uplimit and friends to a
single condition
j.h.davenport
12:44 PM
OC: adding 'condition' changes the abstract model
Michael Kohlhase
12:45 PM
DC now arguments for an extension of OpenMath with <condition> in some way.
12:45 PM
on the grounds that for a lambda we cannot really encode the condition
in a general way
j.h.davenport
12:46 PM
DC is arguing that <condition> should be ALWAYS allowed, and SOMETIMES
defined??
12:47 PM
MK: a complex binding object can do the same task (see page 5)
Michael Kohlhase
12:49 PM
consider forall x>0. x>5
12:49 PM
x>0 is the condition
12:49 PM
represent this as bind(@(forall,x>0) x>5)
12:50 PM
sorry: bind(@(forall,x>0),bvar(x), x>5)
12:51 PM
sorry, this is a new forall, so consider
bind(@(forallcond,x>0),bvar(x), x>5)
paul_libbrecht
12:57 PM
btw... intergeo spec actually relies on constraints... pretty
condition-tasting.
Michael Kohlhase wrote:
> Dear all,
>
> a couple of days back I sent around a note proposing a new calculus3 CD
> and in it a new representational style using complex binding operators
> that allows to get by without condition elements. This is important for
> the OpenMath/MathML alignment, since if we do not find a way to get by
> without a <condition> element in strict content MathML, we will need to
> introduce one in OpenMath, which would be a large change in the language.
>
> Unfortunately, there has not been a lot of response to the proposal, but
> I am not willing to interpret this as a sign of "no opposition". We need
> to discuss this proposal in depth and estimate the consequences for
> OpenMath and MathML. We also need to move forward since the MathML WG
> needs to prepare a final call working draft relatively soon.
>
> Therefore I am calling a virtual Face2Face meeting via Skype conference.
> To plan a date I have prepared a poll at
> http://www.doodle.ch/2d9uyxmczvq2gk6s So if you are interested in this
> topic or think you have something to contribute, please head over there
> and specify your free slots until monday September 29. 23:59 CET.
>
> If you want to prepare, the note is at
> https://svn.openmath.org/OpenMath3/doc/blue/noconds/note.pdf
>
> Michael
>
>
--
----------------------------------------------------------------------
Prof. Dr. Michael Kohlhase, Office: Research 1, Room 62
Professor of Computer Science Campus Ring 12,
School of Engineering & Science D-28759 Bremen, Germany
Jacobs University Bremen* tel/fax: +49 421 200-3140/-493140
m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase
skype: m.kohlhase * International University Bremen until Feb. 2007
----------------------------------------------------------------------
-------------- next part --------------
A non-text attachment was scrubbed...
Name: m_kohlhase.vcf
Type: text/x-vcard
Size: 320 bytes
Desc: not available
Url : http://openmath.org/pipermail/om3/attachments/20081001/88956d0c/attachment.vcf
More information about the Om3
mailing list