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: [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.
Original source: https://en.wikipedia.org/wiki/Type theory with records.
Read more |