[Om3] Summary of the Davenport&Kohlhase Proposal

[Florian Rabe]

Hi David,

> I must be missing something
> If you want to encode
>
>>  \sum_{i,j\in N} f(i,j)
> using attributed variables then
>
>>  \sum_{i,j\in N, i \neq j} f(i,j)
>
> appears to be just the same with the addition of an additional
> attribution, on the inner variable, namely
>
> replace
>
> OMBVAR(OMATTR(OMATP(type,N), OMV(i)), OMATTR(OMATP(type,N), OMV(j)))
>
> by
>
> OMBVAR(OMATTR(OMATP(type,N), OMV(i)), OMATTR(OMATP(type,N) OMATP(neq,OMV(i)), OMV(j)))
>
> which doesn't need any of the complication of  the suggested versions,
> and doesn't rewuire a change in OpeMATH.

You're right - I forgot Option 7.

7) Give condition as attribution to the last bound variable.

pro: works in OpenMath 2
con: a condition that is symmetric in its variables is represented asymmetrically

> But arith1:sum is used with OMA not OMBIND

I just used "sum" as an example for some binder that's not represented via higher-order abstract syntax and lambda terms.

Cheers,
Florian