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:
Object:
Ptype:
Object:
where and are individuals (type ), is proof that is a boy, etc.
References
- ^ Cooper, Robin (2005). "Records and Record Types in Semantic Theory". Journal of Logic and Computation. 15 (2): 99–112. doi:10.1093/logcom/exi004.
- ^ Cooper, Robin (2010). Type theory and semantics in flux. Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics. Elsevier.
- ^ R. Cooper. Type theory and language: From perception to linguistic communication. Draft of book chapters available from https://sites.google.com/site/typetheorywithrecords/drafts
- v
- t
- e
- Compositionality
- Denotation
- Entailment
- Extension
- Generalized quantifier
- Intension
- Logical form
- Presupposition
- Proposition
- Reference
- Scope
- Speech act
- Syntax–semantics interface
- Truth conditions
Areas |
|
---|---|
Phenomena |
|
This semantics article is a stub. You can help Wikipedia by expanding it. |
- v
- t
- e