Теория типов с записями

Теория типов с записями — это формальная структура представления семантики , использующая записи для выражения теории типов типов . Он использовался в обработке естественного языка , главным образом в вычислительной семантике и диалоговых системах .

Синтаксис

Тип записи — это набор полей . Поле — это пара, состоящая из метки и типа. В пределах типа записи метки полей уникальны. Свидетелем типа записи является запись . Запись представляет собой аналогичный набор полей, но поля содержат объекты, а не типы. Объект в каждом поле должен относиться к типу, объявленному в соответствующем поле типа записи.

Базовый тип: ${\begin{bmatrix}{\text{x}}:Ind\end{bmatrix}}$

Объект: ${\begin{bmatrix}{\text{x}}=a\end{bmatrix}}$

Тип: $\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]$

Объект: $\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]$

где $a$ и $b$ являются физическими лицами (тип $Ind$), $p_{1}$ является доказательством того, что $a$ мальчик и т. д.