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]

## 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.[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.

## References

1. ↑ Cooper, Robin (2005). "Records and Record Types in Semantic Theory". Journal of Logic and Computation 15 (2): 99–112. doi:10.1093/logcom/exi004.
2. ↑ Cooper, Robin (2010). Type theory and semantics in flux. Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics. Elsevier.
3. ↑ R. Cooper. Type theory and language: From perception to linguistic communication. Draft of book chapters available from https://sites.google.com/site/typetheorywithrecords/drafts

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Type theory with records. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Type_theory_with_records&oldid=3147784"