PS: << Several inaccuracies crept into the late-night writings below. Gentle reader, please help the embarrassed writer locate and fix them. Thank you so much! >>
On Thu, Jun 5, 2014 at 11:00 PM, Andreas Strotmann < [email protected]> wrote: > 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 >
_______________________________________________ Om3 mailing list [email protected] http://openmath.org/mailman/listinfo/om3
