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

[Andreas Strotmann]

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 <
andreas.strotmann at gmail.com> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://openmath.org/pipermail/om3/attachments/20140606/2aa58318/attachment.html>