Type theory with records

Type theory with records is a formal semantics representation framework, using records to express type theory types. It has been used in natural language processing, principally computational semantics and dialogue systems.^[1][2]

Syntax

A record type is a set of fields. A field is a pair consisting of a label and a type. Within a record type, field labels are unique. The witness of a record type is a record. A record is a similar set of fields, but fields contain objects instead of types. The object in each field must be of the type declared in the corresponding field in the record type.^[3]

Basic type: ${\displaystyle {\begin{bmatrix}{\text{x}}:Ind\end{bmatrix}}}$ 

Object: ${\displaystyle {\begin{bmatrix}{\text{x}}=a\end{bmatrix}}}$ 

Ptype: ${\displaystyle \left[{\begin{array}{lll}{\text{x}}&:&Ind\\{\text{c}}_{\text{boy}}&:&boy({\text{x}})\\{\text{y}}&:&Ind\\{\text{c}}_{\text{dog}}&:&dog({\text{y}})\\{\text{c}}_{\text{hug}}&:&hug(x,y)\end{array}}\right]}$ 

Object: ${\displaystyle \left[{\begin{array}{lll}{\text{x}}&=&a\\{\text{c}}_{\text{boy}}&=&p_{1}\\{\text{y}}&=&b\\{\text{c}}_{\text{dog}}&=&p_{2}\\{\text{c}}_{\text{hug}}&=&p_{3}\end{array}}\right]}$ 

where ${\displaystyle a}$  and ${\displaystyle b}$  are individuals (type ${\displaystyle Ind}$ ), ${\displaystyle p_{1}}$  is proof that ${\displaystyle a}$  is a boy, etc.

References

1. Cooper, Robin (2005). "Records and Record Types in Semantic Theory". Journal of Logic and Computation. 15 (2): 99–112. doi:10.1093/logcom/exi004.
2. Cooper, Robin (2010). Type theory and semantics in flux. Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics. Elsevier.
3. R. Cooper. Type theory and language: From perception to linguistic communication. Draft of book chapters available from https://sites.google.com/site/typetheorywithrecords/drafts