Formalization of Contexts in Type Theory with Records and Modules.pdf Одна из основных проблем теоретико-типовой семантики [1] состоит в отсутствии адекватных методов работы с контекстами. Для восполнения этого дефицита Р. Купером была предложена теория типов с записями [2, 3]. Она, однако, обладает ограниченными возможностями в формализации таких феноменов, как референциальная непрозрачность контекстов. В то же время многие функциональные языки программирования, основанные на теории типов, содержат развитые модульные системы, позволяющие селективно скрывать или открывать информацию тех или иных фрагментов программы. В данной статье мы рассмотрим возможности, которые открываются для формализации контекстов в теории типов с записями и модулями. Формализация будет проведена на языке программирования с зависимыми типами Agda. Использование языка программирования для работы в теоретико-типовой семантике не случайно. Теория типов тесно связана как с логикой, так и вычислениями, в частности с программированием. В контексте теоретико-типовой семантики мы можем понимать смысл как нечто вычисляемое, поэтому многие семантические проблемы оказываются связанными с разработкой способов (или программ) вычисления смысла или референта. Agda, как и многие системы для работы с доказательствами, не создавалась специально для нужд семантики естественного языка, она, скорее, ориентирована на математику и логику. По этой причине ее ресурсы, возможно, недостаточно адекватны проблеме, поэтому одна из задач исследования состоит в тестировании пределов этой адекватности. Конечной целью (не достигаемой, разумеется, в данной краткой статье) является разработка универсального инструментария для работы с семантическими проблемами. Код Agda с описываемой формализацией доступен по адресу: https://github.com/odomanov/ttsemantics/. Необходимые сведения о синтаксисе Agda Нам не потребуется Agda во всем объеме, поэтому в данном разделе описано лишь то, что необходимо для дальнейшего изложения (для более подробного введения см., напр.: [4, 5]). Agda является функциональным языком программирования, основанным на варианте теории типов П. Мартин-Лёфа [6, 7], и во-многом следует ее обозначениям. Программы на Agda состоят из файлов в кодировке Юникод, что позволяет использовать в них большинство математических символов, таких как кванторы, различные стрелки и пр. Типы в Agda понимаются как множества, поэтому запись A : Set означает, что A является типом (существует также иерархия типов, но она нам не понадобится). Запись a : A означает, что a относится к типу A, т.е. является термом, или элементом, типа A. При определениях сначала декларируется тип определяемого, а затем после равенства записывается само определение, например: a : A a = ... Тип функций перехода из типа A в тип B обозначается как A ^ B. Функция определяется действием на свои аргументы. Например, если тип A состоит из двух элементов Tom и Jerry, то функция в тип натуральных чисел может быть определена следующим образом: f : A ^ Nat f Tom = 1 f Jerry = 3 Здесь сначала задается тип функции, а затем - ее значения на элементах типа (Agda требует, чтобы функция была определена на всех этих элементах). При определении функции предполагается, что ее аргументы следуют за ее именем, однако Agda допускает и инфиксную, а также смешанную нотацию: _+_ : Nat ^ Nat ^ Nat Здесь подчерки обозначают места для переменных; применение так определенной функции можно записывать обычным образом как 1 + 4 (но также, при желании, и как _+_ 1 4). Если аргументы функции зависят друг от друга, то соответствующие термы могут быть указаны явно. Например: f : (n : Nat) ^ Fin n ^ C Здесь Fin n - (зависимый) тип чисел, меньших n (конечное множество). Согласно соответствию Карри-Ховарда типы соответствуют пропозициям, и существование элемента типа можно рассматривать как существование доказательства пропозиции (и обратно). Поэтому предикаты или пропозициональные функции определяются как функции в Set. Например, A ^ Set -это одноместный предикат на типе A, A ^ B ^ Set - двуместный на типах A, B и т.д. Благодаря наличию этого соответствия доказательства пропозиций обычно выглядят в Agda следующим образом: prf : Proposition prf = ... Здесь в первой строчке декларируется существование доказательства для Proposition, а затем записывается, чему это доказательство равно. Если имя доказательства несущественно и далее не используется, то допустимо писать: _ : Proposition Я ниже буду часто пользоваться такой записью, приводя при этом доказательства почти без пояснений - для целей данной статьи их конкретный вид обычно не важен, важно лишь наличие. Помимо определения или вычисления типы и их элементы могут быть постулированы: postulate _runs : A ^ Set p : Tom runs Здесь постулировано существование предиката runs на типе A, а также доказательства пропозиции Tom runs. Постулаты, вообще говоря, нарушают принципы конструктивной математики, на которой основана теория Мар-тин-Лёфа. Например, мы можем постулировать существование доказательства дизъюнкции, не предполагая существования доказательства конкретного члена этой дизъюнкции. В случае семантики, однако, это не является недостатком, поскольку люди могут иметь подобные убеждения, и данное свойство позволяет нам их моделировать. Данная запись демонстрирует также роль отступов в Agda. Команда postulate начинает блок, который отмечается отступом, величина которого фиксируется первой строкой после postulate. После этого строки с тем же отступом относятся к начатому блоку, а любая строка с меньшим отступом заканчивает блок. Таким образом, две декларации выше относятся к одному блоку postulate. Аналогично любое выражение считается продолжающимся на следующие строки, если они записаны с отступом. Различные значения в Agda могут определяться как неявные в случаях, когда Agda в состоянии найти их самостоятельно. Эти значения помещаются в фигурные скобки. Например, функция func : {A B : Set} ^ (f : A ^ B) ^ C имеет три аргумента: типы A и B и функцию f : A ^ B. Однако указания последнего аргумента достаточно для того, чтобы вычислить два первых, поэтому они выше определены как неявные. При применении функции func они не указываются. Модульная система Программа на Agda может содержать множество функций, переменных, констант и пр. Было бы неудобно придумывать им всем различные имена. Agda обладает простой, но мощной системой, позволяющей гибко управлять использованием имен. Для этого программа разбивается на модули, в каждом из которых имена должны быть уникальными. Чтобы снаружи модуля M обратиться к имени name, находящемуся внутри него, следует использовать полное имя M. name. Модули могут быть вложены с произвольной глубиной, так что имена также могут иметь несколько уровней: M1.M2 .M3. name. Модуль задается следующей директивой: module M where Эта директива открывает блок, в котором записываются декларации модуля. Для того чтобы сделать имена объектов модуля доступными вне него не по полным, а по сокращенным именам, модуль может быть открыт: open M При этом Agda содержит средства управления тем, какие именно имена могут быть открыты или, наоборот, скрыты. Для этого существуют модификаторы using, hiding и renaming. Например, команда open M using (n1; n2) renaming (n3 to new3) делает доступными только объекты n1, n2 и n3, при этом последний - под именем new3. Команда open M hiding (n2; n3) открывает все имена, кроме n2 и n3. И так далее. Модули можно открывать внутри других модулей, при этом если модуль M2 открывается внутри модуля M1 , то конструкция module M1 where open M2 public означает, что при открытии модуля M1 имена из M2 также становятся доступными (с возможными модификаторами using, hiding, renaming). Модули могут иметь параметры. Например, module M (A : Set) (x : A) where f : B g : A ^ B означает, что все, определенное внутри модуля M, зависит также от дополнительных аргументов типов Set и A. То есть при открытии модуля M функции, которые становятся доступными, имеют следующие типы: f : (A : Set) ^ (x : A) ^ B g : (A : Set) ^ (x : A) ^ A ^ B Такой параметризованный модуль может быть открыт с явно указанными параметрами, например: open M Nat n В этом случае становятся доступными функции типов f : B g : Nat ^ B В результате модульная система предоставляет нам гибкий инструмент для открытия и сокрытия имен, который поможет моделировать прозрачность или непрозрачность контекстов. Для этого нам понадобится также понятие записи. Записи, модули и референциальная непрозрачность Согласно Мартин-Лёфу, основное суждение теории типов a : A представляет собой суждение знания. Его смысл (который, как выражается Мар-тин-Лёф, мы «поясняем») состоит в том, что утверждается существование элемента a, относящегося к типу A. В таком виде теория типов близка ситуационной семантике [8]. Это обстоятельство, а также роль в нем структуры записей отмечены Купером [3]. Я поэтому буду называть моделируемые контексты ситуациями (хотя их связь с ситуационной семантикой, разумеется, должна быть исследована отдельно). Записи (records) являются стандартной структурой многих языков программирования. С точки зрения теории типов они являются обобщением зависимых S-типов или типом кортежей, в котором проекции имеют имена. В упрощенном виде, которого нам для дальнейшего достаточно, тип записи в Agda записывается следующим образом: record R А : Set where field f1 : A1 f2 : A2 Здесь R - имя записи, А - параметры, от которых запись может зависеть, f1, f2, ... - имена полей записи, т.е. термов типов A1, A2, ... (каждый из них может зависеть от предыдущих). Терм записи представляет собой кортеж, состоящий из термов, соответствующих полям, и записывается как r = record { f1 = a1; f2 = a2; ...} Здесь a1, a2, ...- термы типов A1, A2, ... С точки зрения теории типов поля являются проекциями S-типов, т.е. функциями типов (без учета параметров): f1 : R ^ A1 f2 : R ^ A2 В частности, для указанного выше терма записи r выполнены равенства f1 r = a1 f2 r = a2 (= и S обозначают пропозициональное, т.е. доказываемое, равенство и неравенство). Так определенные, записи сходны с модулями. И действительно, Agda для каждой записи определяет соответствующий параметризованный модуль с тем же именем: module R {А} (r : R А) where f1 : A1 f1 = R.f1 r f2 : A2 f1 = R.f2 r (вспомним, что объекты параметризованных модулей являются функциями от параметров). Поэтому записи (фактически, соответствующие им модули) также могут быть открыты, причем допускают использование модификаторов. Более того, при задании записи мы можем добавлять декларации в ее модуль, например: record R А : Set where field f1 : A1 f2 : A2 b : B b = ... Или даже: record R А : Set where field f1 : A1 f2 : A2 open M public В последнем случае при открытии записи R будут также доступны определения из модуля M. Системы знаний, частным случаем которых являются контексты или ситуации, могут быть моделированы либо как модули, либо как записи. Если мы хотим просто вычислить нечто внутри некоторого контекста, то нам достаточно задать модуль с соответствующими определениями и провести в нем необходимые действия. Если же нам требуется метаязык, т.е. высказывания о самих контекстах, композиции контекстов и т.д., то они должны быть определены как термы некоторого типа. В этом случае необходимо формализовать типы контекстов как записи. Рассмотрим моделирование убеждений (belief reports) на классическом примере референциальной непрозрачности, принадлежащем Куайну [9]: некий Ральф знает двух человек - назовем их человеком в шляпе и человеком на пляже - как двух разных людей, причем первого считает шпионом, а второго нет; мы, однако, знаем, что это один и тот же человек по имени Орткут. Прежде всего постулируем существование типа Man и предиката «быть шпионом»: postulate Man : Set _is-a-spy : Man ^ Set Если ситуации определены как записи, то мы можем их комбинировать. Действительно, пусть задан простейший тип ситуаций «Имеется объект типа А»: record SitSmth (А : Set) : Set where field smth : A Как видно, этот тип записей имеет единственное поле, представляющее собой объект типа А. Частным случаем таких ситуаций являются ситуации типа «Имеется человек»: record SitMan : Set where field sitsmth : SitSmth Man open SitSmth sitsmth renaming (smth to man) public Единственным полем этой ситуации является ситуация типа SitSmth с параметром, равным Man. Эта ситуация открыта публично с переименованием поля (фактически, функции) smth в поле (функцию) man. Мы можем далее использовать эту ситуацию как строительный материал для ситуации «Имеется шпион»: record SitSpy : Set where field sitMan : SitMan open SitMan sitMan public field man-spy : man is-a-spy Эта ситуация состоит из ситуации «Имеется человек» и доказательства того, что этот человек шпион. При этом ситуация SitMan открывается, делая доступным объект man, который затем используется. Подобным образом мы можем составлять сложные ситуации из простых, открывая (или не открывая) их, добавляя новую информацию и т.д. Система убеждений Ральфа может быть теперь представлена как модуль module RalphBelief where postulate sitSpy : SitSpy open SitSpy sitSpy public Модуль SitSpy здесь открыт, поэтому мы можем (внутри модуля RalphBelief) записать утверждение о том, что человек, в существование которого верит Ральф, является шпионом, просто как «man is-a-spy», причем его доказательством будет просто доступное Ральфу man-spy: _ : man is-a-spy _ = man-spy Без открытия модуля мы должны были бы писать _ : SitMan.man (SitSpy.sitMan sitSpy) is-a-spy _ = SitSpy.man-spy sitSpy Таким образом, вне модуля RalphBelief - т.е. для нас, вне системы убеждений Ральфа - некоторые доказательства и даже формулировка пропозиций могут оказаться невозможными, если мы не разделяем суждений, в которые верит Ральф. Мы можем, однако, проводить доказательства в локальном контексте, что записывается следующим образом: _ : S[ x G Man ] x is-a-spy _ = man , man-spy where open RalphBelief Здесь S[ x G A ] B обозначает тип (Xx : A)B, т.е. экзистенциальную квантификацию (или, при другой интерпретации, - подмножество элементов множества A, таких что B ). Таким образом, доказываемая пропозиция означает «Существует человек, который является шпионом» (а ее доказательством является пара, состоящая из человека и доказательства того, что он шпион). Директива where позволяет задать локальный контекст, в котором могут быть определены дополнительные типы, их термы, а также открыты модули. В данном случае, мы открываем модуль убеждений Ральфа, т.е. проводим доказательство «внутри» этих убеждений. Вне контекста Ральфа, т.е. для нас, доказательство превращается в следующее: _ : S[ x G Man ] x is-a-spy _ = RalphBelief.man , RalphBelief.man-spy Мы видим, что модульная система позволяют нам разделять наборы убеждений и контролировать то, какая информация доступна нам и Ральфу. Тем самым моделируется контролируемым образом непрозрачность доксических контекстов, которая составляла проблему для Куайна. Действительно, в полном виде убеждение Ральфа можно записать следующим образом: record SitTwo : Set where field {man-in-a-hat} : Man {man-on-the-beach} : Man hspy : man-in-a-hat is-a-spy bspy : - man-on-the-beach is-a-spy h£b : man-in-a-hat £ man-on-the-beach module RalphBelief where postulate sit : SitTwo open SitTwo sit public Здесь SitTwo - это ситуация, в которой есть два различных человека - в шляпе и на пляже - один из которых шпион, а другой нет. Конкретное строение ситуации SitTwo зависит от наших предпочтений, удобства и пр. Например, мы могли бы определить ситуацию SitMan как индексированную натуральным числом и содержащую несколько человек (в частном случае -одного). В этом случае SitTwo могла бы содержать ситуацию SitMan 2 вместо двух элементов типа Man. Язык предоставляет нам определенную гибкость. Приведенное определение является одним из простейших. Аналогично предыдущему модуль RalphBelief моделирует убеждения Ральфа. Внутри него мы можем легко доказать: _ : man-in-a-hat is-a-spy _ = hspy _ : S[ x G Man ] - x is-a-spy _ = man-on-the-beach , bspy Пусть теперь наша система убеждений выглядит следующим образом: module OurBelief where open RalphBelief using (man-in-a-hat; man-on-the-beach) postulate Ortcutt : Man o=h : Ortcutt = man-in-a-hat o=b : Ortcutt = man-on-the-beach Здесь в RalphBelief открываются только элементы man-in-a-hat и man-on-the-beach, что означает, что мы разделяем с Ральфом знание о существовании этих людей (для него и для нас это одни и те же люди), но не убеждение об их различии, а также принадлежности или непринадлежности к шпионам. Но зато мы знаем, что оба эти человека являются на самом деле одним и тем же человеком по имени Орткут. Поскольку информация о принадлежности к шпионам не содержится в нашем контексте, мы не можем, например, доказать, что Орткут шпион. Однако мы можем это сделать, если откроем RalphBelief полностью (что означает, что мы полностью согласимся с Ральфом): _ : Ortcutt is-a-spy _ = subst (A x ^ x is-a-spy) (sym (proj2 (proj2 hs))) hspy where open RalphBelief hs : S[ x G Man ] x is-a-spy x Ortcutt = x hs = man-in-a-hat , hspy , o=h Аналогичным образом мы можем доказать, что Орткут не может быть шпионом, что показывает, что наша с Ральфом объединенная система убеждений противоречива (хотя в каждой из них противоречие доказать невозможно). Впрочем, мы можем вывести противоречие более коротким путем, если предварительно докажем (находясь в нашем контексте), что человек в шляпе совпадает с человеком на пляже: h=b : man-in-a-hat = man-on-the-beach h=b = trans (sym o=h) o=b _ : 1 _ = contradiction h=b (RalphBelief.hSb) Вместе с тем, как нетрудно видеть, открытие дополнительно, например, только hspy (т.е. наше согласие с Ральфом в том, что человек в шляпе шпион) не приводит к противоречию. Таким образом, теория типов с записями и модульной системой позволяет нам разделять системы убеждений и корректно описывать эффекты непрозрачности контекстов. Семантические вычисления: абстрактный и конкретный смысл Рассмотрим еще один пример, а именно понятия абстрактного и конкретного смыслов, как они определяются в ситуационной семантике. В ситуационной семантике для существования смысла (meaning) требуется наличие трех условий [10. P. 610-613]: 1) ситуации говорения кем-то некоторых высказываний, 2) описываемой или фокальной ситуации - той, о которой идет речь в ситуации говорения, 3) референций, устанавливаемых говорящим (speaker's connections) и определяющих, что имеет в виду говорящий, употребляя те или иные языковые выражения. Дополнительно могут понадобиться другие ситуации, например ресурсные, которые непосредственно не присутствуют, но необходимы для вычисления значений, такие как общие знания, ситуации из прошлого и пр. Таким образом, о смысле можно говорить, лишь предполагая ситуацию, в которой кто-то говорит о чем-то, употребляя слова определенным образом. Для описания этой структуры зададим следующие типы: postulate Human LOC TIM Referable : Set и предикаты postulate _speaks-to_/_,_ : Human - Human - LOC - TIM - Set _utters_/_,_ : Human - String - LOC - TIM - Set _refers-to_via_/_,_ : Human -> Referable -> String -> LOC -> TIM - Set Здесь Human - тип людей, LOC и TIM - типы мест и времен, которые я не буду далее конкретизировать, String - встроенный тип, обозначающий строку символов, а Referable - специальный тип, которым будем обозначать все, на что может существовать референция в речи (см. ниже). Предикаты означают: h1 speaks-to h2 / l , t «Человек h1 говорит (что-то) человеку h2 в месте l в момент времени t» h utters S / l , t «Человек h произносит фразу S в месте l в момент времени t» h refers-to E via S / l , t «Человек h отсылает к сущности E посредством фразы S в месте l в момент времени t». Это позволяет нам определить ситуацию говорения: record SitUttering : Set where field {l} : LOC {t} : TIM {speaker} : Human {listener} : Human {phr} : String spk : speaker speaks-to listener / l , t utt : speaker utters phr / l , t Эта ситуация содержит место и время говорения, говорящего (спикера), слушателя, произносимую фразу phr и доказательства того, что говорящий обращается к слушателю и произносит данную фразу. Фигурные скобки вокруг полей означают, что их значения являются имплицитными, и Agda будет пытаться самостоятельно их вычислить. Это позволит нам в дальнейшем для определения термов SitUttering указывать лишь поля spk и utt, остальные Agda будет способна восстановить по типам последних. Рассмотрим пример [10. P. 610]. Пусть Мелисса говорит Наоми: «Человек у двери» (A man is at the door). Когда она это говорит, то: 1) обращается к Наоми; 2) производит отсылки (референции) к человеку и двери, также присутствующим в ситуации. Соответственно, для формализации определим дополнительно типы дверей, объектов и ситуаций: postulate Door Object SIT : Set Вообще говоря, термы почти всех типов одновременно относятся к типу Referable, поскольку о них можно говорить. Agda (как и теория типов Мартин-Лёфа) не позволяет относить термы к нескольким типам одновременно и не содержит встроенного механизма приведения типов (коэрсии). Однако его можно определить посредством подходящей функции. Например, коэрсия Door

Скачать электронную версию публикации