STS documentation is unclear about binders

[jbs1]

migrated from Trac, where originally posted by lars_h on 20-May-2014 1:28pm

As pointed out in Appendix B of http://ceur-ws.org/Vol-1010/paper-21.pdf (paper from OpenMath2013), the declaration of binders in the Small Type System suffers from two problems:

1. http://www.openmath.org/standard/sts.pdf specifies that the sts#binder symbol should be an application like sts#mapsto: it takes two arguments and produces the type of a corresponding binder. However, the binder symbols of the official content dictionaries all have an STS signature where sts#binder is used as a constant, and that is indeed the Role this symbol has in version 4 of sts.ocd.
2. If one wishes to specify a type for a binder, in a manner similar to how sts#mapsto specifies types of applications, then there are at least three types that are involved:
   a. The result type of the binder.
   b. The type of the body to which the binder is applied (n-ary OMBIND #136 will of course raise new issues here, but never mind that now).
   c. The type of the bound variable(s).

It cannot in general be assumed that any two of these are equal. (a) and (b) are equal in many binders from analysis (\lim, \int, \sup, etc.—none of which currently have definitions as OpenMath binder symbols AFAIK), but are distinct in the important case of fns1#lambda. (c) is quite often distinct from both (a) and (b).

It thus seems the small type system needs some work.

[kohlhase]

moved to OpenMath/OMSTD#39