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.

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.

Basic type: [math]\displaystyle{ \begin{bmatrix} \text{x} : Ind \end{bmatrix} }[/math]

Object: [math]\displaystyle{ \begin{bmatrix} \text{x} = a \end{bmatrix} }[/math]

Ptype: [math]\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 ] }[/math]

Object: [math]\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 ] }[/math]

where [math]\displaystyle{ a }[/math] and [math]\displaystyle{ b }[/math] are individuals (type [math]\displaystyle{ Ind }[/math]), [math]\displaystyle{ p_1 }[/math] is proof that [math]\displaystyle{ a }[/math] is a boy, etc.