[Om3] Summary of the Davenport&Kohlhase Proposal

[David Carlisle]

Florian,

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.

>   OMBIND(sum, OMBVAR(OMATTR(OMATP(type,nat), OMATP(condition,
>   prime(x)), OMV(x))), f(x))

But arith1:sum is used with OMA not OMBIND so if we use that, your one
variable example would be something like

  OMA(arith1:sum, setname1:P, f)

and your two variable example would be   (abbreviated)

 OMA(arith1:sum, 
   OMA(set1:suchthat, setname1:N*setname1:N,  OMBIND(lambda i j OMA(neq i j)))
   f
)

which again doesn't need any change to anything.

David

________________________________________________________________________
The Numerical Algorithms Group Ltd is a company registered in England
and Wales with company number 1249803. The registered office is:
Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom.

This e-mail has been scanned for all viruses by Star. The service is
powered by MessageLabs. 
________________________________________________________________________