[Om3] Skype F2F for calculus3 and condition element in OpenMath

[Professor James Davenport]

On Sun, September 28, 2008 10:15 pm, David Carlisle wrote:
> page 2/page3
>
> I don't think that you can model diff and partialdiff as a binding
> operator. (It
> may use a binding operator somewhere but if you do that you have to wrap
> it in an apply to a free variable.
Indeed, but looking at it, OpenMath's current hands aren't clean either.
The example in calculus1.ocd:
  derivative(x + 1.0) = 1.0
has as its answer
 <OMF dec="1.0"/>
(which is STS-incorrect), and should have
        <OMBIND>
          <OMS cd="fns1" name="lambda"/>
          <OMBVAR>
            <OMV name="x"/>
          </OMBVAR>
          <OMF dec="1.0"/>
        </OMBIND>
[Of course, an Algol68er would say that we have merely applied the
coercion of deproceduring, but that isn't spelled out in the STS spec]
> eg the first example on page 3, which is
>
> d x^2/dx
>
> x is _free_ in that expression.
>
> If we model a functional view of differentiation so need to bind x first
> then you need to apply the derivative function to a free variable x at
> the end.
>
> (D(lambda x. x^2))(x)
>
Of course, in OM, (D(lambda x. x^2)) is the same as (D(lambda y. y^2)),
which again might surprise people.

James Davenport
Hebron & Medlock Professor of Information Technology
Formerly RAE Coordinator and Undergraduate Director of Studies, CS Dept
Lecturer on CM30070, 30078, 50209, 50123, 50199
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor
IMU Committee on Electronic Information and Communication