First page Back Continue Last page Overview Graphics
Categorial Type Inference Rules and OpenMath
OpenMath currently implicitly “knows”...
- Beta reduction (normal & n-ary)
- Currying of abstraction, but not of application or signatures
- Thus, our categorial semantics doesn't work!
- Our problem or an OpenMath problem??
OpenMath does not know any other rules yet
- Option: upgrade OpenMath Standard with a few such rules (~ ”OpenMath Expression Level”)
- Option: require definition of multiple signatures per symbol wrt rules above (”CD design rules”)
Notes: