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]

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 \left[\begin{array}{c}\text{x}:Ind\end{array}\right]}$

Object: ${\displaystyle \left[\begin{array}{c}\text{x}=a\end{array}\right]}$

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.

0.00 (0 votes) Original source: https://en.wikipedia.org/wiki/Type theory with records. Read more