[Om3] Results from the OM3/MathML3 telcon yesterday

Sat Oct 11 09:06:31 CEST 2008

Dear all,

yesterday at 17:00-18:00 CET we had the telcon on the future of complex
binding operators and the  condition element in OM3/MathML3.

Present: Olga Caprotti, David Carlisle, James Davenport, Michael
Kohlhase , Chris Rowley.
Minutes: see below.

We talked about the general construction of complex binding objects in
Michael's note and whehter this can be used to get around introducing a
counterpart of the MathML <condition> element into OpenMath for alignment.

Two results were reached:

   1. the group is happy with complex binding operators as a
      representation mechanism for MathML2 qualifier elements like
      <domainofapplication>, <degree>, or <uplimit>. Generally, the
      group finds that we should highlight the use of complex binding
      objects in the CDs and the specification as something that has
      always been possible in OpenMath, but has never been much used (to
      our knowledge). The group suggests that we will introduce special
      binding constructors like a forallset element, so that we can write|
      <OMBIND>
        <OMA><OMS cd="quant1" name="forallset"/><OMS name="R"
      cd="setname1"/></OMA>
        <something here/>
      </OMBIND>
   2. the group does not think that complex binding operators like the
      one above is a suitable representation measure for the <condition>
      qualifier element of pragmatic MathML. In particular, we do not
      want to accept the occurrence of the bound variable in the
      (complex) binding operator. In particular, the OpenMath2 standard
      restricts alpha-conversion to the second and third children of the
      OMBIND, which is consistent with this view.

So in particular the question whether we need a counterpart of the
<condition> element in OpenMath3 for alignment is not resolved yet. We
looked at various examples (see below) and feel we still need more to
understand the issue fully. The group gave itself the homework to
discuss these examples on the OM3 mailing list and set up another telcon
to take decisions when we made progress.

James was tasked to make sense of the integration/differentiation
examples from the MathML2 spec and make concrete suggestions for the
expression-based calculus CD.

Michael
-------------------------------------------8<-----------------------------------------------------

Olga Caprotti
17:16
Chris, James, MK, Olga are on the skype call
17:16

MK has not refined the original note
17:16

since the conditional symbols seems to be accepted
17:17

we need to work out the issue of the bound variable appearing in the binder
17:18

bind(@(forall_onSet,x,x>0), x, x^3>0))
Olga Caprotti added j.h.davenport to this chat
17:18
Olga Caprotti added Chris Rowley to this chat
17:18
Olga Caprotti
17:18
bind(@(forall_onSet,x,x>0), x, x^3>0))
17:19

we need to work out the issue of the bound variable appearing in the binder
17:19

we now state that alpha-renaming can occur only in body of bind
17:20

which would not work in example as above
j.h.davenport
17:20
That's right, I think the problem was in integrals, where people write
int_0^x f(x)dx
Olga Caprotti
17:21
last child of bind
17:21

1st child is binding operator
17:21

2nd child is bound vars
j.h.davenport
17:23
I am not sure about the semantics of forallonset
Michael Kohlhase
17:23
bind(@(forall_cond,x>0), x, x^3>0))
j.h.davenport
17:24
But that is precisely equivalent to bind(forall,x,implies(x>0,x^3>0))
Olga Caprotti
17:24
bind(forall,x,cond(x>0)-> Body)
Michael Kohlhase
17:25
bind(@(int_cond,x>0),x,x^2)
j.h.davenport
17:26
Is that int_0^\inftyx^2
Michael Kohlhase
17:26
bind(@(lambda_cond,x>0),x,x^2)
j.h.davenport
17:27
But MathML's interator isn't really a binder, since the variable of
integration might be free in the result
Chris Rowley
17:29
bind(@(lambda),x,x^2
j.h.davenport
17:31
I think STRONGLY that they are functions, in the sense fo my talk,
rather than expressions.
Michael Kohlhase
17:31
I am not sure that you agree what a function is
j.h.davenport
17:31
The problem is that a lambda-expression in the lambda-calculus isn't
(quite) the ZF definition.
Michael Kohlhase
17:32
we can give the domain as in bind(lambda,x:A,x^2)
17:33

bind (@(typed_lambda,A),x x^2)
17:34

bind (@(cond_lambda,in(x,A),x x^2)
Olga Caprotti added davidcarlisle to this chat
17:34
j.h.davenport
17:34
I don't like Michael's last example. why not
17:35

bind(@(cond_lambda(@lambda(y, in(y,A)),x,x^2))
17:36

and ther eis (independent) alpha-conversion on the y and x: t would be
USUAL to make them the same, but logically they are not.
17:39

What we really want is a predicate_lambda, and predicate_forall
17:41

Olga argued for examples of complicated binding operators, such as typed
lambdas
Olga Caprotti
17:42
David says STS has to be fixed also
j.h.davenport
17:42
david: STS doesn't really handle binders, even simpler ones
17:44

MK proposes we need examples of what is already permitted, i.e.g typed
lambda.
17:45

I think tham MathML bind(x,condition(foo(x)), bar(x))
Michael Kohlhase
17:45
bind(forall,x cond(x>0), x>2)
17:46

bind(lambda, x, cond (x>0), x^2)
j.h.davenport
17:46
MK's example becomes bind(forallpred(lambda(x),x>0)) x,x^2)
17:47

Where two bindings operations take place. Normally, we wil use the same
name in math. vernacualr, but logically two bindings are taking place.
17:48

So my xample a-converst to bind(forallpred(lambda(z),z>0)) x,x^2) or
bind(forallpred(lambda(x),x>0)) y,y^2)
17:49

bind(lambdapred(bind(lambda(x),x>0))) y,y^2)
17:50

Sorry - can you write it?
Michael Kohlhase
17:50
bind(csymbol,x,x>0)
17:51

bind (csymbol, x, cond (x>0), f(x))
17:51

james: bind (csymbolcond (lambda
Olga Caprotti
17:53
bind(cond(csymbol,lambda(x).cond(x)), y, fy)
j.h.davenport
17:54
bind(csymbolcond(bind(lambda,x,cond(x)),y,f(y))
18:02

So david is asking for a 'generic' example. Good, but I would laos like
to know what the specific examples in the MathML standard are that are
causing problems.
Olga Caprotti
18:04
JHD thinks introducing quantifiers over a Set is a good idea
j.h.davenport
18:04
David: James should look at MathML2 (chapter 4).
18:06

MK: chapter 4 AND appendix

-- 
----------------------------------------------------------------------
 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
----------------------------------------------------------------------