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:
[
x
:
I
n
d
]
{\displaystyle {\begin{bmatrix}{\text{x)):Ind\end{bmatrix))}
Object:
[
x
=
a
]
{\displaystyle {\begin{bmatrix}{\text{x))=a\end{bmatrix))}
Ptype:
[
x
:
I
n
d
c
boy
:
b
o
y
(
x
)
y
:
I
n
d
c
dog
:
d
o
g
(
y
)
c
hug
:
h
u
g
(
x
,
y
)
]
{\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:
[
x
=
a
c
boy
=
p
1
y
=
b
c
dog
=
p
2
c
hug
=
p
3
]
{\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
a
{\displaystyle a}
and
b
{\displaystyle b}
are individuals (type
I
n
d
{\displaystyle Ind}
),
p
1
{\displaystyle p_{1))
is proof that
a
{\displaystyle a}
is a boy, etc.
^ 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
Central concepts Topics
Formalism
See also