First page Back Continue Last page Overview Graphics
Categorial Semantics for OpenMath : OMATTR
Attribution(a b,e) is type (A · B) · E
- very different from ECC and STS
Per-attribute-symbol type assignment
- type(typeset_as) = ( X/X ) / Y (the “default”)
- (((X/X)/Y) ·bold) ·ℝ = (X/X) ·ℝ = (ℝ/ℝ) ·ℝ = ℝ
- Attribute does not affect semantics, but is typed
- type(type) = (T / T) / ‘T’
- Unifier to type T given a descriptor for type T
- ‘…’ (“type descriptor”) for explicit type assignments
- e.g. (((T/T)/'T') ·'ℝ') ·X = ℝ ; T=X=ℝ, type(x)=X
Notes: