First page Back Continue Last page Overview Graphics
Categorial Types
Notation due to Lambek, modified to our needs
Abstraction A/B – returns something of type A if given argument of type B
- STS “mapsto(B,A)”; vernacular AB
- A/B/C/D : three args
Application A·B – something of type A applied to an argument of type B
- STS “application(A,B)”; vernacular ??)
- (A/Z/Y/X) · X · Y · Z “simplifies” to type A
Plug in any type system (e.g. ECC) for atoms
- Hence “categorial” semantics / type logic
Notes: