Categorial Types and OpenMath: Binders and Operators

• Binders as operators – and vice versa

  • Binder signature: operator with functional argument
  • Any OM object accepting one function as its argument can be used as a binder (proposal)
  • Any binder can be used as an operator accepting one function as argument (proposal)
  • “set-of” takes function (constructor) and predicate (selector), can only be used as an operator
  • Optional ”range” as operator only (next slide)
  • Meaning of compound binders clarified, e.g. ”exists uniquely”: $! º λP. ($x. P(x)) Ù ("y,z. (P(y) Ù P(z)) Þ y = z)

Notes: