First page Back Continue Last page Overview Graphics
Categorial Semantics for OpenMath : OMBIND
ombind(a,v1,...,vn,e) is type A · (E/Vn/.../V1)
- Different from STS and ECC (but similar!)
- Note that OM defines currying rule for bind
- Binders are therefore generally of type Y/(E/V)
Per-binder type assignments (lexicalism)
- type(lambda) = ((X/Y)/(X/Y))
- ((X/Y)/(X/Y)) · (E/V) = ((E/V)/(E/V)) · (E/V) = E/V
- Note “meta” type variables and unification
- type(forall) = 2/(2/X)
- With type “2” (boolean) plugged in from “outside”
- type(the) = (X/(2/X))
Notes: