Полная полнота против полной абстракции программного перевода

Усилия по проверке компилятора часто сводятся к тому, чтобы доказать, что компилятор полностью абстрактен: он сохраняет и отражает (контекстуальные) эквивалентности.

Вместо того, чтобы предоставлять полные доказательства абстракции, некоторые недавние (основанные на категориях) работы по проверке компилятора Hasegawa [ 1 , 2 ] и Egger et. и др. [ 3 ] доказать полную полноту различных переводов CPS.

Вопрос: В чем разница между полной полнотой и полной абстракцией?

Для меня полнота просто выглядит как отражение эквивалентности для перевода, а полнота представляется следствием сохранения эквивалентности.

Примечание : и Curien [ 7 ], и Abramsky [ 8 ] исследуют связь между определимостью, полной абстракцией и, в некоторой степени, полной полнотой. Я подозреваю, что у этих ресурсов может быть ответ на мой вопрос, но после поверхностного чтения я еще не подтвердил это.

Немного предыстории : термин «полная полнота» был придуман Абрамским и Ягадисаном [ 4 ] для характеристики правильности игровой семантической модели мультипликативной линейной логики.

Blute [ 5 ] дает следующее определение:

Пусть $\mathcal{F}$ свободная категория. Мы говорим , что категорический модель $\mathcal{M}$ является полностью завершен для $\mathcal{F}$ , или что мы имеем полную завершенность $\mathcal{F}$ относительно $\mathcal{M}$ , если, по некоторой интерпретации генераторов, единственный свободный функтор $[\![ - ]\!] : \mathcal{F} \rightarrow \mathcal{M}$ заполнено.

Насколько я могу судить, Хасэгава в [ 6 ] первым адаптировал полную полноту для описания перевода программы вместо категориальной семантической модели. В этом случае перевод Жирара из просто набранного лямбда-исчисления в линейное лямбда-исчисление. Позже, в [ 1 ], он определяет полную полноту перевода CPS $(\cdot)^\circ$ как:

Если $\Gamma^{\circ};\emptyset \vdash N : (\sigma^\circ \rightarrow o) \multimap o$ выводима в линейное лямбда - исчисление, то существует в вычислительном лямбда - исчислении , такие , что выполняется в линейном лямбда-исчислении. $\Gamma \vdash M : \sigma$ $\Gamma^{\circ};\emptyset \vdash M^\circ = N : (\sigma^\circ \rightarrow o) \multimap o$

(где - базовый тип в линейном лямбда-исчислении (целевой язык), но не в вычислительном лямбда-исчислении (исходный язык).) $o$

Мне определение Хасэгавы кажется полнотой и должно действительно сочетаться с полнотой, чтобы получить полную полноту.

Эггер и др. и др. [ 3 ] определить полную полноту перевода CPS как комбинацию (1) полноты и (2) полноты: $(\cdot)^v$

(1): Если и затем $\Theta \vdash M,N : \tau$ $\Theta^v | - \vdash M^v =_{\beta\eta} N^v : !\tau^v$ $\Theta \vdash M =_{\lambda_c} N : \tau$

(2): если $\Theta^v | - \vdash t : !\tau^v$ то существует такой термин , что $\Theta \vdash M : \tau$ $\Theta^v | - \vdash M^v =_{\beta\eta} t : !\tau^v$

(где $=_{\lambda_c}$ - вычислительная )

[1] « Линейно используемые эффекты: монадические и CPS-преобразования в линейное лямбда-исчисление », Hasegawa 2002

[2] « Семантика линейного продолжения-прохождения в обращении по имени », Хасегава, 2004

[3] « Линейные трансляции CPS в исчислении обогащенных эффектов », Egger et. и др. 2012

[4] « Игры и полная полнота мультипликативной линейной логики », Абрамский и Ягадисан, 1992

[5] « Теория категорий для линейных логиков », Blute 2003

[6] « Перевод Жирара и логические предикаты », Хасегава 2000

[7] « Определимость и полная абстракция », Curien 2007

[8] " Аксиомы определимости и полной полноты ", Абрамский, 1999

pl.programming-languages ct.category-theory semantics denotational-semantics program-verification Филип Мэйтс
источник

Ответы:

К сожалению, здесь слишком много всего происходит. Так что все легко перепутать. Использование «полной» в «полной полноте» и «полной абстракции» относится к совершенно разным представлениям о полноте. Но есть также некоторая неопределенная связь между ними. Таким образом, это будет сложный ответ.

Полная завершенность : «Звук и завершенность» - это свойство, которое вы хотите, чтобы традиционная логика имела в отношении своей семантики. Обоснованность означает, что все, что вы можете доказать в логике, верно в семантической модели. Полнота означает, что все, что верно в семантической модели, доказуемо в логике. Мы говорим, что логика является правильной и полной для конкретной семантической модели. Когда мы приходим к конструктивной логикеНапример, теорию типа Мартина-Лофа или линейную логику, нас интересует не только доказуемость формул, но и их доказательства. У доказуемой формулы может быть много доказательств, и конструктивная логика хочет их отделить. Таким образом, семантика для конструктивной логики включает в себя указание не только того, является ли формула истинной, но также некоторое абстрактное семантическое понятие «доказательства» («доказательства») для ее истинности. Абрамский и его коллеги придумали термин «полная полнота», чтобы обозначить, что доказательства в логике могут выражать все семантические доказательства в модели. Итак, «полный» относится к доказательствам здесь. «Полная» логика может доказать все, что нужно. «Полностью завершенная» логика имеет все доказательства, которые ей необходимы. Таким образом, «полная полнота» означает «конструктивная полнота» или «доказательная полнота». Это не имеет ничего общего с полной абстракцией.

Полная абстракция : «Адекватный и полностью абстрактный» - это свойство, которое вы хотите для семантической модели языка программирования. (Обратите внимание на первое отличие: мы сейчас имеем дело со свойствами семантической модели, а не свойства языка!) Адекватность означает, что всякий раз, когда два термина имеют одинаковое значение в семантической модели, они обсервационно эквивалентны в языке программирования (по отношению к некоторому понятию исполнения). Полная абстракция означает, что, если два термина обсервационно эквивалентны, они имеют одинаковое значение в семантической модели. Эти идеи могут быть связаны с обоснованностью и полнотой, но несколько надуманным способом. Если мы думаем о семантической модели языка программирования как о «логике» или «методе доказательства», чтобы говорить о наблюдательной эквивалентности, то адекватность означает, что этот метод доказательства является надежным; полная абстракция означает, что этот метод доказательства завершен. Нет понятия «полная полнота»метод доказательства. (Но такая вещь теоретически возможна, и на днях кто-то может сделать это.)

В вашем случае вас интересуют переводы, а не семантические модели. Свойства адекватности и полной абстракции могут быть расширены, чтобы иметь дело с переводами следующим образом. Вы рассматриваете целевой язык как свою «семантическую модель», то есть формализм, который вы как-то полностью понимаете. Если это так, у вас есть некоторое представление об эквивалентности для него. Затем мы говорим, что перевод является адекватным, если всякий раз, когда переводы двух исходных программ эквивалентны на целевом языке, они обсервационно эквивалентны на исходном языке. Мы говорим, что это полностью абстрактно, если, когда две исходные программы обсервационно эквивалентны на исходном языке, их переводы эквивалентны на целевом языке.

τ (M) ≅ τ (N) ⟹ M ≅ N

$\tau(M) \cong \tau(N) \Longrightarrow M \cong N$

M ≅ N ⟹ τ (M) ≅ τ (N)

$M \cong N \Longrightarrow \tau(M) \cong \tau(N)$

M ≅ N ⟺ τ (M) ≅ τ (N)

$M \cong N \iff \tau(M) \cong \tau(N)$

$A$ $A$

\forall N : τ (A) . \exists M : A . τ (M) = N

$\forall N : \tau(A).\; \exists M : A.\, \tau(M) = N$

Теперь о неясной связи между полной полнотой и полной абстракцией. Доказательство того, что семантическая модель или перевод полностью абстрактны, часто подразумевает определенность. Это потому, что наши языки, как правило, высшего порядка. Таким образом, если у семантической модели или целевого языка слишком много «контекстов», тогда он сможет высовывать наши термины или смысловые значения нежелательными способами и испортить их эквивалентность. «Нежелательные пути» означают, что язык программирования сам по себе их не сможет сунуть. Таким образом, чтобы получить полную абстракцию, нам нужно убедиться, что «контексты», доступные в семантической модели или в целевом языке, исходят от тех, которые в исходном языке в той или иной форме. Обратите внимание, что это относится к свойству полной полноты.

Почему мы хотим такие свойства? Это не имеет ничегоделать с компиляторами! Мы хотим эти свойства, чтобы утверждать, что исходный язык встраивается в целевой язык. Если мы довольны определенным целевым языком (чистым, понятным, каким-то фундаментальным или богоданным), то, если исходный язык встраивается в него, то мы можем утверждать, что в исходном языке нет ничего нового. Это просто фрагмент целевого языка, который мы знаем и любим. Это просто синтаксический сахар. Таким образом, полностью абстрактные переводы даются людьми, чтобы установить, что конкретные целевые языки великолепны. Они также иногда даются людьми, которые имеют большой или сложный язык для общения. Таким образом, вместо определения семантики для него напрямую, они переводят его на некоторый базовый язык и затем дают семантику для базового языка. Например, отчет Haskell делает это. Но полная абстракция этих переводов редко когда-либо доказывается, потому что исходные языки большие и сложные. Люди верят, что перевод хорош.

Еще раз, это не имеет ничего общего с компиляторами. Компиляторы редко бывают адекватными или полностью абстрактными. И они не должны быть! Все, что нужно сделать компилятору - это сохранить поведение выполнения завершенных программ. Целевой язык компилятора, как правило, огромный, что означает, что он имеет много контекстов, которые могут испортить эквивалентность. Таким образом, эквивалентные программы на исходном языке практически никогда не являются контекстно-эквивалентными при компиляции.

Удай Редди
источник

Что вы имеете в виду, говоря, что нет никаких языков, которые мы действительно "понимаем"?

Мартин Бергер

Что вы имеете в виду, говоря, что никто еще не создал семантическую модель, которая представляет собой метод конструктивного доказательства?

Мартин Бергер

Извините, но последствия для "переводов" кажутся мне неправильными по сравнению с вашим предыдущим текстом. Полная абстракция, скажем, для PCF запрашивает M≅N⟹τ (M) ≅τ (N) (где τ обозначает денотационную семантику и игнорирует необходимость изменения символов): как вы говорите, «полная абстракция означает, что если два термина обсервационно эквивалентны, они имеют одинаковое значение в семантической модели ". Но вы подразумеваете обратное (а именно, вы пишете τ (M) ≅τ (N) ⟹M≅N)! Или переводы работают иначе, чем денотационная семантика?

Blaisorblade

@Blaisorblade: Вы абсолютно правы! Я внес исправление в текст моего ответа.

Удай Редди

Полная абстракция также представляет интерес для безопасности на уровне языка и, возможно, для межъязыковой интеграции. Т.е. полезно знать, что ничто на целевом языке не может нарушать абстракции исходного языка.

dmbarbour

Резюме: полная полнота означает, что функция интерпретации не только завершена, но и сюръективна в программах. Полная абстракция не требует сюръективности. $\newcommand{\semb}[1]{[\![ #1 ]\!]}$

$\semb{.}$

$A$ $\semb{A}$
$\Gamma$ $\semb{\Gamma}$
$\Gamma \vdash P : \alpha$ $\semb{\Gamma} \vdash \semb{P} : \semb{\alpha}$

$\semb{.}$

P ≅^{S} Q iff [[P]] ≅^{T} [[Q]]

$P \cong^S Q\ \ \ \ \ \text{iff}\ \ \ \ \ \semb{P} \cong^T \semb{Q}$

$P, Q$ $\cong^S$ $\cong^T$

P ≅_{Γ, α}^{S} Q iff [[P]] ≅_{[[Γ]], [[α]]}^{T} [[Q]]

$P \cong^S_{\Gamma, \alpha} Q\ \ \ \ \ \text{iff}\ \ \ \ \ \semb{P} \cong^T_{\semb{\Gamma}, \semb{\alpha}} \semb{Q}$

Γ, α, P, Q

$\Gamma, \alpha, P, Q$

[[.]]

$\semb{.}$

$\semb{.}$ на целевом языке обозначение некоторого $\semb{\Gamma} \vdash Q : \semb{\alpha}$ $\Gamma \vdash P : \alpha$ $Q = \semb{P}$ быть сюръективным в отношении типов и контекстов, потому что это свойство редко имеет место в интерпретациях, которые обычно нас интересуют. $\semb{.}$

Мартин Бергер
источник