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]
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:
\begin{bmatrix}x:Ind\end{bmatrix}
Object:
\begin{bmatrix} x=a \end{bmatrix}
Ptype:
\left[\begin{array}{lll} x&:&Ind\\ cboy&:&boy(x)\\ y&:&Ind\\ cdog&:&dog(y)\\ chug&:&hug(x,y) \end{array}\right]
Object:
\left[\begin{array}{lll} x&=&a\\ cboy&=&p1\\ y&=&b\\ cdog&=&p2\\ chug&=&p3 \end{array}\right]
where
a
b
Ind
p1
a