[Om3] homework, describing a definition for n-ary plus

[Andreas Strotmann]

Sorry to butt in here, but I believe that what you are looking for is
something like this, in a lambda calculus sense:

  plus =  compose(sum, sequence, get_args)

where

  sum = reduce(plus2)

(with "sequence" denoting a casting operator, used here so it doesn't
matter which concrete form the arg list gets fetched in, and "reduce" being
an operator that takes a function and returns a binder)

or generally

  nary_op(bin_op) = compose(big_op(bin_op), sequence, get_args, where
big_op(bin_op) = reduce(bin_op)

(Note that these exact equations only hold for commutative bin_ops; for
others, one needs to distinguish between left_reduce and right_reduce.)

The two-step definition of the n-ary operator via the "big" operator
isolates the recursion in the definition of the "reduce" operator, which is
available in many programming languages, if in a slightly different form.

Unfortunately, AFAIK, Openmath 2, unlike OpenMath 1, disallows expressing
these equations - perhaps that should be corrected?

(Note also that, AFAIR, these equation pairs formed the theoretical basis
for the definition of n-ary operator semantics in certain contexts in
MathML 2.1+.)

See also Davenport&Kohlhase (or Kohlhase&Davenport)'s paper on big_ops.

Best regards,

 -- Andreas Strotmann
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://openmath.org/pipermail/om3/attachments/20140605/52123601/attachment.html>