First page Back Continue Last page Overview Graphics
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: