 # 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: ${\begin{bmatrix}{\text{x}}:Ind\end{bmatrix}}$ Object: ${\begin{bmatrix}{\text{x}}=a\end{bmatrix}}$ Ptype: $\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: $\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 $a$ and $b$ are individuals (type $Ind$ ), $p_{1}$ is proof that $a$ is a boy, etc.

This page was last updated at 2019-11-13 06:00, View original page

All information on this site, including but not limited to text, pictures, etc., are reproduced on Wikipedia (wikipedia.org), following the . Creative Commons Attribution-ShareAlike License

Top

If the math, chemistry, physics and other formulas on this page are not displayed correctly, please useFirefox or Safari