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
